Fixed the type checker accidentally chucking cases in some cases.

This commit is contained in:
Samuel Hammersberg 2023-02-20 16:43:54 +01:00
parent cd0f9dd456
commit afbc700db2

View file

@ -154,6 +154,20 @@ check cxt exp typ = case exp of
unless (typeEq t1 typ) $ throwError "Wrong lamda type!"
pure $ T.EAbs t1 (x, t) e'
ECase e cs t -> do
(e',t1) <- infer cxt e
unless (typeEq t t1) $
throwError "Inferred type and type annotation doesn't match"
case traverse (\(CaseMatch c e) -> do
-- //TODO check c as well
e' <- check cxt e t
unless (typeEq t t1) $
throwError "Inferred type and type annotation doesn't match"
pure (t1, T.Case c e')
) cs of
Right cs -> pure $ T.ECase t1 e' cs
Left e -> throwError e
ELet b e -> do
let cxt' = insertBind b cxt
b' <- checkBind cxt' b
@ -165,11 +179,6 @@ check cxt exp typ = case exp of
throwError "Inferred type and type annotation doesn't match"
check cxt e t
ECase e _ t -> do
unless (typeEq t typ) $
throwError "Inferred type and type annotation doesn't match"
check cxt e t
-- | Check if types are equivalent. Doesn't handle coercion or polymorphism.
typeEq :: Type -> Type -> Bool
typeEq (TFun t t1) (TFun q q1) = typeEq t q && typeEq t1 q1