rewrote unification for data type and variable.

could definitely be wrong. have to double check
This commit is contained in:
sebastianselander 2023-03-24 18:48:40 +01:00
parent e500c70529
commit b08ae7aef1
3 changed files with 19 additions and 7 deletions

View file

@ -83,7 +83,7 @@ checkPrg :: Program -> Infer T.Program
checkPrg (Program bs) = do
preRun bs
-- Type check the program twice to produce all top-level types in the first pass through
bs' <- checkDef bs
_ <- checkDef bs
bs'' <- checkDef bs
return $ T.Program bs''
where
@ -132,7 +132,7 @@ checkBind err@(Bind name args e) = do
return $ T.Bind (apply sub (coerce name, newT)) (map coerce args) e
_ -> do
insertSig (coerce name) (Just lambdaT)
return (T.Bind (coerce name, lambdaT) (map coerce args) e) -- (apply s e)
return (T.Bind (coerce name, lambdaT) (map coerce args) e)
isMoreSpecificOrEq :: T.Type -> T.Type -> Bool
isMoreSpecificOrEq _ (T.TAll _ _) = True
@ -321,6 +321,9 @@ unify t0 t1 = do
s1 <- unify a c
s2 <- unify (apply s1 b) (apply s1 d)
return $ s1 `compose` s2
-- TODO: BEWARY. THIS IS PROBABLY WRONG!!!
(T.TVar (T.MkTVar a), t@(T.TData _ _)) -> return $ M.singleton a t
(t@(T.TData _ _), T.TVar (T.MkTVar b)) -> return $ M.singleton b t
(T.TVar (T.MkTVar a), t) -> occurs a t
(t, T.TVar (T.MkTVar b)) -> occurs b t
(T.TAll _ t, b) -> unify t b

View file

@ -7,6 +7,7 @@ module TypeChecker.TypeCheckerIr (
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.Char (isDigit)
import Data.Functor.Identity (Identity)
import Data.Map (Map)
import Data.String qualified
@ -227,7 +228,10 @@ instance Print TVar where
instance Print Type where
prt i = \case
TLit uident -> prPrec i 2 (concatD [prt 0 uident])
TVar tvar -> prPrec i 2 (concatD [prt 0 tvar])
TVar tvar@(MkTVar (Ident iden)) ->
if all isDigit iden
then prPrec i 2 (concatD [prt 0 $ TVar (MkTVar (Ident ("a" <> iden)))])
else prPrec i 2 (concatD [prt 0 tvar])
TAll tvar type_ -> prPrec i 1 (concatD [doc (showString "forall"), prt 0 tvar, doc (showString "."), prt 0 type_])
TData ident types -> prPrec i 1 (concatD [prt 0 ident, prt 0 types])
TFun type_1 type_2 -> prPrec i 0 (concatD [prt 1 type_1, doc (showString "->"), prt 0 type_2])

View file

@ -35,7 +35,12 @@ data List (a) where {
-- main = firstIsOne (Cons 1 Nil);
test xs = case xs of {
1 => 0;
lol => 1;
};
-- test xs = case xs of {
-- 1 => 0;
-- lol => 1;
-- };
deepList xs = case xs of {
Cons Nil _ => 1 ;
_ => 0 ;
};