Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More typechecking error message improvements #1308

Merged
merged 17 commits into from
Jun 10, 2023
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
update some comments
  • Loading branch information
byorgey committed Jun 8, 2023
commit f5a9944bb41482fa989b84754d3a543378db4d78
28 changes: 15 additions & 13 deletions src/Swarm/Language/Typecheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -265,11 +265,8 @@ noSkolems l (Forall xs upty) = do
infix 4 =:=

-- | @unify t expTy actTy@ ensures that the given two types are equal.
-- The first type is the expected type (passed down from the
-- context) whereas the second is the actual type (extracted from a
-- term). If we know the actual term @t@ which is supposed to have
-- these types, we can use it to generate better error
-- messages.
-- If we know the actual term @t@ which is supposed to have these
-- types, we can use it to generate better error messages.
--
-- We first do a quick-and-dirty check to see whether we know for
-- sure the types either are or cannot be equal, generating an
Expand Down Expand Up @@ -363,10 +360,7 @@ generalize uty = do
-- Type errors

-- | A type error along with various contextual information to help us
-- generate better error messages. For now there is only a SrcLoc
-- but there will be additional context in the future, such as a
-- stack of stuff we were in the middle of doing, relevant names in
-- scope, etc. (#1297).
-- generate better error messages.
data ContextualTypeErr = CTE {cteSrcLoc :: SrcLoc, cteStack :: TCStack, cteTypeErr :: TypeErr}
deriving (Show)

Expand Down Expand Up @@ -443,23 +437,29 @@ instance Fallible TypeF IntVar ContextualTypeErr where
------------------------------------------------------------
-- Type decomposition

-- | Decompose a type that is supposed to be a delay type.
-- | Decompose a type that is supposed to be a delay type. Also take
-- the term which is supposed to have that type, for use in error
-- messages.
decomposeDelayTy :: Syntax -> Sourced UType -> TC UType
decomposeDelayTy _ (_, UTyDelay a) = return a
decomposeDelayTy t ty = do
a <- fresh
_ <- unify (Just t) (mkJoin ty (UTyDelay a))
return a

-- | Decompose a type that is supposed to be a command type.
-- | Decompose a type that is supposed to be a command type. Also take
-- the term which is supposed to have that type, for use in error
-- messages.
decomposeCmdTy :: Syntax -> Sourced UType -> TC UType
decomposeCmdTy _ (_, UTyCmd a) = return a
decomposeCmdTy t ty = do
a <- fresh
_ <- unify (Just t) (mkJoin ty (UTyCmd a))
return a

-- | Decompose a type that is supposed to be a function type.
-- | Decompose a type that is supposed to be a function type. Also take
-- the term which is supposed to have that type, for use in error
-- messages.
decomposeFunTy :: Syntax -> Sourced UType -> TC (UType, UType)
decomposeFunTy _ (_, UTyFun ty1 ty2) = return (ty1, ty2)
decomposeFunTy t ty = do
Expand All @@ -468,7 +468,9 @@ decomposeFunTy t ty = do
_ <- unify (Just t) (mkJoin ty (UTyFun ty1 ty2))
return (ty1, ty2)

-- | Decompose a type that is supposed to be a product type.
-- | Decompose a type that is supposed to be a product type. Also take
-- the term which is supposed to have that type, for use in error
-- messages.
decomposeProdTy :: Syntax -> Sourced UType -> TC (UType, UType)
decomposeProdTy _ (_, UTyProd ty1 ty2) = return (ty1, ty2)
decomposeProdTy t ty = do
Expand Down