Skip to content

Commit

Permalink
better reporting of kinds/types of holes TODO: term-level (empty/none…
Browse files Browse the repository at this point in the history
…mpty) hole subterm in syn position with a "match" constraint -- App and APP

`List {? Maybe ?}` now reports "expected `*`, got `* -> *`"
`{? Nat ?} Bool` now reports "expected `? -> ?`, got `*`"

Improving the reporting further is left as future work. (For example,
`List ({? Nat ?} Bool)` could report "expected `* -> *`" by noting
`Bool : *` and `List : * -> *`. However, this is starting to veer into
type inference territory, which we have avoided so far.
  • Loading branch information
brprice committed Nov 9, 2023
1 parent ae93fb9 commit 0e99a55
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 13 deletions.
34 changes: 25 additions & 9 deletions primer-api/test/Tests/API.hs
Original file line number Diff line number Diff line change
Expand Up @@ -541,9 +541,13 @@ test_selectioninfo =
pure $ defAST =<< foldMap' moduleDefsQualified (progModules p) M.!? qualifyName scope d
let getExpr d = astDefExpr <<$>> getDef d
let getType d = astDefType <<$>> getDef d
let mkExpr d as = do
let mkExpr d tyAct tmAct = do
_ <- expectSuccess $ edit sid $ Edit [CreateDef scope $ Just $ unName d]
i <-
tyId <-
getType d >>= \case
Just t@TEmptyHole{} -> pure $ getID t
_ -> assertFailure' $ "unexpected form of " <> toS (unName d)
tmId <-
getExpr d >>= \case
Just e@EmptyHole{} -> pure $ getID e
_ -> assertFailure' $ "unexpected form of " <> toS (unName d)
Expand All @@ -552,7 +556,8 @@ test_selectioninfo =
$ edit sid
$ Edit
[ MoveToDef $ qualifyName scope d
, BodyAction $ SetCursor i : as
, SigAction $ SetCursor tyId : tyAct
, BodyAction $ SetCursor tmId : tmAct
]
pure ()
let mkType d as = do
Expand All @@ -571,7 +576,7 @@ test_selectioninfo =
pure ()

step "tm1 :: ? = not {? Zero ?}"
mkExpr "tm1" [ConstructApp, Move Child1
mkExpr "tm1" [] [ConstructApp, Move Child1
, ConstructVar $ GlobalVarRef PL.not
, Move Parent, Move Child2
, constructSaturatedCon cZero
Expand All @@ -588,8 +593,10 @@ test_selectioninfo =
zeroTKIds tm1tk @?= zeroTKIds (Type $ Mismatch {got = viewTreeType $ create' $ tcon tNat
, expected = viewTreeType $ create' $ tcon tBool})

step "tm2 :: ? = {? Zero ?} True"
mkExpr "tm2" [ConstructApp, Move Child1
step "tm2 :: Maybe Nat = {? Zero ?} True"
mkExpr "tm2" [ConstructTApp
, Move Child1, constructTCon tMaybe
, Move Parent, Move Child2, constructTCon tNat ] [ConstructApp, Move Child1
, EnterHole, constructSaturatedCon cZero
, Move Parent, Move Parent, Move Child2
, constructSaturatedCon cTrue
Expand All @@ -604,7 +611,12 @@ test_selectioninfo =
tm2tk <- getSelectionTypeOrKind sid $ SelectionDef $ DefSelection (qualifyName scope "tm2")
$ Just $ NodeSelection BodyNode htm2
zeroTKIds tm2tk @?= zeroTKIds (Type $ Mismatch {got = viewTreeType $ create' $ tcon tNat
, expected = viewTreeType $ create' tEmptyHole}) -- TODO: do we want ? or ? -> ?
-- We require @expected@ to be an empty hole, matching
-- the behaviour of @? True@
-- Arguably we should change both this and the empty hole case to
-- expose that we expect @Bool -> Maybe Nat@, see
-- https://github.com/hackworthltd/primer/issues/81
, expected = viewTreeType $ create' tEmptyHole})

step "ty1 :: List {? Maybe ?} = ?"
mkType "ty1" [ConstructTApp, Move Child1
Expand All @@ -622,7 +634,7 @@ test_selectioninfo =
ty1tk <- getSelectionTypeOrKind sid $ SelectionDef $ DefSelection (qualifyName scope "ty1")
$ Just $ NodeSelection SigNode hty1
zeroTKIds ty1tk @?= zeroTKIds (Kind $ Mismatch {got = viewTreeKind $ create' $ ktype `kfun` ktype
, expected = viewTreeKind $ create' khole}) -- TODO: do we want ? or *
, expected = viewTreeKind $ create' ktype})

step "ty2 :: {? Nat ?} Bool = ?"
mkType "ty2" [ConstructTApp, Move Child1
Expand All @@ -640,7 +652,11 @@ test_selectioninfo =
ty2tk <- getSelectionTypeOrKind sid $ SelectionDef $ DefSelection (qualifyName scope "ty2")
$ Just $ NodeSelection SigNode hty2
zeroTKIds ty2tk @?= zeroTKIds (Kind $ Mismatch {got = viewTreeKind $ create' ktype
, expected = viewTreeKind $ create' khole}) -- TODO: do we want ? or ? -> *
-- We require @expected@ to be @? -> ?@, matching the behaviour of an empty hole.
-- Arguably we should change both this and the empty hole case to
-- expose that we expect @* -> *@, see
-- https://github.com/hackworthltd/primer/issues/81
, expected = viewTreeKind $ create' $ khole `kfun` khole})

zeroTKIds :: TypeOrKind -> TypeOrKind
zeroTKIds = \case
Expand Down
13 changes: 9 additions & 4 deletions primer/src/Primer/Typecheck/Kindcheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -108,15 +108,20 @@ synthKind = \case
asks (lookupLocalTy v) >>= \case
Right k -> pure (k, TVar (annotate k m) v)
Left err -> throwError' err
TApp ma (TEmptyHole mh) t -> do
-- Same as @TApp _ s t@ except to change the metadata on the hole
-- to have the kind ? -> ?
checkKind (KHole ()) t >>= \t' -> pure (KHole (),
TApp (annotate (KHole ()) ma) (TEmptyHole $ annotate (KFun () (KHole ()) (KHole ())) mh) t')
TApp ma (THole mh s) t -> do
-- If we didn't have this special case, we might remove this hole (in a
-- recursive call), only to reintroduce it again with a different ID
-- TODO: ugly and duplicated...
sh <- asks smartHoles
(k, s') <- synthKind s
case (matchArrowKind k, sh) of
(_, NoSmartHoles) -> checkKind (KHole ()) t >>= \t' -> pure (KHole (), TApp (annotate (KHole ()) ma) (THole (annotate (KHole ()) mh) s') t')
(Nothing, SmartHoles) -> checkKind (KHole ()) t >>= \t' -> pure (KHole (), TApp (annotate (KHole ()) ma) (THole (annotate (KHole ()) mh) s') t')
(_, NoSmartHoles) -> checkKind (KHole ()) t >>= \t' -> pure (KHole (), TApp (annotate (KHole ()) ma) (THole (annotate (KFun () (KHole ()) (KHole ())) mh) s') t')
(Nothing, SmartHoles) -> checkKind (KHole ()) t >>= \t' -> pure (KHole (), TApp (annotate (KHole ()) ma) (THole (annotate (KFun () (KHole ()) (KHole ())) mh) s') t')
(Just (k1, k2), SmartHoles) -> checkKind k1 t >>= \t' -> pure (k2, TApp (annotate k2 ma) s' t')
TApp m s t -> do
sh <- asks smartHoles
Expand All @@ -141,9 +146,9 @@ checkKind k (THole m t) = do
sh <- asks smartHoles
(k', t') <- synthKind t
case (consistentKinds k k', sh) of
(_, NoSmartHoles) -> pure $ THole (annotate (KHole ()) m) t'
(_, NoSmartHoles) -> pure $ THole (annotate k m) t'
(True, SmartHoles) -> pure t'
(False, SmartHoles) -> pure $ THole (annotate (KHole ()) m) t'
(False, SmartHoles) -> pure $ THole (annotate k m) t'
checkKind k t = do
sh <- asks smartHoles
(k', t') <- synthKind t
Expand Down

0 comments on commit 0e99a55

Please sign in to comment.