feat: ConstructKType needs a hole

For consistency with other actions, we require creating a KType to take place in a (kind) hole. Signed-off-by: Ben Price <[email protected]>
hackworthltd · Sep 6, 2023 · d8c5102 · d8c5102
1 parent 91dee13
commit d8c5102
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 3 deletions.
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
@@ -1005,7 +1005,7 @@ applyProgAction prog = \case
                 ( traverseOf _2 $
                     flip
                       ( foldlM $ flip \case
-                          ConstructKType -> modifyKind $ const ktype
+                          ConstructKType -> modifyKind $ replaceHole ConstructKType ktype
                           ConstructKFun -> modifyKind \k -> ktype `kfun` pure k
                           Delete -> modifyKind $ const khole
                           a -> const $ throwError $ ActionError $ CustomFailure a "unexpected non-kind action"
@@ -1032,6 +1032,9 @@ applyProgAction prog = \case
             KHole _ -> pure k
             KType _ -> pure k
             KFun m k1 k2 -> KFun m <$> modifyKind f k1 <*> modifyKind f k2
+      replaceHole a r = \case
+        KHole{} -> r
+        _ -> throwError' $ CustomFailure a "can only construct this kind in a hole"
   SetSmartHoles smartHoles ->
     pure $ prog & #progSmartHoles .~ smartHoles
   CopyPasteSig fromIds setup -> case mdefName of

diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
@@ -26,7 +26,7 @@ import Primer.Action (
     Move,
     RemoveAnn
   ),
-  ActionError (ImportNameClash),
+  ActionError (CustomFailure, ImportNameClash),
   BranchMove (Pattern),
   Movement (
     Branch,
@@ -1200,12 +1200,22 @@ unit_ParamKindAction_2 =
     [ ParamKindAction tT pB 30 [ConstructKFun]
     , ParamKindAction tT pB 5 [ConstructKType]
     ]
+    $ expectError (@?= ActionError (CustomFailure ConstructKType "can only construct this kind in a hole"))
+
+unit_ParamKindAction_2b :: Assertion
+unit_ParamKindAction_2b =
+  progActionTest
+    ( defaultProgEditableTypeDefs (pure [])
+    )
+    [ ParamKindAction tT pB 30 [ConstructKFun]
+    , ParamKindAction tT pB 5 [Delete]
+    ]
     $ expectSuccess
     $ \_ prog' -> do
       td <- findTypeDef tT prog'
       astTypeDefParameters td
         @?= [ ("a", KType ())
-            , ("b", KFun () (KType ()) (KType ()))
+            , ("b", KFun () (KHole ()) (KType ()))
             ]
 
 unit_ParamKindAction_3 :: Assertion