ref: d3bcabcd08f9ab9669f170a78311e9bcc5743b73
parent: dbdb80b7bb46c4169cb3812a3f0ac3f239a50ce4
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Sat Oct 7 05:09:35 EDT 2023
Temp
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v3.5
-945
-(($A :0 _829) (($A :1 (($B _875) _0)) (($A :2 ((($S' _875) _0) $I)) (($A :3 _799) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _828) (($C _74) _5))) (($A :7 ((($C' _6) (_846 _71)) ((_74 _844) _70))) (($A :8 (($B (($S _875) _844)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_74 _186)) _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 _757)))) (($A :18 (($B (_73 _9)) ($BK ($P _757)))) (($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 _757)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _757))) (($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 _804) (($A :35 _805) (($A :36 ((($S' _27) (_796 97)) (($C _796) 122))) (($A :37 ((($S' _27) (_796 65)) (($C _796) 90))) (($A :38 ((($S' _26) _36) _37)) (($A :39 ((($S' _27) (_796 48)) (($C _796) 57))) (($A :40 ((($S' _27) (_796 32)) (($C _796) 126))) (($A :41 _793) (($A :42 _794) (($A :43 _796) (($A :44 _795) (($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 (((_756 "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 (((_756 "lib/Data/Char.hs") 3) 8)))) (($B _34) ((($C' _81) ((($C' _82) _35) (_35 97))) (_35 65))))) (($A :48 _764) (($A :49 _765) (($A :50 _766) (($A :51 _767) (($A :52 (_49 %0.0)) (($A :53 _48) (($A :54 _49) (($A :55 _50) (($A :56 _51) (($A :57 _768) (($A :58 _769) (($A :59 _57) (($A :60 _58) (($A :61 _770) (($A :62 _771) (($A :63 _772) (($A :64 _773) (($A :65 _61) (($A :66 _62) (($A :67 _63) (($A :68 _64) (($A :69 _774) (($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 _800) (($A :79 (($C (($C $S') _186)) _187)) (($A :80 ((($C' ($S' ($C' $B))) $B) $I)) (($A :81 _758) (($A :82 _759) (($A :83 _760) (($A :84 _761) (($A :85 _762) (($A :86 _763) (($A :87 (_82 0)) (($A :88 _781) (($A :89 _782) (($A :90 _783) (($A :91 _784) (($A :92 _785) (($A :93 _786) (($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 _175)) ((($C' ($C' $B)) ((($C' $C) _88) _175)) _176))) (($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
+965
+(($A :0 _849) (($A :1 (($B _895) _0)) (($A :2 ((($S' _895) _0) $I)) (($A :3 _819) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _848) (($C _74) _5))) (($A :7 ((($C' _6) (_866 _71)) ((_74 _864) _70))) (($A :8 (($B (($S _895) _864)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_74 _187)) _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 _777)))) (($A :18 (($B (_73 _9)) ($BK ($P _777)))) (($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 _777)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _777))) (($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 _824) (($A :35 _825) (($A :36 ((($S' _27) (_816 97)) (($C _816) 122))) (($A :37 ((($S' _27) (_816 65)) (($C _816) 90))) (($A :38 ((($S' _26) _36) _37)) (($A :39 ((($S' _27) (_816 48)) (($C _816) 57))) (($A :40 ((($S' _27) (_816 32)) (($C _816) 126))) (($A :41 _813) (($A :42 _814) (($A :43 _816) (($A :44 _815) (($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 (((_776 "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 (((_776 "lib/Data/Char.hs") 3) 8)))) (($B _34) ((($C' _81) ((($C' _82) _35) (_35 97))) (_35 65))))) (($A :48 _784) (($A :49 _785) (($A :50 _786) (($A :51 _787) (($A :52 (_49 %0.0)) (($A :53 _48) (($A :54 _49) (($A :55 _50) (($A :56 _51) (($A :57 _788) (($A :58 _789) (($A :59 _57) (($A :60 _58) (($A :61 _790) (($A :62 _791) (($A :63 _792) (($A :64 _793) (($A :65 _61) (($A :66 _62) (($A :67 _63) (($A :68 _64) (($A :69 _794) (($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 _820) (($A :79 (($C (($C $S') _187)) _188)) (($A :80 ((($C' ($S' ($C' $B))) $B) $I)) (($A :81 _778) (($A :82 _779) (($A :83 _780) (($A :84 _781) (($A :85 _782) (($A :86 _783) (($A :87 (_82 0)) (($A :88 _801) (($A :89 _802) (($A :90 _803) (($A :91 _804) (($A :92 _805) (($A :93 _806) (($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 _175)) ((($C' ($C' $B)) ((($C' $C) _88) _175)) _176))) (($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/lib/Data/Maybe.hs
+++ b/lib/Data/Maybe.hs
@@ -2,6 +2,7 @@
-- See LICENSE file for full license.
module Data.Maybe(module Data.Maybe) where
import Primitives
+import Data.Bool
data Maybe a = Nothing | Just a
@@ -19,6 +20,10 @@
catMaybes :: forall a . [Maybe a] -> [a]
catMaybes mxs = [ x | Just x <- mxs ]
+
+isJust :: forall a . Maybe a -> Bool
+isJust Nothing = False
+isJust (Just _) = True
{-mapMaybe is in Data.List to avoid recursive modules
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -7,6 +7,7 @@
impossible,
) where
import Prelude
+import Data.Char
import Data.List
import Data.Maybe
import qualified Data.IntMap as IM
@@ -33,8 +34,8 @@
data Entry = Entry Expr ETypeScheme
--Xderiving(Show)
---entryType :: Entry -> ETypeScheme
---entryType (Entry _ t) = t
+entryType :: Entry -> ETypeScheme
+entryType (Entry _ t) = t
type ValueTable = M.Map [Entry]
type TypeTable = M.Map [Entry]
@@ -371,18 +372,19 @@
kArrow :: EKind -> EKind -> EKind
kArrow = tArrow
+isArrow :: EType -> Bool
+isArrow = isJust . getArrow
+
getArrow :: EType -> Maybe (EType, EType)
getArrow (EApp (EApp (EVar n) a) b) =
if eqIdent n (mkIdent "->") || eqIdent n (mkIdent "Primitives.->") then Just (a, b) else Nothing
getArrow _ = Nothing
-{-getTuple :: Int -> EType -> Maybe [EType]
getTuple n t = loop t []
where loop (EVar i) r | isTupleConstr n i && length r == n = Just (reverse r)
loop (EApp f a) r = loop f (a:r)
loop _ _ = Nothing
--}
addUVar :: Int -> EType -> T ()
addUVar i t = T.do
@@ -532,7 +534,7 @@
if null vks then T.return t
else T.do
let vs = map idKindIdent vks
- us <- T.mapM (const newUVar) (replicate (length vs) ())
+ us <- T.mapM (const newUVar) vks
T.return (subst (zip vs us) t)
t -> T.return t
@@ -809,6 +811,19 @@
Nothing -> putUvarSubst (IM.insert ref t m)
Just _ -> error "tSetRefType"
+-- Get the type of an already set Expected
+tGetExpType :: Expected -> T EType
+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
+ t <- newUVar
+ tSetRefType r t
+ T.return t
+
tcExpr :: --XHasCallStack =>
Expected -> Expr -> T Expr
tcExpr mt ae = T.do
@@ -923,8 +938,7 @@
SBind p a -> T.do
v <- newUVar
ea <- tCheckExpr (tApp (tList loc) v) a
- tcPat v p $ \ ep ->
- doStmts (SBind ep ea : rss) ss
+ tcPatE (Check v) p $ \ ep -> doStmts (SBind ep ea : rss) ss
SThen a -> T.do
ea <- tCheckExpr (tBool (getSLocExpr a)) a
doStmts (SThen ea : rss) ss
@@ -948,9 +962,7 @@
EAt i e -> T.do
(_, ti) <- tLookupInst "impossible!" i
e' <- tcExpr mt e
- tt <- case mt of
- Check t -> T.return t
- Infer ref -> tGetRefType ref
+ tt <- tGetExpType mt
unify loc tt ti
T.return (EAt i e')
EForall vks t ->
@@ -1033,18 +1045,18 @@
getFixity :: FixTable -> Ident -> Fixity
getFixity fixs i = fromMaybe (AssocLeft, 9) $ M.lookup i fixs
-tcPats :: forall a . EType -> [EPat] -> (EType -> [Typed EPat] -> T a) -> T a
+tcPats :: forall a . EType -> [EPat] -> (EType -> [EPat] -> T a) -> T a
tcPats t [] ta = ta t []
tcPats t (p:ps) ta = T.do
(tp, tr) <- unArrow (getSLocExpr p) t
- tcPat tp p $ \ pp -> tcPats tr ps $ \ tt pps -> ta tt ((pp, tp) : pps)
+ tcPat tp p $ \ pp -> tcPats tr ps $ \ tt pps -> ta tt (pp : pps)
tcExprLam :: Expected -> [EPat] -> Expr -> T Expr
tcExprLam mt aps expr = T.do
t <- unMType mt
- tcPats t aps $ \ tt pts -> T.do
+ tcPats t aps $ \ tt ps -> T.do
er <- tCheckExpr tt expr
- T.return (ELam (map fst pts) er)
+ T.return (ELam ps er)
tcEqns :: EType -> [Eqn] -> T [Eqn]
tcEqns t eqns = T.mapM (tcEqn t) eqns
@@ -1052,9 +1064,9 @@
tcEqn :: EType -> Eqn -> T Eqn
tcEqn t eqn =
case eqn of
- Eqn ps alts -> tcPats t ps $ \ tt tps -> T.do
+ Eqn ps alts -> tcPats t ps $ \ tt ps' -> T.do
aalts <- tcAlts tt alts
- T.return (Eqn (map fst tps) aalts)
+ T.return (Eqn ps' aalts)
tcAlts :: EType -> EAlts -> T EAlts
tcAlts tt (EAlts alts bs) =
@@ -1070,7 +1082,7 @@
tcGuard :: forall a . EStmt -> (EStmt -> T a) -> T a
tcGuard (SBind p e) ta = T.do
(ee, tt) <- tInferExpr e
- tcPat tt p $ \ pp -> ta (SBind pp ee)
+ tcPatE (Check tt) p $ \ pp -> ta (SBind pp ee)
tcGuard (SThen e) ta = T.do
ee <- tCheckExpr (tBool (getSLocExpr e)) e
ta (SThen ee)
@@ -1079,11 +1091,88 @@
tcArm :: EType -> EType -> ECaseArm -> T ECaseArm
tcArm t tpat arm =
case arm of
- (p, alts) -> tcPat tpat p $ \ pp -> T.do
+ (p, alts) -> tcPatE (Check tpat) p $ \ pp -> T.do
aalts <- tcAlts t alts
T.return (pp, aalts)
-tcPat ::forall a . EType -> EPat -> (EPat -> T a) -> T a
+tInferPatE :: forall a . --XHasCallStack =>
+ EPat -> (EPat -> EType -> T a) -> T a
+tInferPatE p ta = T.do
+ r <- newUniq
+ tcPatE (Infer r) p $ \ p' -> T.do
+ t <- tGetRefType r
+ ta p' t
+
+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 =>
+ SLoc -> Sigma -> Expected -> T ()
+instPatSigmaE _ pt (Infer r) = tSetRefType r pt
+instPatSigmaE loc pt (Check t) = subsCheckE loc t pt
+
+subsCheckE :: --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
+ (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"
+
+tcPat :: forall a . EType -> EPat -> (EPat -> T a) -> T a
tcPat t p@(EVar v) ta | not (isConIdent v) = T.do -- simple special case
withExtVals [(v, t)] $ ta p
tcPat t ap ta = T.do
@@ -1185,7 +1274,6 @@
-}
-----------------------------------------------------
-{-type Sigma = EType
type Tau = EType
@@ -1192,12 +1280,14 @@
type Rho = EType
type TyVar = Ident
+type Tc a = T a
+
+{-+
type TcRef = Int
--data Expected = Infer TcRef | Check EType
type MetaTv = TcRef
-type Tc a = T a
-
xtypecheck :: EType -> Tc Sigma
xtypecheck e = T.do
(ty, _) <- inferSigma e
@@ -1216,6 +1306,7 @@
Nothing -> error "readTcRef"
writeTcRef :: TcRef -> EType -> Tc ()
writeTcRef r t = addUVar r t
+-}
getFreeTyVars :: [EType] -> Tc [TyVar]
getFreeTyVars tys = T.do
@@ -1222,6 +1313,7 @@
tys' <- T.mapM zonkType tys
T.return (freeTyVars tys')
+{-getMetaTyVars :: [EType] -> Tc [MetaTv]
getMetaTyVars tys = T.do
tys' <- T.mapM zonkType tys
@@ -1229,6 +1321,7 @@
getEnvTypes :: Tc [EType]
getEnvTypes = gets (map entryType . concat . M.elems . valueTable)
+-}
zonkType :: EType -> Tc EType
zonkType (EForall ns ty) = T.do
@@ -1241,7 +1334,8 @@
Nothing -> T.return t
Just ty -> T.do
ty' <- zonkType ty
- writeTcRef tv ty' -- "Short out" multiple hops
+ --writeTcRef tv ty' -- "Short out" multiple hops
+ addUVar tv ty'
T.return ty'
zonkType (EApp arg res) = T.do
arg' <- zonkType arg
@@ -1249,6 +1343,7 @@
T.return (EApp arg' res')
zonkType _ = undefined
+{-quantify :: [MetaTv] -> Rho -> Tc Sigma
-- Quantify over the specified type variables (all flexible)
quantify tvs ty = T.do
@@ -1262,21 +1357,27 @@
new_bndrs_kind = map (\ i -> IdKind i undefined) new_bndrs
allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,...
-allBinders = [ mkIdent [x] | x <- ['a'..'z'] ] ++
- [ mkIdent (x : showInt i) | i <- [1 ..], x <- ['a'..'z']]
+allBinders = [ mkIdent [chr x] | x <- [ord 'a' .. ord 'z'] ] ++
+ [ mkIdent (chr x : showInt i) | i <- [1 ..], x <- [ord 'a' .. ord 'z']]
+-}
-skolemise :: Sigma -> Tc ([TyVar], Rho)
--- Performs deep skolemisation, retuning the
+skolemise :: --XHasCallStack =>
+ Sigma -> Tc ([TyVar], Rho)
+-- Performs deep skolemisation, returning the
-- skolem constants and the skolemised type
skolemise (EForall tvs ty) = T.do -- Rule PRPOLY
sks1 <- T.mapM (newSkolemTyVar . idKindIdent) tvs
- (sks2, ty') <- skolemise (substTy (map idKindIdent tvs) (map EVar sks1) ty)
+ (sks2, ty') <- skolemise (subst (zip (map idKindIdent tvs) (map EVar sks1)) ty)
T.return (sks1 ++ sks2, ty')
-skolemise (EApp arg_ty res_ty) = T.do -- Rule PRFUN
+skolemise t@(EApp _ _) | Just (arg_ty, res_ty) <- getArrow t = T.do -- Rule PRFUN
(sks, res_ty') <- skolemise res_ty
- T.return (sks, EApp arg_ty res_ty')
-skolemise ty@(EVar _) = T.return ([], ty) -- Rule PRMONO
-skolemise _ty = undefined
+ T.return (sks, arg_ty `tArrow` res_ty')
+skolemise (EApp f a) = T.do
+ (sks1, f') <- skolemise f
+ (sks2, a') <- skolemise a
+ T.return (sks1 ++ sks2, EApp f' a')
+skolemise ty =
+ T.return ([], ty) -- Rule PRMONO
-- Skolem tyvars are just identifiers that start with a uniq
newSkolemTyVar :: Ident -> Tc Ident
@@ -1284,7 +1385,8 @@
uniq <- newUniq
T.return (mkIdentSLoc (getSLocIdent tv) (showInt uniq ++ unIdent tv))
-extendVarEnvList :: [(Ident, Sigma)] -> Tc a -> Tc a
+{-+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)
@@ -1293,6 +1395,7 @@
T.return a
------------------
+-}
freeTyVars :: [EType] -> [TyVar]
-- Get the free TyVars from a type; no duplicates in result
@@ -1311,6 +1414,7 @@
go _bound (EUVar _) acc = acc
go _ _ _ = undefined
+{-metaTvs :: [EType] -> [MetaTv]
-- Get the MetaTvs from a type; no duplicates in result
metaTvs tys = foldr go [] tys
@@ -1390,13 +1494,13 @@
tcRho :: Expr -> Expected -> Tc Expr
tcRho (EVar v) exp_ty = T.do
(expr', v_sigma) <- tLookup "variable" v
- instSigma v_sigma exp_ty
+ 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 fun_ty
+ (arg_ty, res_ty) <- unifyFun noSLoc fun_ty
arg' <- checkSigma arg arg_ty
- instSigma res_ty exp_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
@@ -1406,6 +1510,7 @@
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
@@ -1425,6 +1530,7 @@
mapM_ (\ r -> do { subsCheck rho r; subsCheck r rho }) rhoswriteTcRef 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
@@ -1449,8 +1555,8 @@
e1' <- checkRho e1 (tBool (getSLocExpr e1))
(e2', rho1) <- inferRho e2
(e3', rho2) <- inferRho e3
- subsCheck rho1 rho2
- subsCheck rho2 rho1
+ 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
@@ -1505,7 +1611,7 @@
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 ann_ty exp_ty
+ instSigma noSLoc ann_ty exp_ty
T.return body'
tcRho (EAt _i _e) _ = impossible
tcRho (EForall vks t) exp_ty =
@@ -1517,7 +1623,7 @@
tcLitRho :: SLoc -> Lit -> Expected -> Tc ()
tcLitRho loc l exp_ty = T.do
let
- lit t = instSigma t exp_ty
+ lit t = instSigma loc t exp_ty
case l of
LInt _ -> lit (tConI loc "Primitives.Int")
LDouble _ -> lit (tConI loc "Primitives.Double")
@@ -1533,7 +1639,7 @@
writeTcRef ref (pat_ty `tArrow` body_ty)
T.return (pat, body')
tcLamRho pat body (Check ty) = T.do
- (arg_ty, res_ty) <- unifyFun ty
+ (arg_ty, res_ty) <- unifyFun noSLoc ty
binds <- checkPat pat arg_ty
body' <- extendVarEnvList binds (checkRho body res_ty)
T.return (pat, body')
@@ -1571,7 +1677,7 @@
instPatSigma :: Sigma -> Expected -> Tc ()
instPatSigma pat_ty (Infer ref) = writeTcRef ref pat_ty
-instPatSigma pat_ty (Check exp_ty) = subsCheck exp_ty 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])
@@ -1590,11 +1696,12 @@
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 alts = T.do
+inferAlts (EAlts pat alts) = T.do
ref <- newTcRef (error "inferAlts: empty result")
alts <- tcAltsRho pat (Infer ref)
ty <- readTcRef ref
@@ -1604,6 +1711,10 @@
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
@@ -1622,49 +1733,55 @@
let con = tupleConstr builtinLoc n
unify noSLoc tau $ tApps con ts
T.return ts
+-}
-unifyFun :: Rho -> Tc (Sigma, Rho)
+unifyFun :: SLoc -> Rho -> Tc (Sigma, Rho)
-- (arg,res) <- unifyFunTy fun
-- unifies 'fun' with '(arg -> res)'
-unifyFun tau =
+unifyFun loc tau =
case getArrow tau of
Just tt -> T.return tt
Nothing -> T.do
arg_ty <- newUVar
res_ty <- newUVar
- unify noSLoc tau (arg_ty `tArrow` res_ty)
+ unify loc tau (arg_ty `tArrow` res_ty)
T.return (arg_ty, res_ty)
-subsCheck :: Sigma -> Sigma -> Tc ()
+subsCheck :: SLoc -> Sigma -> Sigma -> Tc ()
-- (subsCheck args off exp) checks that
-- 'off' is at least as polymorphic as 'args -> exp'
-subsCheck sigma1 sigma2 = T.do -- Rule DEEP-SKOL
+subsCheck loc sigma1 sigma2 = T.do -- Rule DEEP-SKOL
(skol_tvs, rho2) <- skolemise sigma2
- subsCheckRho sigma1 rho2
+ subsCheckRho loc sigma1 rho2
esc_tvs <- getFreeTyVars [sigma1,sigma2]
let bad_tvs = filter (\ i -> elemBy eqIdent i esc_tvs) skol_tvs
- check (null bad_tvs) "Subsumption check failed"
+ T.when (not (null bad_tvs)) $
+ tcError loc "Subsumption check failed"
-subsCheckRho :: Sigma -> Rho -> Tc ()
+subsCheckRho :: SLoc -> Sigma -> Rho -> Tc ()
-- Invariant: the second argument is in weak-prenex form
-subsCheckRho sigma1@(EForall _ _) rho2 = T.do -- Rule SPEC
+subsCheckRho loc sigma1@(EForall _ _) rho2 = T.do -- Rule SPEC
rho1 <- instantiate sigma1
- subsCheckRho rho1 rho2
-subsCheckRho rho1 rho2 | Just (a2, r2) <- getArrow rho2 = T.do -- Rule FUN
- (a1, r1) <- unifyFun rho1
- subsCheckFun a1 r1 a2 r2
-subsCheckRho rho1 rho2 | Just (a1, r1) <- getArrow rho1 = T.do -- Rule FUN
- (a2,r2) <- unifyFun rho2
- subsCheckFun a1 r1 a2 r2
-subsCheckRho tau1 tau2 -- Rule MONO
- = unify noSLoc tau1 tau2 -- Revert to ordinary unification
+ subsCheckRho loc rho1 rho2
+subsCheckRho loc rho1 rho2 | Just (a2, r2) <- getArrow rho2 = T.do -- Rule FUN
+ (a1, r1) <- unifyFun loc rho1
+ subsCheckFun loc a1 r1 a2 r2
+subsCheckRho loc rho1 rho2 | Just (a1, r1) <- getArrow rho1 = T.do -- Rule FUN
+ (a2,r2) <- unifyFun loc rho2
+ subsCheckFun loc a1 r1 a2 r2
+subsCheckRho loc tau1 tau2 -- Rule MONO
+ = unify loc tau1 tau2 -- Revert to ordinary unification
-subsCheckFun :: Sigma -> Rho -> Sigma -> Rho -> Tc ()
-subsCheckFun a1 r1 a2 r2 = T.do
- subsCheck a2 a1
- subsCheckRho r1 r2
+subsCheckFun :: SLoc -> Sigma -> Rho -> Sigma -> Rho -> Tc ()
+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
@@ -1673,11 +1790,11 @@
instantiate ty =
T.return ty
-instSigma :: Sigma -> Expected -> Tc ()
+instSigma :: SLoc -> Sigma -> Expected -> Tc ()
-- Invariant: if the second argument is (Check rho),
-- then rho is in weak-prenex form
-instSigma t1 (Check t2) = subsCheckRho t1 t2
-instSigma t1 (Infer r) = T.do
+instSigma loc t1 (Check t2) = subsCheckRho loc t1 t2
+instSigma _ t1 (Infer r) = T.do
t1' <- instantiate t1
writeTcRef r t1'
-}
--
⑨