ref: 1a1d3c21d966d5833ea301dae7618cfa705fb389
parent: bd15c42f1966dbc55ad1a89cc82630add7612095
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Sun Oct 8 19:30:53 EDT 2023
Clean up a bit.
--- a/TODO
+++ b/TODO
@@ -3,8 +3,6 @@
* Have compile return a Stats record of timing etc
* Add overloading
* Implement deriving
-* Make sure rank-N works correctly
- - redo type checker
* Add the possibility to save a compiler cache in a file
- Add SHA checksumming to the C code
- Use filename as the cache lookup key and SHA for validation
@@ -21,3 +19,7 @@
f x = let f' y = ... f' e ...
this will specialize recursive functions
(and make more efficient 'map' etc)
+* Type checker improvements:
+ - allow generalization for local bindings
+ - use subsumption (like if) in the arms of alternatives.
+ - allow missing top level signatures (and generalize)
--- 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
+967
+(($A :0 _851) (($A :1 (($B _897) _0)) (($A :2 ((($S' _897) _0) $I)) (($A :3 _821) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _850) (($C _74) _5))) (($A :7 ((($C' _6) (_868 _71)) ((_74 _866) _70))) (($A :8 (($B (($S _897) _866)) _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 _779)))) (($A :18 (($B (_73 _9)) ($BK ($P _779)))) (($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 _779)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _779))) (($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 _826) (($A :35 _827) (($A :36 ((($S' _27) (_818 97)) (($C _818) 122))) (($A :37 ((($S' _27) (_818 65)) (($C _818) 90))) (($A :38 ((($S' _26) _36) _37)) (($A :39 ((($S' _27) (_818 48)) (($C _818) 57))) (($A :40 ((($S' _27) (_818 32)) (($C _818) 126))) (($A :41 _815) (($A :42 _816) (($A :43 _818) (($A :44 _817) (($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 (((_778 "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 (((_778 "lib/Data/Char.hs") 3) 8)))) (($B _34) ((($C' _81) ((($C' _82) _35) (_35 97))) (_35 65))))) (($A :48 _786) (($A :49 _787) (($A :50 _788) (($A :51 _789) (($A :52 (_49 %0.0)) (($A :53 _48) (($A :54 _49) (($A :55 _50) (($A :56 _51) (($A :57 _790) (($A :58 _791) (($A :59 _57) (($A :60 _58) (($A :61 _792) (($A :62 _793) (($A :63 _794) (($A :64 _795) (($A :65 _61) (($A :66 _62) (($A :67 _63) (($A :68 _64) (($A :69 _796) (($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 _822) (($A :79 (($C (($C $S') _188)) _189)) (($A :80 ((($C' ($S' ($C' $B))) $B) $I)) (($A :81 _780) (($A :82 _781) (($A :83 _782) (($A :84 _783) (($A :85 _784) (($A :86 _785) (($A :87 (_82 0)) (($A :88 _803) (($A :89 _804) (($A :90 _805) (($A :91 _806) (($A :92 _807) (($A :93 _808) (($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
@@ -43,6 +43,11 @@
type SynTable = M.Map ETypeScheme
type FixTable = M.Map Fixity
+type Sigma = EType
+--type Tau = EType
+type Rho = EType
+type TyVar = Ident
+
typeCheck :: forall a . [(ImportSpec, TModule a)] -> EModule -> TModule [EDef]
typeCheck aimps (EModule mn exps defs) =
-- trace (show amdl) $
@@ -467,7 +472,10 @@
mt <- getUVar i
case mt of
Nothing -> T.return at
- Just t -> derefUVar t
+ Just t -> T.do
+ t' <- derefUVar t
+ addUVar i t'
+ T.return t'
EVar _ -> T.return at
ESign t k -> flip ESign k <$> derefUVar t
EForall iks t -> EForall iks <$> derefUVar t
@@ -506,6 +514,7 @@
EUVar i -> addUVar i b
_ -> impossible
+{-unMType :: Expected -> T EType
unMType mt =
case mt of
@@ -514,6 +523,7 @@
tSetRefType r t
T.return t
Check t -> T.return t
+-}
-- Reset type variable and unification map
tcReset :: T ()
@@ -903,7 +913,7 @@
case tcm of
TCPat -> T.do
a' <- tCheckExpr at a
- instPatSigmaE loc rt mt
+ instPatSigma loc rt mt
T.return (EApp f' a')
_ -> T.do
a' <- checkSigma a at
@@ -915,7 +925,7 @@
ELit loc' l -> tcLit mt loc' l
ECase a arms -> T.do
(ea, ta) <- tInferExpr a
- tt <- unMType mt
+ tt <- tGetExpTypeSet 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) }@@ -954,27 +964,25 @@
let x = eVarI loc "$x"
tcExpr mt (ELam [x] (EApp (EApp (EVar i) x) e))
EIf e1 e2 e3 -> T.do
- ee1 <- tCheckExpr (tBool (getSLocExpr e1)) e1
+ e1' <- tCheckExpr (tBool (getSLocExpr e1)) e1
case mt of
Check t -> T.do
- ee2 <- tCheckExpr t e2
- ee3 <- tCheckExpr t e3
- T.return (EIf ee1 ee2 ee3)
+ e2' <- checkSigma e2 t
+ e3' <- checkSigma e3 t
+ T.return (EIf e1' e2' e3')
Infer ref -> T.do
- (ee2, te2) <- tInferExpr e2
- (ee3, te3) <- tInferExpr e3
- unify loc te2 te3
- tSetRefType ref te2
- T.return (EIf ee1 ee2 ee3)
+ (e2', t1) <- tInferExpr e2
+ (e3', t2) <- tInferExpr e3
+ subsCheck loc t1 t2
+ subsCheck loc t2 t1
+ tSetRefType ref t1
+ T.return (EIf e1' e2' e3')
+
EListish (LList es) -> T.do
- (ees, ts) <- T.fmap unzip (T.mapM tInferExpr es)
- te <- case ts of
- [] -> newUVar
- t : _ -> T.return t
- let
- tlist = tApp (tList loc) te
- munify loc mt tlist
- T.return (EListish (LList ees))
+ te <- newUVar
+ munify loc mt (tApp (tList loc) te)
+ es' <- T.mapM (tCheckExpr te) es
+ T.return (EListish (LList es'))
EListish (LCompr eret ass) -> T.do
let
doStmts :: [EStmt] -> [EStmt] -> T ([EStmt], Typed Expr)
@@ -1009,7 +1017,7 @@
tcm <- gets tcMode
case tcm of
TCPat -> T.do
- instPatSigmaE loc t' mt
+ instPatSigma loc t' mt
tCheckExpr t' e
_ -> T.do
instSigma loc t' mt
@@ -1032,8 +1040,8 @@
enum loc f = foldl EApp (EVar (mkIdentSLoc loc ("enum" ++ f)))tcLit :: Expected -> SLoc -> Lit -> T Expr
-tcLit mt loc l =
- let { lit t = T.do { munify loc mt t; T.return (ELit loc l) } } in+tcLit mt loc l = T.do
+ let lit t = instSigma loc t mt
case l of
LInt _ -> lit (tConI loc "Primitives.Int")
LDouble _ -> lit (tConI loc "Primitives.Double")
@@ -1041,6 +1049,7 @@
LStr _ -> lit (tApp (tConI loc "Data.List.[]") (tConI loc "Primitives.Char"))
LPrim _ -> newUVar T.>>= lit -- pretend it is anything
LForImp _ -> impossible
+ T.return (ELit loc l)
tcOper :: --XHasCallStack =>
Expr -> [(Ident, Expr)] -> T Expr
@@ -1098,7 +1107,7 @@
tcExprLam :: Expected -> [EPat] -> Expr -> T Expr
tcExprLam mt aps expr = T.do
- t <- unMType mt
+ t <- tGetExpTypeSet mt
tcPats t aps $ \ tt ps -> T.do
er <- tCheckExpr tt expr
T.return (ELam ps er)
@@ -1141,70 +1150,16 @@
T.return (pp, aalts)
-{--tcPatE :: forall a . --XHasCallStack =>
- Expected -> EPat -> (EPat -> T a) -> T a
-tcPatE _ p@(EVar i) ta | isUnderscore i =
- ta p
-tcPatE mt p@(EVar i) ta | isConIdent i = T.do
- p' <- tcExpr mt p -- just instantiate constructor
- ta p'
-tcPatE mt p@(EVar i) ta = T.do
- t <- tGetExpTypeSet mt
- withExtVal i t $ ta p
-tcPatE mt ap@(EApp _ _) ta = T.do
- let apps (EApp f a) as = apps f (a:as)
- apps (EVar i) as | isConIdent i = T.do
- (c, t) <- tLookupInst "constructor" i
- unApps c t as
- apps p _ = tcError (getSLocExpr p) "Bad pattern"
- unApps p t [] = T.do
- T.when (isArrow t) $
- tcError (getSLocExpr p) "Too few constructor arguments"
- instPatSigmaE (getSLocExpr p) t mt
- ta p
- -- getArrow is OK here rather than unifyFun, since the
- -- constructor arrows are inserted by the compiler.
- unApps p t (a:as) | Just (arg, res) <- getArrow t =
- tcPatE (Check arg) a $ \ a' -> unApps (EApp p a') res as
- unApps p _ _ = tcError (getSLocExpr p) "Too many constructor arguments"
- apps ap []
-tcPatE mt (ESign p pt) ta = T.do
- instPatSigmaE (getSLocExpr p) pt mt
- tcPatE (Check pt) p ta
-tcPatE mt (EAt i p) ta =
- tcPatE mt p $ \ p' -> T.do
- t <- tGetExpType mt
- withExtVal i t $ ta (EAt i p')
-tcPatE mt p@(ELit _ _) ta = T.do
- p' <- tcExpr mt p
- ta p'
-tcPatE mt ap@(ETuple ps) ta = T.do
- let p = foldl EApp (EVar c) ps -- desugar
- c = tupleConstr (getSLocExpr ap) (length ps)
- tcPatE mt p ta
-tcPatE mt ap@(EListish (LList aps)) ta = T.do -- XXX could do better for Check
- te <- newUVar
- let loc = getSLocExpr ap
- loop [] ps' = T.do
- instPatSigmaE loc (tApp (tList loc) te) mt
- ta (EListish (LList ps'))
- loop (p:ps) ps' = tcPatE (Check te) p $ \ p' -> loop ps (ps' ++ [p'])
- loop aps []
-tcPatE _ p _ = --Xtrace ("tcPatE: " ++ show p) $- impossible
--}
-
-instPatSigmaE :: --XHasCallStack =>
+instPatSigma :: --XHasCallStack =>
SLoc -> Sigma -> Expected -> T ()
-instPatSigmaE _ pt (Infer r) = tSetRefType r pt
-instPatSigmaE loc pt (Check t) = subsCheckE loc t pt
+instPatSigma _ pt (Infer r) = tSetRefType r pt
+instPatSigma loc pt (Check t) = subsCheck loc t pt
-subsCheckE :: --XHasCallStack =>
+subsCheck :: --XHasCallStack =>
SLoc -> Sigma -> Sigma -> T ()
-- (subsCheck args off exp) checks that
-- 'off' is at least as polymorphic as 'args -> exp'
-subsCheckE loc sigma1 sigma2 = T.do -- Rule DEEP-SKOL
+subsCheck loc sigma1 sigma2 = T.do -- Rule DEEP-SKOL
(skol_tvs, rho2) <- skolemise sigma2
subsCheckRho loc sigma1 rho2
esc_tvs <- getFreeTyVars [sigma1,sigma2]
@@ -1252,7 +1207,6 @@
where
check0 = if n /= 0 then tcError (getSLocExpr p) "Bad pattern" else T.return ()
--- XXX No mutual recursion yet
tcBinds :: forall a . [EBind] -> ([EBind] -> T a) -> T a
tcBinds xbs ta = T.do
let
@@ -1339,55 +1293,23 @@
-----------------------------------------------------
-type Sigma = EType
---type Tau = EType
-type Rho = EType
-type TyVar = Ident
-
-type Tc a = T a
-
-{--
-type TcRef = Int
---data Expected = Infer TcRef | Check EType
-type MetaTv = TcRef
-
-xtypecheck :: EType -> Tc Sigma
-xtypecheck e = T.do
- (ty, _) <- inferSigma e
- zonkType ty
-
-newTcRef :: EType -> Tc TcRef
-newTcRef t = T.do
- r <- newUniq
- addUVar r t
- T.return r
-readTcRef :: TcRef -> Tc EType
-readTcRef r = T.do
- mt <- getUVar r
- case mt of
- Just t -> T.return t
- Nothing -> error "readTcRef"
-writeTcRef :: TcRef -> EType -> Tc ()
-writeTcRef r t = addUVar r t
--}
-
-getFreeTyVars :: [EType] -> Tc [TyVar]
+getFreeTyVars :: [EType] -> T [TyVar]
getFreeTyVars tys = T.do
- tys' <- T.mapM zonkType tys
+ tys' <- T.mapM derefUVar tys
T.return (freeTyVars tys')
{--getMetaTyVars :: [EType] -> Tc [MetaTv]
+getMetaTyVars :: [EType] -> T [MetaTv]
getMetaTyVars tys = T.do
tys' <- T.mapM zonkType tys
T.return (metaTvs tys')
-}
-getEnvTypes :: Tc [EType]
+getEnvTypes :: T [EType]
getEnvTypes = gets (map entryType . concat . M.elems . valueTable)
-zonkType :: EType -> Tc EType
+{-+zonkType :: EType -> T EType
zonkType (EForall ns ty) = T.do
ty' <- zonkType ty
T.return (EForall ns ty')
@@ -1406,9 +1328,9 @@
res' <- zonkType res
T.return (EApp arg' res')
zonkType _ = undefined
-
+-}
{--quantify :: [MetaTv] -> Rho -> Tc Sigma
+quantify :: [MetaTv] -> Rho -> T Sigma
-- Quantify over the specified type variables (all flexible)
quantify tvs ty = T.do
T.mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
@@ -1426,7 +1348,7 @@
-}
skolemise :: --XHasCallStack =>
- Sigma -> Tc ([TyVar], Rho)
+ Sigma -> T ([TyVar], Rho)
-- Performs deep skolemisation, returning the
-- skolem constants and the skolemised type
skolemise (EForall tvs ty) = T.do -- Rule PRPOLY
@@ -1444,23 +1366,11 @@
T.return ([], ty) -- Rule PRMONO
-- Skolem tyvars are just identifiers that start with a uniq
-newSkolemTyVar :: Ident -> Tc Ident
+newSkolemTyVar :: Ident -> T Ident
newSkolemTyVar tv = T.do
uniq <- newUniq
T.return (mkIdentSLoc (getSLocIdent tv) (showInt uniq ++ unIdent tv))
-{--extendVarEnvList :: forall a . [(Ident, Sigma)] -> Tc a -> Tc a
-extendVarEnvList varTys ta = T.do
- venv <- gets valueTable
- putValueTable (foldr (\ (i, t) -> M.insert i [Entry (EVar i) t]) venv varTys)
- a <- ta
- putValueTable venv
- T.return a
-
-------------------
--}
-
freeTyVars :: [EType] -> [TyVar]
-- Get the free TyVars from a type; no duplicates in result
freeTyVars = foldr (go []) []
@@ -1501,31 +1411,7 @@
bndrs (EVar _) = []
bndrs _ = undefined
-substTy :: [Ident] -> [EType] -> EType -> EType
-
--- Replace the specified quantified type variables by
--- given meta type variables
--- No worries about capture, because the two kinds of type
--- variable are distinct
-substTy tvs tys ty = subst_ty (tvs `zip` tys) ty
-
-subst_ty :: [(TyVar, Tau)] -> EType -> EType
-subst_ty env (EApp arg res) = EApp (subst_ty env arg) (subst_ty env res)
-subst_ty env ty@(EVar n) = fromMaybe ty (lookupBy eqIdent n env)
-subst_ty _env (EUVar tv) = EUVar tv
-subst_ty env (EForall nks rho) = EForall nks (subst_ty env' rho)
- where
- env' = [(n, ty') | (n, ty') <- env, not (elemBy eqIdent n ns)]
- ns = map idKindIdent nks
-subst_ty _ _ = undefined
-
------------------------
-
-check :: Bool -> String -> Tc ()
-check False msg = error msg
-check True _ = T.return ()
-
-inferSigma :: Expr -> Tc (Expr, Sigma)
+inferSigma :: Expr -> T (Expr, Sigma)
inferSigma e = T.do
(e', exp_ty) <- inferRho e
env_tys <- getEnvTypes
@@ -1535,7 +1421,7 @@
(e',) <$> quantify forall_tvs exp_ty
-}
-checkSigma :: Expr -> Sigma -> Tc Expr
+checkSigma :: Expr -> Sigma -> T Expr
checkSigma expr sigma = T.do
(skol_tvs, rho) <- skolemise sigma
expr' <- tCheckExpr rho expr
@@ -1550,288 +1436,7 @@
tcError (getSLocExpr expr) "Type not polymorphic enough"
T.return expr'
-{--checkRho :: Expr -> Rho -> Tc Expr
-checkRho expr ty =
- tcRho expr (Check ty)
-
-inferRho :: Expr -> Tc (Expr, Rho)
-inferRho expr = T.do
- ref <- newTcRef (error "inferRho: empty result")
- expr' <- tcRho expr (Infer ref)
- (expr',) <$> readTcRef ref
-
-tcRho :: Expr -> Expected -> Tc Expr
-tcRho (EVar v) exp_ty = T.do
- (expr', v_sigma) <- tLookup "variable" v
- instSigma noSLoc v_sigma exp_ty
- T.return expr'
-tcRho (EApp fun arg) exp_ty = T.do
- (fun', fun_ty) <- inferRho fun
- (arg_ty, res_ty) <- unifyFun noSLoc fun_ty
- arg' <- checkSigma arg arg_ty
- instSigma noSLoc res_ty exp_ty
- T.return (EApp fun' arg')
-tcRho (EOper _e _ies) _ = undefined
-tcRho (ELam [] body) exp_ty = ELam [] <$> tcRho body exp_ty
-tcRho (ELam (pat:pats) body) exp_ty = T.do
- (pat', ELam pats' body') <- tcLamRho pat (ELam pats body) exp_ty
- T.return (ELam (pat' : pats') body')
-tcRho expr@(ELit loc l) exp_ty = T.do
- tcLitRho loc l exp_ty
- T.return expr
-{--tcRho (ECase _ []) _ = impossible
-tcRho (ECase e arms) (Check exp_ty) = T.do
- (e', tpat) <- inferRho e -- XXX check for kind Type
- let checkArm (pat, alts) = T.do
- binds <- checkPat pat tpat
- alts' <- extendVarEnvList binds $ checkAlts alts exp_ty
- T.return (pat, alts')
- arms' <- mapM checkArm arms
- T.return (ECase e' arms')
-tcRho (ECase e arms) (Infer ref) = T.do
- (e', tpat) <- inferRho e -- XXX check for kind Type
- let inferArm (pat, alts) = T.do
- binds <- checkPat pat tpat
- (alts', rho) <- extendVarEnvList binds $ inferAlts alts
- T.return ((pat, alts'), rho)
- (arms', rho:rhos) <- unzip <$> mapM inferArm arms
- mapM_ (\ r -> do { subsCheck rho r; subsCheck r rho }) rhos- writeTcRef ref rho
- T.return (ECase e' arms')
--}
-tcRho (ELet _bs _a) _ = undefined
-tcRho (ETuple es) (Check exp_ty) = T.do
- ts <- unifyTuple (length es) exp_ty
- es' <- T.sequence (zipWith checkRho es ts)
- T.return (ETuple es')
-tcRho (ETuple es) (Infer ref) = T.do
- let n = length es
- (es', ts) <- unzip <$> T.mapM inferRho es
- writeTcRef ref $ tApps (tupleConstr builtinLoc n) ts
- T.return (ETuple es')
-tcRho (EDo _mmn _ass) _ = undefined
-tcRho (ESectL e i) exp_ty = tcRho (EApp (EVar i) e) exp_ty
-tcRho (ESectR i e) exp_ty = T.do
- let x = eVarI (getSLocIdent i) "$x"
- tcRho (ELam [x] (EApp (EApp (EVar i) x) e)) exp_ty
-tcRho (EIf e1 e2 e3) (Check exp_ty) = T.do
- e1' <- checkRho e1 (tBool (getSLocExpr e1))
- e2' <- checkSigma e2 exp_ty
- e3' <- checkSigma e3 exp_ty
- T.return (EIf e1' e2' e3')
-tcRho (EIf e1 e2 e3) (Infer ref) = T.do
- e1' <- checkRho e1 (tBool (getSLocExpr e1))
- (e2', rho1) <- inferRho e2
- (e3', rho2) <- inferRho e3
- subsCheck noSLoc rho1 rho2
- subsCheck noSLoc rho2 rho1
- writeTcRef ref rho1
- T.return (EIf e1' e2' e3')
-tcRho ee@(EListish lst) exp_ty = T.do
- let loc = getSLocExpr ee
- case lst of
- LList es ->
- case exp_ty of
- Check tl -> T.do
- te <- unifyList tl
- es' <- T.mapM (\ e -> checkRho e te) es
- T.return (EListish (LList es'))
- Infer ref -> T.do
- (es', ts') <- unzip <$> T.mapM inferRho es
- te <- case ts' of
- [] -> newUVar
- tt : tts -> T.do
- T.mapM_ (unify loc tt) tts
- T.return tt
- writeTcRef ref (tApp (tList loc) te)
- T.return (EListish (LList es'))
-{-- LCompr eret ass -> T.do
- let
- doStmts :: [EStmt] -> [EStmt] -> T ([EStmt], Typed Expr)
- doStmts rss xs =
- case xs of
- [] -> T.do
- r <- tcExpr Nothing eret
- T.return (reverse rss, r)
- as : ss ->
- case as of
- SBind p a -> T.do
- v <- newUVar
- (ea, _) <- tcExpr (Just $ tApp (tList loc) v) a
- tcPat v p $ \ ep ->
- doStmts (SBind ep ea : rss) ss
- SThen a -> T.do
- (ea, _) <- tcExpr (Just (tBool (getSLocExpr a))) a
- doStmts (SThen ea : rss) ss
- SLet bs ->
- tcBinds bs $ \ ebs ->
- doStmts (SLet ebs : rss) ss
- (rss, (ea, ta)) <- doStmts [] ass
- let
- tr = tApp (tList loc) ta
- munify loc mt tr
- T.return (EListish (LCompr ea rss), tr)
--}
- LFrom e -> tcRho (enum loc "From" [e]) exp_ty
- LFromTo e1 e2 -> tcRho (enum loc "FromTo" [e1, e2]) exp_ty
- LFromThen e1 e2 -> tcRho (enum loc "FromThen" [e1,e2]) exp_ty
- LFromThenTo e1 e2 e3 -> tcRho (enum loc "FromThenTo" [e1,e2,e3]) exp_ty
-tcRho (ESign body ann_ty) exp_ty = T.do
- body' <- checkSigma body ann_ty
- instSigma noSLoc ann_ty exp_ty
- T.return body'
-tcRho (EAt _i _e) _ = impossible
-tcRho (EForall vks t) exp_ty =
- withVks vks kType $ \ vvks _ -> T.do
- t' <- withVars vvks (tcRho t exp_ty)
- T.return (EForall vvks t')
-tcRho _ _ = impossible
-
-tcLitRho :: SLoc -> Lit -> Expected -> Tc ()
-tcLitRho loc l exp_ty = T.do
- let
- lit t = instSigma loc t exp_ty
- case l of
- LInt _ -> lit (tConI loc "Primitives.Int")
- LDouble _ -> lit (tConI loc "Primitives.Double")
- LChar _ -> lit (tConI loc "Primitives.Char")
- LStr _ -> lit (tApp (tConI loc "Data.List.[]") (tConI loc "Primitives.Char"))
- LPrim _ -> newUVar T.>>= lit
- LForImp _ -> impossible
-
-tcLamRho :: EPat -> Expr -> Expected -> Tc (EPat, Expr)
-tcLamRho pat body (Infer ref) = T.do
- (binds, pat_ty) <- inferPat pat
- (body', body_ty) <- extendVarEnvList binds (inferRho body)
- writeTcRef ref (pat_ty `tArrow` body_ty)
- T.return (pat, body')
-tcLamRho pat body (Check ty) = T.do
- (arg_ty, res_ty) <- unifyFun noSLoc ty
- binds <- checkPat pat arg_ty
- body' <- extendVarEnvList binds (checkRho body res_ty)
- T.return (pat, body')
-
-checkPat :: EPat -> Sigma -> Tc [(Ident, Sigma)]
-checkPat p exp_ty = tcPatRho p (Check exp_ty)
-
-inferPat :: EPat -> Tc ([(Ident, Sigma)], Sigma)
-inferPat pat = T.do
- ref <- newTcRef (error "inferPat: empty result")
- binds <- tcPatRho pat (Infer ref)
- ty <- readTcRef ref
- T.return (binds, ty)
-
-tcPatRho :: EPat -> Expected -> Tc [(Ident,Sigma)]
-tcPatRho (EVar i) _exp_ty | isUnderscore i = T.return []
-tcPatRho econ exp_ty | Just (con, ps) <- getConApp econ = T.do
- (arg_tys, res_ty) <- instDataCon con
- let check_arg (p, ty) = checkPat p ty
- check (length ps == length arg_tys) "Bad constructor pattern"
- envs <- T.mapM check_arg (ps `zip` arg_tys)
- instPatSigma res_ty exp_ty
- T.return (concat envs)
-tcPatRho (EVar v) (Infer ref) = T.do
- ty <- newUVar
- writeTcRef ref ty
- T.return [(v,ty)]
-tcPatRho (EVar v) (Check ty) =
- T.return [(v, ty)]
-tcPatRho (ESign p pat_ty) exp_ty = T.do
- binds <- checkPat p pat_ty
- instPatSigma pat_ty exp_ty
- T.return binds
-tcPatRho _ _ = impossible
-
-instPatSigma :: Sigma -> Expected -> Tc ()
-instPatSigma pat_ty (Infer ref) = writeTcRef ref pat_ty
-instPatSigma pat_ty (Check exp_ty) = subsCheck noSLoc exp_ty pat_ty
-
-getConApp :: Expr -> Maybe (Ident, [Expr])
-getConApp (EApp f a) | Just (con, ps) <- getConApp f = Just (con, ps ++ [a])
-getConApp (EVar i) | isConIdent i = Just (i, [])
-getConApp _ = Nothing
-
-instDataCon :: Ident -> Tc ([Sigma], Tau)
-instDataCon c = T.do
- (_, v_sigma) <- tLookup "constructor" c
- v_sigma' <- instantiate v_sigma
- T.return (argsAndRes v_sigma')
-
-argsAndRes :: Rho -> ([Sigma], Tau)
-argsAndRes t | Just (arg_ty, res_ty) <- getArrow t =
- let (arg_tys, res_ty') = argsAndRes res_ty
- in (arg_ty : arg_tys, res_ty')
-argsAndRes t = ([], t)
-
-{--checkAlts :: EAlts -> EType -> Tc EAlts
-checkAlts alts ty = tcAltsRho alts (Check ty)
-
-inferAlts :: EAlts -> Tc (EAlts, Sigma)
-inferAlts (EAlts pat alts) = T.do
- ref <- newTcRef (error "inferAlts: empty result")
- alts <- tcAltsRho pat (Infer ref)
- ty <- readTcRef ref
- T.return (alts, ty)
-
-tcAltsRho :: EAlts -> Expected -> Tc (EAlts, EType)
-tcAltsRho (EAlts alts bs) exp_ty =
- tcBindsRho bs $ \ bs' -> T.do { alts' <- T.mapM (\ a -> tcAlt a exp_ty) alts; T.return (EAlts alts' bs') }-
-tcBindsRho :: [EBind] -> ([EBind] -> Tc EAlts) -> Tc (EAlts, EType)
-tcBindsRho = undefined
--}
-
----------------
-
-unifyList :: Rho -> Tc Rho
-unifyList (EApp (EVar i) t) | eqIdent i (tListI noSLoc) = T.return t
-unifyList tau = T.do
- t <- newUVar
- unify noSLoc tau (tApp (tList noSLoc) t)
- T.return t
-
-unifyTuple :: Int -> Rho -> Tc [Rho]
-unifyTuple n tau =
- case getTuple n tau of
- Just ts -> T.return ts
- Nothing -> T.do
- ts <- sequence (replicate n newUVar)
- let con = tupleConstr builtinLoc n
- unify noSLoc tau $ tApps con ts
- T.return ts
--}
-
-{--unifyFun :: SLoc -> Rho -> Tc (Sigma, Rho)
--- (arg,res) <- unifyFunTy fun
--- unifies 'fun' with '(arg -> res)'
-unifyFun loc tau =
- case getArrow tau of
- Just tt -> T.return tt
- Nothing -> T.do
- arg_ty <- newUVar
- res_ty <- newUVar
- unify loc tau (arg_ty `tArrow` res_ty)
- T.return (arg_ty, res_ty)
--}
-
-subsCheck :: SLoc -> Sigma -> Sigma -> Tc ()
--- (subsCheck args off exp) checks that
--- 'off' is at least as polymorphic as 'args -> exp'
-subsCheck loc sigma1 sigma2 = T.do -- Rule DEEP-SKOL
- (skol_tvs, rho2) <- skolemise sigma2
- subsCheckRho loc sigma1 rho2
- esc_tvs <- getFreeTyVars [sigma1,sigma2]
- let bad_tvs = filter (\ i -> elemBy eqIdent i esc_tvs) skol_tvs
- T.when (not (null bad_tvs)) $
- tcError loc "Subsumption check failed"
-
-subsCheckRho :: SLoc -> Sigma -> Rho -> Tc ()
--- Invariant: the second argument is in weak-prenex form
+subsCheckRho :: SLoc -> Sigma -> Rho -> T ()
subsCheckRho loc sigma1@(EForall _ _) rho2 = T.do -- Rule SPEC
rho1 <- tInst sigma1
subsCheckRho loc rho1 rho2
@@ -1844,36 +1449,12 @@
subsCheckRho loc tau1 tau2 -- Rule MONO
= unify loc tau1 tau2 -- Revert to ordinary unification
-subsCheckFun :: SLoc -> Sigma -> Rho -> Sigma -> Rho -> Tc ()
+subsCheckFun :: SLoc -> Sigma -> Rho -> Sigma -> Rho -> T ()
subsCheckFun loc a1 r1 a2 r2 = T.do
subsCheck loc a2 a1
subsCheckRho loc r1 r2
---instantiate :: Sigma -> Tc Rho
---instantiate = tInst
-
-{--instantiate :: Sigma -> Tc Rho
--- Instantiate the topmost for-alls of the argument type
--- with flexible type variables
-instantiate (EForall tvs ty) = T.do
- tvs' <- T.mapM (\_ -> newUVar) tvs
- T.return (substTy (map idKindIdent tvs) tvs' ty)
-instantiate ty =
- T.return ty
-
-instSigma :: SLoc -> Sigma -> Expected -> Tc ()
--- Invariant: if the second argument is (Check rho),
--- then rho is in weak-prenex form
-instSigma loc t1 (Check t2) = subsCheckRho loc t1 t2
-instSigma _ t1 (Infer r) = T.do
- t1' <- instantiate t1
- writeTcRef r t1'
--}
-
-instSigma :: SLoc -> Sigma -> Expected -> Tc ()
--- Invariant: if the second argument is (Check rho),
--- then rho is in weak-prenex form
+instSigma :: SLoc -> Sigma -> Expected -> T ()
instSigma loc t1 (Check t2) = subsCheckRho loc t1 t2
instSigma _ t1 (Infer r) = T.do
t1' <- tInst t1
--- a/tests/Rank2.hs
+++ b/tests/Rank2.hs
@@ -7,7 +7,14 @@
g :: (forall a . a -> Int -> a) -> (Int, Bool)
g c = (c 1 1, c True 1)
+data Id = Id (forall a . a -> a)
+
+iD :: Id
+iD = Id (\ x -> x)
+
main :: IO ()
main = do
putStrLn $ showPair showInt showBool $ f id
putStrLn $ showPair showInt showBool $ g const
+ case iD of
+ Id i -> showPair showInt showBool (i 1, i True)
--
⑨