Skip to content

Commit

Permalink
Demote the panic that arises from bare type applications
Browse files Browse the repository at this point in the history
to a kind-checking error.  This at least provides actionable
feedback about where the error occurs.

We should also improve the parser post-processing pass to
handle these situations better, but this at least removes
the panic.
  • Loading branch information
robdockins committed Feb 10, 2021
1 parent b2fbb01 commit 19630f8
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 2 deletions.
10 changes: 10 additions & 0 deletions src/Cryptol/TypeCheck/Error.hs
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,9 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
-- but we know it must be at least as large as the given type
-- (or unconstrained, if Nothing).

| BareTypeApp
-- ^ Bare expression of the form `{_}

| UndefinedExistVar Name
| TypeShadowing String Name String
| MissingModTParam (Located Ident)
Expand All @@ -139,6 +142,7 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
errorImportance :: Error -> Int
errorImportance err =
case err of
BareTypeApp{} -> 11 -- basically a parse error
KindMismatch {} -> 10
TyVarWithParams {} -> 9
TypeMismatch {} -> 8
Expand Down Expand Up @@ -180,6 +184,7 @@ errorImportance err =




instance TVars Warning where
apSubst su warn =
case warn of
Expand Down Expand Up @@ -219,6 +224,7 @@ instance TVars Error where
RepeatedTypeParameter {} -> err
AmbiguousSize x t -> AmbiguousSize x !$ (apSubst su t)

BareTypeApp{} -> err

UndefinedExistVar {} -> err
TypeShadowing {} -> err
Expand Down Expand Up @@ -250,6 +256,8 @@ instance FVS Error where
RepeatedTypeParameter {} -> Set.empty
AmbiguousSize _ t -> fvs t

BareTypeApp{} -> Set.empty

UndefinedExistVar {} -> Set.empty
TypeShadowing {} -> Set.empty
MissingModTParam {} -> Set.empty
Expand Down Expand Up @@ -403,6 +411,8 @@ instance PP (WithNames Error) where
Nothing -> empty
in addTVarsDescsAfter names err ("Ambiguous numeric type:" <+> pp (tvarDesc x) $$ sizeMsg)

BareTypeApp -> "Unexpected bare type application"

UndefinedExistVar x -> "Undefined type" <+> quotes (pp x)
TypeShadowing this new that ->
"Type" <+> text this <+> quotes (pp new) <+>
Expand Down
4 changes: 2 additions & 2 deletions src/Cryptol/TypeCheck/Kind.hs
Original file line number Diff line number Diff line change
Expand Up @@ -387,8 +387,8 @@ doCheckType ty k =

P.TInfix t x _ u-> doCheckType (P.TUser (thing x) [t, u]) k

P.TTyApp _fs -> panic "doCheckType"
["TTyApp found when kind checking, but it should have been eliminated already"]
P.TTyApp _fs -> do kRecordError BareTypeApp
kNewType TypeWildCard KNum

where
checkF _nm (rng,v) = kInRange rng $ doCheckType v (Just KType)
Expand Down

0 comments on commit 19630f8

Please sign in to comment.