github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-11-28 18:23:44 +03:00
Code Issues Projects Releases Wiki Activity

add separate InfiniteType constructor to TypeError

Browse Source
This commit is contained in:
Charlie Somerville 2018-07-05 22:56:48 +10:00
parent fa00126ab6
commit b819ff8a3b
1 changed files with 17 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/Data/Abstract/Type.hs
View File

@ -60,13 +60,23 @@ zeroOrMoreProduct = maybe Unit oneOrMoreProduct . nonEmpty
-- | Errors representing failures in typechecking. Note that we should in general constrain allowable types by 'unify'ing, and thus throwing 'UnificationError's when constraints aren’t met, in order to allow uniform resumption with one or the other parameter type.
data TypeError resume where
UnificationError :: Type -> Type -> TypeError Type
InfiniteType :: Type -> Type -> TypeError Type
deriving instance Eq (TypeError resume)
deriving instance Ord (TypeError resume)
deriving instance Show (TypeError resume)
instance Eq1 TypeError where liftEq _ (UnificationError a1 b1) (UnificationError a2 b2) = a1 == a2 && b1 == b2
instance Ord1 TypeError where liftCompare _ (UnificationError a1 b1) (UnificationError a2 b2) = compare a1 a2 <> compare b1 b2
instance Eq1 TypeError where
liftEq _ (UnificationError a1 b1) (UnificationError a2 b2) = a1 == a2 && b1 == b2
liftEq _ (InfiniteType a1 b1) (InfiniteType a2 b2) = a1 == a2 && b1 == b2
liftEq _ _ _ = False
instance Ord1 TypeError where
liftCompare _ (UnificationError a1 b1) (UnificationError a2 b2) = compare a1 a2 <> compare b1 b2
liftCompare _ (InfiniteType a1 b1) (InfiniteType a2 b2) = compare a1 a2 <> compare b1 b2
liftCompare _ (InfiniteType _ _) (UnificationError _ _) = LT
liftCompare _ (UnificationError _ _) (InfiniteType _ _) = GT
instance Show1 TypeError where liftShowsPrec _ _ = showsPrec
runTypeError :: Effectful m => m (Resumable TypeError ': effects) a -> m effects (Either (SomeExc TypeError) a)
@ -162,9 +172,11 @@ substitute :: ( Effectful m
-> m effects Type
substitute id ty = do
infiniteType <- occur id ty
if infiniteType
then throwResumable (UnificationError (Var id) ty)
else modifyTypeMap (Map.insert id ty) $> ty
ty <- if infiniteType
then throwResumable (InfiniteType (Var id) ty)
else pure ty
modifyTypeMap (Map.insert id ty)
pure ty
-- | Unify two 'Type's.
unify :: ( Effectful m