ref: c651641083508579592c962726be14fd306a8279
parent: ed4d9b81423432e432b2c171844bd82c4a22580b
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Thu Oct 26 15:48:47 EDT 2023
Use a regular type variable for Infer. This enables Infer to be used for recursive functions in a better way.
--- a/TODO
+++ b/TODO
@@ -33,3 +33,10 @@
- The IORef will need GC support
* Redo type synonym expansion
- Only non-injective synonyms necessitate expansion(?)
+ - Do expansion during unification
+* Redo handling of synonym and instance tables.
+ - These tables can persist during the compilation
+ and only grow
+* Just put exported classes in class export
+* Implement two level tables for instances even in the tricky cases
+* Handle tupled dictionaries better for recursive calls
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v4.0
-1121
-((A :0 _944) ((A :1 ((B _990) _0)) ((A :2 (((S' _990) _0) I)) ((A :3 _914) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _943) ((C _84) _5))) ((A :7 (((C' _6) (_961 _73)) ((_84 _959) _72))) ((A :8 ((B ((S _990) _959)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_84 _210)) _10)) ((A :12 ((B (B (_82 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_82 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_82 _9)) P)) ((A :15 ((B (B (_82 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 (((C' B) _12) (((C' B) _12) (B _14)))) ((A :18 ((B (_82 _9)) (B (P _872)))) ((A :19 ((B (_82 _9)) (BK (P _872)))) ((A :20 ((_82 _9) ((S P) I))) ((A :21 ((B (_82 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _122)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _123)))))) ((A :23 ((B Y) ((B (B (P (_14 _872)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _872))) ((A :26 (_22 _85)) ((A :27 (R _34)) ((A :28 (T _33)) ((A :29 ((P _34) _33)) ((A :30 _34) ((A :31 ((C ((C S') _29)) I)) ((A :32 ((C S) _29)) ((A :33 K) ((A :34 A) ((A :35 ((_76 _908) _909)) ((A :36 ((_76 _918) (_80 _36))) ((A :37 _919) ((A :38 _920) ((A :39 (((S' _28) (_911 #97)) ((C _911) #122))) ((A :40 (((S' _28) (_911 #65)) ((C _911) #90))) ((A :41 (((S' _27) _39) _40)) ((A :42 (((S' _28) (_911 #48)) ((C _911) #57))) ((A :43 (((S' _28) (_911 #32)) ((C _911) #126))) ((A :44 _908) ((A :45 _909) ((A :46 _911) ((A :47 _910) ((A :48 (((S' _27) ((C (_77 _35)) #32)) (((S' _27) ((C (_77 _35)) #9)) ((C (_77 _35)) #10)))) ((A :49 ((S ((S (((S' _28) (_46 #65)) ((C _46) #90))) (_34 (((_871 "lib/Data/Char.hs") #3) #8)))) ((B _37) (((C' _91) (((C' _92) _38) (_38 #65))) (_38 #97))))) ((A :50 ((S ((S (((S' _28) (_46 #97)) ((C _46) #97))) (_34 (((_871 "lib/Data/Char.hs") #3) #8)))) ((B _37) (((C' _91) (((C' _92) _38) (_38 #97))) (_38 #65))))) ((A :51 _879) ((A :52 _880) ((A :53 _881) ((A :54 _882) ((A :55 (_52 %0.0)) ((A :56 _51) ((A :57 _52) ((A :58 _53) ((A :59 _54) ((A :60 ((_76 _883) _884)) ((A :61 (_77 _60)) ((A :62 (_78 _60)) ((A :63 _885) ((A :64 _886) ((A :65 _887) ((A :66 _888) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _66) ((A :71 _889) ((A :72 ((B BK) T)) ((A :73 (BK T)) ((A :74 (((S' _76) (((S' C) ((B (C S')) (((C' C) ((B (C C')) ((B _77) (T K)))) (K _33)))) ((B ((C' B) (T (K _33)))) ((B _77) (T A))))) ((B _80) ((B _74) (((S' P) (T K)) (T A)))))) ((A :75 P) ((A :76 P) ((A :77 (T K)) ((A :78 (T A)) ((A :79 (K (noDefault "Eq.=="))) ((A :80 ((B (B (B _29))) _77)) ((A :81 ((_76 ((C ((C S') _29)) I)) (_80 _81))) ((A :82 I) ((A :83 (S _916)) ((A :84 B) ((A :85 I) ((A :86 K) ((A :87 C) ((A :88 _915) ((A :89 ((C ((C S') _210)) _211)) ((A :90 (((C' (S' (C' B))) B) I)) ((A :91 _873) ((A :92 _874) ((A :93 _875) ((A :94 _876) ((A :95 _877) ((A :96 _878) ((A :97 (_92 #0)) ((A :98 ((_76 _896) _897)) ((A :99 _898) ((A :100 _899) ((A :101 _900) ((A :102 _901) ((A :103 (BK K)) ((A :104 ((B BK) ((B (B BK)) P))) ((A :105 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :106 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_100 #0))) ((C (_77 _98)) #0)))) ((B (B ((C' P) (_96 #1)))) _91))) (C P))) _94)) _95)) ((A :107 _103) ((A :108 (((S' C) ((B (P _197)) (((C' (C' B)) (((C' C) (_77 _98)) _197)) _198))) ((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') ((C (_77 _98)) #0))))) ((B ((C' (C' C)) ((B (B ((S' S') ((C (_77 _98)) #1)))) ((B ((C' C) ((B ((C' S') ((C (_77 _98)) #2))) (C _108)))) (C _108))))) (C _108))))) (C _108)))) (T K))) (T A)))) ((C _106) #4)))) ((A :109 (_115 _86)) ((A :110 ((_131 (_89 _109)) _107)) ((A :111 ((C (((C' B) ((P _122) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _112)))) (((S' (C' (C' B))) ((B (B (B _112))) (((S' (C' B)) ((B (B _112)) (((C' B) ((B _129) (T #0))) _111))) (((C' B) ((B _129) (T #1))) _111)))) (((C' B) ((B _129) (T #2))) _111)))) (((C' B) ((B _129) (T #3))) _111)))) ((B T) ((B (B P)) ((C' _91) (_93 #4)))))) ((A :112 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C')
\ No newline at end of file
+1120
+((A :0 _943) ((A :1 ((B _989) _0)) ((A :2 (((S' _989) _0) I)) ((A :3 _913) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _942) ((C _84) _5))) ((A :7 (((C' _6) (_960 _73)) ((_84 _958) _72))) ((A :8 ((B ((S _989) _958)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_84 _210)) _10)) ((A :12 ((B (B (_82 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_82 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_82 _9)) P)) ((A :15 ((B (B (_82 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 (((C' B) _12) (((C' B) _12) (B _14)))) ((A :18 ((B (_82 _9)) (B (P _871)))) ((A :19 ((B (_82 _9)) (BK (P _871)))) ((A :20 ((_82 _9) ((S P) I))) ((A :21 ((B (_82 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _122)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _123)))))) ((A :23 ((B Y) ((B (B (P (_14 _871)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _871))) ((A :26 (_22 _85)) ((A :27 (R _34)) ((A :28 (T _33)) ((A :29 ((P _34) _33)) ((A :30 _34) ((A :31 ((C ((C S') _29)) I)) ((A :32 ((C S) _29)) ((A :33 K) ((A :34 A) ((A :35 ((_76 _907) _908)) ((A :36 ((_76 _917) (_80 _36))) ((A :37 _918) ((A :38 _919) ((A :39 (((S' _28) (_910 #97)) ((C _910) #122))) ((A :40 (((S' _28) (_910 #65)) ((C _910) #90))) ((A :41 (((S' _27) _39) _40)) ((A :42 (((S' _28) (_910 #48)) ((C _910) #57))) ((A :43 (((S' _28) (_910 #32)) ((C _910) #126))) ((A :44 _907) ((A :45 _908) ((A :46 _910) ((A :47 _909) ((A :48 (((S' _27) ((C (_77 _35)) #32)) (((S' _27) ((C (_77 _35)) #9)) ((C (_77 _35)) #10)))) ((A :49 ((S ((S (((S' _28) (_46 #65)) ((C _46) #90))) (_34 (((_870 "lib/Data/Char.hs") #3) #8)))) ((B _37) (((C' _91) (((C' _92) _38) (_38 #65))) (_38 #97))))) ((A :50 ((S ((S (((S' _28) (_46 #97)) ((C _46) #97))) (_34 (((_870 "lib/Data/Char.hs") #3) #8)))) ((B _37) (((C' _91) (((C' _92) _38) (_38 #97))) (_38 #65))))) ((A :51 _878) ((A :52 _879) ((A :53 _880) ((A :54 _881) ((A :55 (_52 %0.0)) ((A :56 _51) ((A :57 _52) ((A :58 _53) ((A :59 _54) ((A :60 ((_76 _882) _883)) ((A :61 (_77 _60)) ((A :62 (_78 _60)) ((A :63 _884) ((A :64 _885) ((A :65 _886) ((A :66 _887) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _66) ((A :71 _888) ((A :72 ((B BK) T)) ((A :73 (BK T)) ((A :74 (((S' _76) (((S' C) ((B (C S')) (((C' C) ((B (C C')) ((B _77) (T K)))) (K _33)))) ((B ((C' B) (T (K _33)))) ((B _77) (T A))))) ((B _80) ((B _74) (((S' P) (T K)) (T A)))))) ((A :75 P) ((A :76 P) ((A :77 (T K)) ((A :78 (T A)) ((A :79 (K (noDefault "Eq.=="))) ((A :80 ((B (B (B _29))) _77)) ((A :81 ((_76 ((C ((C S') _29)) I)) (_80 _81))) ((A :82 I) ((A :83 (S _915)) ((A :84 B) ((A :85 I) ((A :86 K) ((A :87 C) ((A :88 _914) ((A :89 ((C ((C S') _210)) _211)) ((A :90 (((C' (S' (C' B))) B) I)) ((A :91 _872) ((A :92 _873) ((A :93 _874) ((A :94 _875) ((A :95 _876) ((A :96 _877) ((A :97 (_92 #0)) ((A :98 ((_76 _895) _896)) ((A :99 _897) ((A :100 _898) ((A :101 _899) ((A :102 _900) ((A :103 (BK K)) ((A :104 ((B BK) ((B (B BK)) P))) ((A :105 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :106 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_100 #0))) ((C (_77 _98)) #0)))) ((B (B ((C' P) (_96 #1)))) _91))) (C P))) _94)) _95)) ((A :107 _103) ((A :108 (((S' C) ((B (P _197)) (((C' (C' B)) (((C' C) (_77 _98)) _197)) _198))) ((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') ((C (_77 _98)) #0))))) ((B ((C' (C' C)) ((B (B ((S' S') ((C (_77 _98)) #1)))) ((B ((C' C) ((B ((C' S') ((C (_77 _98)) #2))) (C _108)))) (C _108))))) (C _108))))) (C _108)))) (T K))) (T A)))) ((C _106) #4)))) ((A :109 (_115 _86)) ((A :110 ((_131 (_89 _109)) _107)) ((A :111 ((C (((C' B) ((P _122) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _112)))) (((S' (C' (C' B))) ((B (B (B _112))) (((S' (C' B)) ((B (B _112)) (((C' B) ((B _129) (T #0))) _111))) (((C' B) ((B _129) (T #1))) _111)))) (((C' B) ((B _129) (T #2))) _111)))) (((C' B) ((B _129) (T #3))) _111)))) ((B T) ((B (B P)) ((C' _91) (_93 #4)))))) ((A :112 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C')
\ No newline at end of file
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -612,7 +612,7 @@
munify :: --XHasCallStack =>
SLoc -> Expected -> EType -> T ()
-munify _ (Infer r) b = tSetRefType r b
+munify loc (Infer r) b = tSetRefType loc r b
munify loc (Check a) b = unify loc a b
expandSyn :: --XHasCallStack =>
@@ -695,7 +695,7 @@
Just t' -> unify loc t' t
unifyUnboundVar :: --XHasCallStack =>
- SLoc -> TRef -> EType -> T ()
+ SLoc -> TRef -> EType -> T ()
unifyUnboundVar loc r1 at2@(EUVar r2) = T.do
-- We know r1 /= r2
mt2 <- getUVar r2
@@ -709,7 +709,7 @@
else
setUVar r1 t2
--- Reset type variable and unification map
+-- Reset unification map
tcReset :: T ()
tcReset = T.do
TC mn u fx tenv senv venv ast _ m cs is es <- get
@@ -1256,17 +1256,17 @@
tGetRefType ref = T.do
m <- gets uvarSubst
case IM.lookup ref m of
- Nothing -> error "tGetRefType"
- Just t -> T.return t
+ Nothing -> T.return (EUVar ref) -- error "tGetRefType"
+ Just t -> T.return t
-- Set the type for an Infer
tSetRefType :: --XHasCallStack =>
- TRef -> EType -> T ()
-tSetRefType ref t = T.do
+ SLoc -> TRef -> EType -> T ()
+tSetRefType loc ref t = T.do
m <- gets uvarSubst
case IM.lookup ref m of
Nothing -> putUvarSubst (IM.insert ref t m)
- Just _ -> error "tSetRefType"
+ Just tt -> unify loc tt t
-- Get the type of an already set Expected
tGetExpType :: Expected -> T EType
@@ -1273,13 +1273,15 @@
tGetExpType (Check t) = T.return t
tGetExpType (Infer r) = tGetRefType r
--- Get the type of an unset Expected
-tGetExpTypeSet :: Expected -> T EType
-tGetExpTypeSet (Check t) = T.return t
-tGetExpTypeSet (Infer r) = T.do
+{-+-- Get the type of a possibly unset Expected
+tGetExpTypeSet :: SLoc -> Expected -> T EType
+tGetExpTypeSet _ (Check t) = T.return t
+tGetExpTypeSet loc (Infer r) = tGetRefType r {-T.dot <- newUVar
- tSetRefType r t
- T.return t
+ tSetRefType loc r t
+ T.return t-}
+-}
tcExpr :: --XHasCallStack =>
Expected -> Expr -> T Expr
@@ -1299,7 +1301,7 @@
case tcm of
TCPat | isDummyIdent i -> T.do
-- _ can be anything, so just ignore it
- _ <- tGetExpTypeSet mt
+ _ <- tGetExpType mt
T.return ae
| isConIdent i -> T.do
@@ -1308,15 +1310,15 @@
-- We will only have an expected type for a non-nullary constructor
case mt of
Check ext -> subsCheck loc p ext pt
- Infer r -> T.do { tSetRefType r pt; T.return p }+ Infer r -> T.do { tSetRefType loc r pt; T.return p }| otherwise -> T.do
-- All pattern variables are in the environment as
-- type references. Assign the reference the given type.
- ext <- tGetExpTypeSet mt
+ ext <- tGetExpType mt
(p, t) <- tLookupV i
case t of
- EUVar r -> tSetRefType r ext
+ EUVar r -> tSetRefType loc r ext
_ -> impossible
T.return p
@@ -1364,7 +1366,7 @@
ELit loc' l -> tcLit mt loc' l
ECase a arms -> T.do
(ea, ta) <- tInferExpr a
- tt <- tGetExpTypeSet mt
+ tt <- tGetExpType mt
earms <- T.mapM (tcArm tt ta) arms
T.return (ECase ea earms)
ELet bs a -> tcBinds bs $ \ ebs -> T.do { ea <- tcExpr mt a; T.return (ELet ebs ea) }@@ -1414,7 +1416,7 @@
(e3', t3) <- tInferExpr e3
e2'' <- subsCheck loc e2' t2 t3
e3'' <- subsCheck loc e3' t3 t2
- tSetRefType ref t2
+ tSetRefType loc ref t2
T.return (EIf e1' e2'' e3'')
EListish (LList es) -> T.do
@@ -1466,7 +1468,7 @@
e' <- tcExpr mt e
tt <- tGetExpType mt
case ti of
- EUVar r -> tSetRefType r tt
+ EUVar r -> tSetRefType loc r tt
_ -> impossible
T.return (EAt i e')
EForall vks t ->
@@ -1546,7 +1548,7 @@
tcExprLam :: Expected -> [EPat] -> Expr -> T Expr
tcExprLam mt aps expr = T.do
- t <- tGetExpTypeSet mt
+ t <- tGetExpType mt
tcPats t aps $ \ tt ps -> T.do
er <- tCheckExpr tt expr
T.return (ELam ps er)
@@ -1618,7 +1620,7 @@
instPatSigma :: --XHasCallStack =>
SLoc -> Sigma -> Expected -> T ()
-instPatSigma _ pt (Infer r) = tSetRefType r pt
+instPatSigma loc pt (Infer r) = tSetRefType loc r pt
instPatSigma loc pt (Check t) = T.do { _ <- subsCheck loc undefined t pt; T.return () } -- XXX really?subsCheck :: --XHasCallStack =>
@@ -1911,10 +1913,10 @@
instSigma loc e1 t1 (Check t2) = T.do
-- traceM ("instSigma: Check " ++ showEType t1 ++ " = " ++ showEType t2)subsCheckRho loc e1 t1 t2
-instSigma _ e1 t1 (Infer r) = T.do
+instSigma loc e1 t1 (Infer r) = T.do
(e1', t1') <- tInst (e1, t1)
-- traceM ("instSigma: Infer " ++ showEType t1 ++ " ==> " ++ showEType t1')- tSetRefType r t1'
+ tSetRefType loc r t1'
T.return e1'
-----
--
⑨