Rebase of #1040, do not merge to main

primer/src/Primer/API.hs

@@ -1183,7 +1183,7 @@ availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, se
       (editable, def) <- findASTTypeDef allTypeDefs sel.def
       let getActions = case sel.node of
             Nothing -> Available.forTypeDef
-            Just (TypeDefParamNodeSelection _) -> Available.forTypeDefParamNode
+            Just (TypeDefParamNodeSelection p) -> Available.forTypeDefParamNode p
             Just (TypeDefConsNodeSelection s) -> case s.field of
               Nothing -> Available.forTypeDefConsNode
               Just field -> Available.forTypeDefConsFieldNode s.con field.index field.meta

primer/src/Primer/Action.hs

@@ -30,6 +30,7 @@ import Control.Monad.Fresh (MonadFresh)
 import Data.Aeson (Value)
 import Data.Bifunctor.Swap qualified as Swap
 import Data.Bitraversable (bisequence)
+import Data.Data (Data)
 import Data.Functor.Compose (Compose (..))
 import Data.Generics.Product (typed)
 import Data.List (delete, findIndex, insertBy)
@@ -1051,6 +1052,7 @@ renameForall b zt = case target zt of
 
 -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's.
 toProgActionNoInput ::
+  (HasID a, Data a) =>
   DefMap ->
   Either (ASTTypeDef a) ASTDef ->
   Selection' ID ->
@@ -1084,18 +1086,27 @@ toProgActionNoInput defs def0 sel0 = \case
     -- on the domain (left) side of the arrow.
     toProgAction [ConstructArrowL, Move Child1]
   Available.AddInput -> do
-    -- This action traverses the function type and adds a function arrow to the end of it,
-    -- resulting in a new argument type. The result type is unchanged.
-    -- The cursor location is also unchanged.
-    -- e.g. A -> B -> C ==> A -> B -> ? -> C
-    id <- nodeID
-    def <- termDef
-    type_ <- case findType id $ astDefType def of
-      Just t -> pure t
-      Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of
-        Just (TypeNode t) -> pure t
-        Just sm -> Left $ NeedType sm
-        Nothing -> Left $ IDNotFound id
+    type_ <- case def0 of
+      Left def -> do
+        (tName, vcName, field) <- conFieldSel
+        let id = field.meta
+        vc <- maybeToEither (ValConNotFound tName vcName) $ find ((== vcName) . valConName) $ astTypeDefConstructors def
+        t <- maybeToEither (FieldIndexOutOfBounds vcName field.index) $ flip atMay field.index $ valConArgs vc
+        case findType id t of
+          Just t' -> pure $ forgetTypeMetadata t'
+          Nothing -> Left $ IDNotFound id
+      Right def -> do
+        -- This action traverses the function type and adds a function arrow to the end of it,
+        -- resulting in a new argument type. The result type is unchanged.
+        -- The cursor location is also unchanged.
+        -- e.g. A -> B -> C ==> A -> B -> ? -> C
+        id <- nodeID
+        forgetTypeMetadata <$> case findType id $ astDefType def of
+          Just t -> pure t
+          Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of
+            Just (TypeNode t) -> pure t
+            Just sm -> Left $ NeedType sm
+            Nothing -> Left $ IDNotFound id
     l <- case type_ of
       TFun _ a b -> pure $ NE.length $ fst $ unfoldFun a b
       t -> Left $ NeedTFun t

primer/src/Primer/Action/Available.hs

@@ -69,6 +69,7 @@ import Primer.Core (
   Pattern (PatCon, PatPrim),
   PrimCon (PrimChar, PrimInt),
   TyConName,
+  TyVarName,
   Type,
   Type' (..),
   TypeMeta,
@@ -84,7 +85,7 @@ import Primer.Core (
   _typeMetaLens,
  )
 import Primer.Core.Transform (decomposeTAppCon)
-import Primer.Core.Utils (forgetTypeMetadata, freeVars)
+import Primer.Core.Utils (forgetTypeMetadata, freeVars, freeVarsTy)
 import Primer.Def (
   ASTDef (..),
   DefMap,
@@ -367,20 +368,26 @@ forTypeDef l Editable tydefs defs tdName td =
         )
 
 forTypeDefParamNode ::
+  TyVarName ->
   Level ->
   Editable ->
   TypeDefMap ->
   DefMap ->
   TyConName ->
   ASTTypeDef TypeMeta ->
   [Action]
-forTypeDefParamNode _ NonEditable _ _ _ _ = mempty
-forTypeDefParamNode l Editable tydefs defs tdName td =
+forTypeDefParamNode _ _ NonEditable _ _ _ _ = mempty
+forTypeDefParamNode paramName l Editable tydefs defs tdName td =
   sortByPriority l $
     [ Input RenameTypeParam
     ]
       <> mwhen
-        (l == Expert && not (typeInUse tdName td tydefs defs))
+        ( l == Expert
+            && not
+              ( typeInUse tdName td tydefs defs
+                  || any (elem paramName . freeVarsTy) (concatMap valConArgs $ astTypeDefConstructors td)
+              )
+        )
         [NoInput DeleteTypeParam]
 
 forTypeDefConsNode ::

primer/src/Primer/Action/Errors.hs

@@ -13,7 +13,7 @@ import Data.Aeson (FromJSON (..), ToJSON (..))
 import Primer.Action.Actions (Action)
 import Primer.Action.Available qualified as Available
 import Primer.Action.Movement (Movement)
-import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, Pattern, TyConName, Type, Type', ValConName)
+import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, Pattern, TyConName, Type', ValConName)
 import Primer.JSON (CustomJSON (..), PrimerJSON)
 import Primer.Typecheck.TypeError (TypeError)
 import Primer.Zipper (SomeNode)
@@ -62,7 +62,7 @@ data ActionError
     -- The extra unit is to avoid having two constructors with a single
     -- TypeError field, breaking our MonadNestedError machinery...
     ImportFailed () TypeError
-  | NeedTFun Type
+  | NeedTFun (Type' ())
   | NeedType SomeNode
   | NeedGlobal Available.Option
   | NeedLocal Available.Option
@@ -78,5 +78,6 @@ data ActionError
   | NeedTypeDefParamSelection
   | NoNodeSelection
   | ValConNotFound TyConName ValConName
+  | FieldIndexOutOfBounds ValConName Int
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON ActionError