ref: 643636103de5138fbabd8513e7fec538a456d799
parent: f3c83a1c968467d1be14499be5131a7568c82723
author: Lennart Augustsson <lennart@augustsson.net>
date: Tue Oct 10 19:45:13 EDT 2023
Redo unification and add occurs check.
--- a/TODO
+++ b/TODO
@@ -25,8 +25,6 @@
- allow missing top level signatures (and generalize)
- instead of skolemization, use regular variables, making sure they are unique
- allow existential quantification
-* Add occurrence check
-* Fix bug in type variable expansion for unification
* Try Oleg's abstraction algorithm
* Generate (compressed) combinators in a separate file for compilation
- Distribute this file instead of .comb file
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v3.5
-970
-(($A :0 _854) (($A :1 (($B _900) _0)) (($A :2 ((($S' _900) _0) $I)) (($A :3 _824) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _853) (($C _74) _5))) (($A :7 ((($C' _6) (_871 _71)) ((_74 _869) _70))) (($A :8 (($B (($S _900) _869)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_74 _188)) _10)) (($A :12 (($B ($B (_73 _9))) ((($C' $B) (($B $C) _10)) ($B _10)))) (($A :13 (($B ($B (_73 _9))) ((($C' $B) (($B $C) _10)) ($BK _10)))) (($A :14 (($B (_73 _9)) $P)) (($A :15 (($B ($B (_73 _9))) (($B (($C' $C) _10)) ($B $P)))) (($A :16 _15) (($A :17 (($B (_73 _9)) ($B ($P _782)))) (($A :18 (($B (_73 _9)) ($BK ($P _782)))) (($A :19 ((_73 _9) (($S $P) $I))) (($A :20 (($B (_73 _9)) (($C ($S' $P)) $I))) (($A :21 (($B $Y) (($B ($B ($P (_14 _114)))) ((($C' $B) (($B ($C' $B)) ($B _12))) ((($C' ($C' $B)) ($B _12)) (($B ($B _14)) _115)))))) (($A :22 (($B $Y) (($B ($B ($P (_14 _782)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _782))) (($A :25 (_21 _75)) (($A :26 (($C $C) _33)) (($A :27 ($T _32)) (($A :28 (($P _33) _32)) (($A :29 _33) (($A :30 (($C (($C $S') _28)) $I)) (($A :31 (($C $S) _28)) (($A :32 $K) (($A :33 $A) (($A :34 _829) (($A :35 _830) (($A :36 ((($S' _27) (_821 97)) (($C _821) 122))) (($A :37 ((($S' _27) (_821 65)) (($C _821) 90))) (($A :38 ((($S' _26) _36) _37)) (($A :39 ((($S' _27) (_821 48)) (($C _821) 57))) (($A :40 ((($S' _27) (_821 32)) (($C _821) 126))) (($A :41 _818) (($A :42 _819) (($A :43 _821) (($A :44 _820) (($A :45 ((($S' _26) (($C _41) 32)) ((($S' _26) (($C _41) 9)) (($C _41) 10)))) (($A :46 (($S (($S ((($S' _27) (_43 65)) (($C _43) 90))) (_33 (((_781 "lib/Data/Char.hs") 3) 8)))) (($B _34) ((($C' _81) ((($C' _82) _35) (_35 65))) (_35 97))))) (($A :47 (($S (($S ((($S' _27) (_43 97)) (($C _43) 97))) (_33 (((_781 "lib/Data/Char.hs") 3) 8)))) (($B _34) ((($C' _81) ((($C' _82) _35) (_35 97))) (_35 65))))) (($A :48 _789) (($A :49 _790) (($A :50 _791) (($A :51 _792) (($A :52 (_49 %0.0)) (($A :53 _48) (($A :54 _49) (($A :55 _50) (($A :56 _51) (($A :57 _793) (($A :58 _794) (($A :59 _57) (($A :60 _58) (($A :61 _795) (($A :62 _796) (($A :63 _797) (($A :64 _798) (($A :65 _61) (($A :66 _62) (($A :67 _63) (($A :68 _64) (($A :69 _799) (($A :70 (($B $BK) $T)) (($A :71 ($BK $T)) (($A :72 $P) (($A :73 $I) (($A :74 $B) (($A :75 $I) (($A :76 $K) (($A :77 $C) (($A :78 _825) (($A :79 (($C (($C $S') _188)) _189)) (($A :80 ((($C' ($S' ($C' $B))) $B) $I)) (($A :81 _783) (($A :82 _784) (($A :83 _785) (($A :84 _786) (($A :85 _787) (($A :86 _788) (($A :87 (_82 0)) (($A :88 _806) (($A :89 _807) (($A :90 _808) (($A :91 _809) (($A :92 _810) (($A :93 _811) (($A :94 _88) (($A :95 ($BK $K)) (($A :96 (($B $BK) (($B ($B $BK)) $P))) (($A :97 (($B ($B ($B $BK))) (($B ($B ($B $BK))) (($B ($B ($B $C))) (($B ($B $C)) $P))))) (($A :98 ((($S' $S) ((($S' ($S' $C)) ((($C' ($C' $S)) ((($C' $B) (($B ($S' $S')) ((($C' $B) (($B _26) (_91 0))) (_88 0)))) (($B ($B (($C' $P) (_86 1)))) _81))) ($C $P))) _84)) _85)) (($A :99 _95) (($A :100 ((($S' $C) (($B ($P _176)) ((($C' ($C' $B)) ((($C' $C) _88) _176)) _177))) (($B (($C' ($C' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) (($B (($C' ($C' ($C' $C))) (($B ($B ($B (($S' $S') (_88 0))))) (($B (($C' ($C' $C)) (($B ($B (($S' $S') (_88 1)))) (($B (($C' $C) (($B (($C' $S') (_88 2))) ($C _100)))) ($C _100))))) ($C _100))))) ($C _100)))) ($T $K))) ($T $A)))) (($C _98) 4)))) (($A :101 (_107 _76)) (($A :102 ((_122 (_79 _101)) _99)) (($A :103 (($C ((($C' $B) (($P _114) ((($C' ($C' $O)) $P) $K))) ((($S' ($C' ($C' ($C' $B)))) (($B ($B ($B ($B _104)))) ((($S' ($C' ($C' $B))) (($B ($B ($B _104))) ((($S' ($C' $B)) (($B ($B _104)) ((($C' $B) (($B _120) ($T 0))) _103))) ((($C' $B) (($B _120) ($T 1))) _103)))) ((($C' $B) (($B _120) ($T 2))) _103)))) ((($C' $B) (($B _120) ($T 3))) _103)))) (($B $T) (($B ($B $P)) (($C' _81) (_83 4)))))) (($A :104 (($S $S) (($B $BK) (($B $BK) ((($S' $S) $T) (($B $BK) (($B $BK) (($C ((($S' $C') $S) (($B ($B ($B ($S $B)))) (($B ($B ($B ($B ($B $BK))))) (($B (($S' ($C' $B)) (($B $B') $B'))) (($B ($B ($B ($B ($B ($S $B)))))) (($B ($B ($B (
\ No newline at end of file
+973
+(($A :0 _857) (($A :1 (($B _903) _0)) (($A :2 ((($S' _903) _0) $I)) (($A :3 _827) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _856) (($C _74) _5))) (($A :7 ((($C' _6) (_874 _71)) ((_74 _872) _70))) (($A :8 (($B (($S _903) _872)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_74 _188)) _10)) (($A :12 (($B ($B (_73 _9))) ((($C' $B) (($B $C) _10)) ($B _10)))) (($A :13 (($B ($B (_73 _9))) ((($C' $B) (($B $C) _10)) ($BK _10)))) (($A :14 (($B (_73 _9)) $P)) (($A :15 (($B ($B (_73 _9))) (($B (($C' $C) _10)) ($B $P)))) (($A :16 _15) (($A :17 (($B (_73 _9)) ($B ($P _785)))) (($A :18 (($B (_73 _9)) ($BK ($P _785)))) (($A :19 ((_73 _9) (($S $P) $I))) (($A :20 (($B (_73 _9)) (($C ($S' $P)) $I))) (($A :21 (($B $Y) (($B ($B ($P (_14 _114)))) ((($C' $B) (($B ($C' $B)) ($B _12))) ((($C' ($C' $B)) ($B _12)) (($B ($B _14)) _115)))))) (($A :22 (($B $Y) (($B ($B ($P (_14 _785)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _785))) (($A :25 (_21 _75)) (($A :26 (($C $C) _33)) (($A :27 ($T _32)) (($A :28 (($P _33) _32)) (($A :29 _33) (($A :30 (($C (($C $S') _28)) $I)) (($A :31 (($C $S) _28)) (($A :32 $K) (($A :33 $A) (($A :34 _832) (($A :35 _833) (($A :36 ((($S' _27) (_824 97)) (($C _824) 122))) (($A :37 ((($S' _27) (_824 65)) (($C _824) 90))) (($A :38 ((($S' _26) _36) _37)) (($A :39 ((($S' _27) (_824 48)) (($C _824) 57))) (($A :40 ((($S' _27) (_824 32)) (($C _824) 126))) (($A :41 _821) (($A :42 _822) (($A :43 _824) (($A :44 _823) (($A :45 ((($S' _26) (($C _41) 32)) ((($S' _26) (($C _41) 9)) (($C _41) 10)))) (($A :46 (($S (($S ((($S' _27) (_43 65)) (($C _43) 90))) (_33 (((_784 "lib/Data/Char.hs") 3) 8)))) (($B _34) ((($C' _81) ((($C' _82) _35) (_35 65))) (_35 97))))) (($A :47 (($S (($S ((($S' _27) (_43 97)) (($C _43) 97))) (_33 (((_784 "lib/Data/Char.hs") 3) 8)))) (($B _34) ((($C' _81) ((($C' _82) _35) (_35 97))) (_35 65))))) (($A :48 _792) (($A :49 _793) (($A :50 _794) (($A :51 _795) (($A :52 (_49 %0.0)) (($A :53 _48) (($A :54 _49) (($A :55 _50) (($A :56 _51) (($A :57 _796) (($A :58 _797) (($A :59 _57) (($A :60 _58) (($A :61 _798) (($A :62 _799) (($A :63 _800) (($A :64 _801) (($A :65 _61) (($A :66 _62) (($A :67 _63) (($A :68 _64) (($A :69 _802) (($A :70 (($B $BK) $T)) (($A :71 ($BK $T)) (($A :72 $P) (($A :73 $I) (($A :74 $B) (($A :75 $I) (($A :76 $K) (($A :77 $C) (($A :78 _828) (($A :79 (($C (($C $S') _188)) _189)) (($A :80 ((($C' ($S' ($C' $B))) $B) $I)) (($A :81 _786) (($A :82 _787) (($A :83 _788) (($A :84 _789) (($A :85 _790) (($A :86 _791) (($A :87 (_82 0)) (($A :88 _809) (($A :89 _810) (($A :90 _811) (($A :91 _812) (($A :92 _813) (($A :93 _814) (($A :94 _88) (($A :95 ($BK $K)) (($A :96 (($B $BK) (($B ($B $BK)) $P))) (($A :97 (($B ($B ($B $BK))) (($B ($B ($B $BK))) (($B ($B ($B $C))) (($B ($B $C)) $P))))) (($A :98 ((($S' $S) ((($S' ($S' $C)) ((($C' ($C' $S)) ((($C' $B) (($B ($S' $S')) ((($C' $B) (($B _26) (_91 0))) (_88 0)))) (($B ($B (($C' $P) (_86 1)))) _81))) ($C $P))) _84)) _85)) (($A :99 _95) (($A :100 ((($S' $C) (($B ($P _176)) ((($C' ($C' $B)) ((($C' $C) _88) _176)) _177))) (($B (($C' ($C' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) (($B (($C' ($C' ($C' $C))) (($B ($B ($B (($S' $S') (_88 0))))) (($B (($C' ($C' $C)) (($B ($B (($S' $S') (_88 1)))) (($B (($C' $C) (($B (($C' $S') (_88 2))) ($C _100)))) ($C _100))))) ($C _100))))) ($C _100)))) ($T $K))) ($T $A)))) (($C _98) 4)))) (($A :101 (_107 _76)) (($A :102 ((_122 (_79 _101)) _99)) (($A :103 (($C ((($C' $B) (($P _114) ((($C' ($C' $O)) $P) $K))) ((($S' ($C' ($C' ($C' $B)))) (($B ($B ($B ($B _104)))) ((($S' ($C' ($C' $B))) (($B ($B ($B _104))) ((($S' ($C' $B)) (($B ($B _104)) ((($C' $B) (($B _120) ($T 0))) _103))) ((($C' $B) (($B _120) ($T 1))) _103)))) ((($C' $B) (($B _120) ($T 2))) _103)))) ((($C' $B) (($B _120) ($T 3))) _103)))) (($B $T) (($B ($B $P)) (($C' _81) (_83 4)))))) (($A :104 (($S $S) (($B $BK) (($B $BK) ((($S' $S) $T) (($B $BK) (($B $BK) (($C ((($S' $C') $S) (($B ($B ($B ($S $B)))) (($B ($B ($B ($B ($B $BK))))) (($B (($S' ($C' $B)) (($B $B') $B'))) (($B ($B ($B ($B ($B ($S $B)))))) (($B ($B ($B (
\ No newline at end of file
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -414,15 +414,10 @@
loop _ _ = Nothing
-}
-addUVar :: Int -> EType -> T ()
-addUVar i t = T.do
- let
- add = T.do
- TC mn n fx tenv senv venv sub m <- get
- put (TC mn n fx tenv senv venv (IM.insert i t sub) m)
- case t of
- EUVar j -> if i == j then T.return () else add
- _ -> add
+setUVar :: TRef -> EType -> T ()
+setUVar i t = T.do
+ TC mn n fx tenv senv venv sub m <- get
+ put (TC mn n fx tenv senv venv (IM.insert i t sub) m)
getUVar :: Int -> T (Maybe EType)
getUVar i = gets (IM.lookup i . uvarSubst)
@@ -432,12 +427,6 @@
munify _ (Infer r) b = tSetRefType r b
munify loc (Check a) b = unify loc a b
-expandType :: --XHasCallStack =>
- EType -> T EType
-expandType at = T.do
- tt <- derefUVar at
- expandSyn tt
-
expandSyn :: --XHasCallStack =>
EType -> T EType
expandSyn at =
@@ -474,7 +463,7 @@
Nothing -> T.return at
Just t -> T.do
t' <- derefUVar t
- addUVar i t'
+ setUVar i t'
T.return t'
EVar _ -> T.return at
ESign t k -> flip ESign k <$> derefUVar t
@@ -484,6 +473,48 @@
unify :: --XHasCallStack =>
SLoc -> EType -> EType -> T ()
unify loc a b = T.do
+ aa <- expandSyn a
+ bb <- expandSyn b
+ unifyR loc aa bb
+
+-- XXX should do occur check
+unifyR :: --XHasCallStack =>
+ SLoc -> EType -> EType -> T ()
+unifyR _ (EVar x1) (EVar x2) | eqIdent x1 x2 = T.return ()
+unifyR loc (EApp f1 a1) (EApp f2 a2) = T.do { unifyR loc f1 f2; unifyR loc a1 a2 }+unifyR _ (EUVar r1) (EUVar r2) | r1 == r2 = T.return ()
+unifyR loc (EUVar r1) t2 = unifyVar loc r1 t2
+unifyR loc t1 (EUVar r2) = unifyVar loc r2 t1
+unifyR loc t1 t2 =
+ tcError loc $ "Cannot unify " ++ showExpr t1 ++ " and " ++ showExpr t2 ++ "\n"
+
+unifyVar :: --XHasCallStack =>
+ SLoc -> TRef -> EType -> T ()
+unifyVar loc r t = T.do
+ mt <- getUVar r
+ case mt of
+ Nothing -> unifyUnboundVar loc r t
+ Just t' -> unify loc t' t
+
+unifyUnboundVar :: --XHasCallStack =>
+ SLoc -> TRef -> EType -> T ()
+unifyUnboundVar loc r1 at2@(EUVar r2) = T.do
+ -- We know r1 /= r2
+ mt2 <- getUVar r2
+ case mt2 of
+ Nothing -> setUVar r1 at2
+ Just t2 -> unify loc (EUVar r1) t2
+unifyUnboundVar loc r1 t2 = T.do
+ vs <- getMetaTyVars [t2]
+ if elemBy (==) r1 vs then
+ tcError loc $ "Cyclic type"
+ else
+ setUVar r1 t2
+
+{-+unify :: --XHasCallStack =>
+ SLoc -> EType -> EType -> T ()
+unify loc a b = T.do
-- traceM ("unify1 " ++ showExpr a ++ " = " ++ showExpr b)aa <- expandType a
bb <- expandType b
@@ -514,6 +545,7 @@
EUVar i -> addUVar i b
_ -> --Xtrace ("impossible unify 2 " ++ showExpr a ++ " = " ++ showExpr b) $impossible
+-}
{-unMType :: Expected -> T EType
@@ -1311,38 +1343,15 @@
tys' <- T.mapM derefUVar tys
T.return (freeTyVars tys')
-{--getMetaTyVars :: [EType] -> T [MetaTv]
+getMetaTyVars :: [EType] -> T [TRef]
getMetaTyVars tys = T.do
- tys' <- T.mapM zonkType tys
+ tys' <- T.mapM derefUVar tys
T.return (metaTvs tys')
--}
getEnvTypes :: T [EType]
getEnvTypes = gets (map entryType . concat . M.elems . valueTable)
{--zonkType :: EType -> T EType
-zonkType (EForall ns ty) = T.do
- ty' <- zonkType ty
- T.return (EForall ns ty')
-zonkType t@(EVar _) = T.return t
-zonkType t@(EUVar tv) = T.do -- A mutable type variable
- mb_ty <- getUVar tv
- case mb_ty of
- Nothing -> T.return t
- Just ty -> T.do
- ty' <- zonkType ty
- --writeTcRef tv ty' -- "Short out" multiple hops
- addUVar tv ty'
- T.return ty'
-zonkType (EApp arg res) = T.do
- arg' <- zonkType arg
- res' <- zonkType res
- T.return (EApp arg' res')
-zonkType _ = undefined
--}
-{-quantify :: [MetaTv] -> Rho -> T Sigma
-- Quantify over the specified type variables (all flexible)
quantify tvs ty = T.do
@@ -1401,8 +1410,7 @@
go _bound (EUVar _) acc = acc
go _ _ _ = undefined
-{--metaTvs :: [EType] -> [MetaTv]
+metaTvs :: [EType] -> [TRef]
-- Get the MetaTvs from a type; no duplicates in result
metaTvs tys = foldr go [] tys
where
@@ -1410,10 +1418,11 @@
| elemBy eqInt tv acc = acc
| otherwise = tv : acc
go (EVar _) acc = acc
- go (EForall _ ty) acc = go ty acc -- ForAll binds TyVars only
+ go (EForall _ ty) acc = go ty acc
go (EApp fun arg) acc = go fun (go arg acc)
go _ _ = undefined
+{-tyVarBndrs :: Rho -> [TyVar]
-- Get all the binders used in ForAlls in the type, so that
-- when quantifying an outer for-all we can avoid these inner ones
--
⑨