feat: ConstructKType needs a hole (#1135)

hackworthltd · Sep 11, 2023 · 4ea7a18 · 4ea7a18 · github-actions · Sep 11, 2023
2 parents b74d29b + d8c5102
commit 4ea7a18
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
@@ -1004,7 +1004,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"
@@ -1031,6 +1031,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
Benchmark suite	Current: `4ea7a18`	Previous: `b74d29b`	Ratio
`evalTestM/discard logs/mapEven 1: outlier variance`	`0.16094741256692316` outlier variance	`0.02324263038548748` outlier variance	`6.92`
`typecheck/mapOdd 10: outlier variance`	`0.17493026139283516` outlier variance	`0.01492194674012856` outlier variance	`11.72`
`typecheck/mapOddPrim 1: outlier variance`	`0.5798705255991006` outlier variance	`0.012343749999999999` outlier variance	`46.98`