ref: b4d42894068af095ff3f39096d72b5c1b6c2d971
parent: d3bcabcd08f9ab9669f170a78311e9bcc5743b73
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Sun Oct 8 13:49:21 EDT 2023
More steps towards rank-n
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v3.5
-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
+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
--- a/lib/Data/List.hs
+++ b/lib/Data/List.hs
@@ -311,3 +311,7 @@
init [] = error "init: []"
init [_] = []
init (x:xs) = x : init xs
+
+anySameBy :: forall a . (a -> a -> Bool) -> [a] -> Bool
+anySameBy _ [] = False
+anySameBy eq (x:xs) = elemBy eq x xs || anySameBy eq xs
--- a/src/Compat.hs
+++ b/src/Compat.hs
@@ -204,3 +204,7 @@
compareString :: String -> String -> Ordering
compareString = compare
+
+anySameBy :: (a -> a -> Bool) -> [a] -> Bool
+anySameBy _ [] = False
+anySameBy eq (x:xs) = elemBy eq x xs || anySameBy eq xs
--- a/src/MicroHs/Expr.hs
+++ b/src/MicroHs/Expr.hs
@@ -22,7 +22,7 @@
LHS,
Constr,
ConTyInfo,
- Con(..), conIdent, conArity, eqCon,
+ Con(..), conIdent, conArity, eqCon, getSLocCon,
tupleConstr, untupleConstr, isTupleConstr,
subst,
allVarsExpr, allVarsBind,
@@ -309,6 +309,11 @@
-- XXX Should use locations in ELit
getSLocExpr :: Expr -> SLoc
getSLocExpr e = head $ filter (not . isNoSLoc) (map getSLocIdent (allVarsExpr e)) ++ [noSLoc]
+
+getSLocCon :: Con -> SLoc
+getSLocCon (ConData _ i) = getSLocIdent i
+getSLocCon (ConNew i) = getSLocIdent i
+getSLocCon _ = noSLoc
setSLocExpr :: SLoc -> Expr -> Expr
setSLocExpr l (EVar i) = EVar (setSLocIdent l i)
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -237,55 +237,74 @@
type Typed a = (a, EType)
-data TCState = TC IdentModule Int FixTable TypeTable SynTable ValueTable (IM.IntMap EType)
+data TCState = TC IdentModule Int FixTable TypeTable SynTable ValueTable (IM.IntMap EType) TCMode
--Xderiving (Show)
+data TCMode = TCExpr | TCPat | TCType
+ --Xderiving (Show)
+
typeTable :: TCState -> TypeTable
-typeTable (TC _ _ _ tt _ _ _) = tt
+typeTable (TC _ _ _ tt _ _ _ _) = tt
valueTable :: TCState -> ValueTable
-valueTable (TC _ _ _ _ _ vt _) = vt
+valueTable (TC _ _ _ _ _ vt _ _) = vt
synTable :: TCState -> SynTable
-synTable (TC _ _ _ _ st _ _) = st
+synTable (TC _ _ _ _ st _ _ _) = st
fixTable :: TCState -> FixTable
-fixTable (TC _ _ ft _ _ _ _) = ft
+fixTable (TC _ _ ft _ _ _ _ _) = ft
uvarSubst :: TCState -> IM.IntMap EType
-uvarSubst (TC _ _ _ _ _ _ sub) = sub
+uvarSubst (TC _ _ _ _ _ _ sub _) = sub
moduleName :: TCState -> IdentModule
-moduleName (TC mn _ _ _ _ _ _) = mn
+moduleName (TC mn _ _ _ _ _ _ _) = mn
+tcMode :: TCState -> TCMode
+tcMode (TC _ _ _ _ _ _ _ m) = m
+
putValueTable :: ValueTable -> T ()
putValueTable venv = T.do
- TC mn n fx tenv senv _ m <- get
- put (TC mn n fx tenv senv venv m)
+ TC mn n fx tenv senv _ sub m <- get
+ put (TC mn n fx tenv senv venv sub m)
putTypeTable :: TypeTable -> T ()
putTypeTable tenv = T.do
- TC mn n fx _ senv venv m <- get
- put (TC mn n fx tenv senv venv m)
+ TC mn n fx _ senv venv sub m <- get
+ put (TC mn n fx tenv senv venv sub m)
putSynTable :: SynTable -> T ()
putSynTable senv = T.do
- TC mn n fx tenv _ venv m <- get
- put (TC mn n fx tenv senv venv m)
+ TC mn n fx tenv _ venv sub m <- get
+ put (TC mn n fx tenv senv venv sub m)
putUvarSubst :: IM.IntMap EType -> T ()
-putUvarSubst m = T.do
- TC mn n fx tenv senv venv _ <- get
- put (TC mn n fx tenv senv venv m)
+putUvarSubst sub = T.do
+ TC mn n fx tenv senv venv _ m <- get
+ put (TC mn n fx tenv senv venv sub m)
+putTCMode :: TCMode -> T ()
+putTCMode m = T.do
+ TC mn n fx tenv senv venv sub _ <- get
+ put (TC mn n fx tenv senv venv sub m)
+
+withTCMode :: forall a . TCMode -> T a -> T a
+withTCMode m ta = T.do
+ om <- gets tcMode
+ putTCMode m
+ a <- ta
+ putTCMode om
+ T.return a
+
-- Use the type table as the value table, and the primKind table as the type table.
withTypeTable :: forall a . T a -> T a
withTypeTable ta = T.do
- TC mn n fx tt st vt m <- get
- put (TC mn n fx primKindTable M.empty tt m)
+ TC mn n fx tt st vt sub m <- get
+ put (TC mn n fx primKindTable M.empty tt sub m)
a <- ta
- TC mnr nr _ _ _ ttr mr <- get
- put (TC mnr nr fx ttr st vt mr)
+ TC mnr nr _ _ _ ttr subr mr <- get
+ put (TC mnr nr fx ttr st vt subr mr)
T.return a
initTC :: IdentModule -> FixTable -> TypeTable -> SynTable -> ValueTable -> TCState
@@ -294,7 +313,7 @@
let
xts = foldr (uncurry M.insert) ts primTypes
xvs = foldr (uncurry M.insert) vs primValues
- in TC mn 1 fs xts ss xvs IM.empty
+ in TC mn 1 fs xts ss xvs IM.empty TCExpr
kTypeS :: ETypeScheme
kTypeS = kType
@@ -372,8 +391,10 @@
kArrow :: EKind -> EKind -> EKind
kArrow = tArrow
+{-isArrow :: EType -> Bool
isArrow = isJust . getArrow
+-}
getArrow :: EType -> Maybe (EType, EType)
getArrow (EApp (EApp (EVar n) a) b) =
@@ -380,18 +401,20 @@
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
let
add = T.do
- TC mn n fx tenv senv venv sub <- get
- put (TC mn n fx tenv senv venv (IM.insert i t sub))
+ 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
@@ -495,8 +518,8 @@
-- Reset type variable and unification map
tcReset :: T ()
tcReset = T.do
- TC mn _ fx tenv senv venv _ <- get
- put (TC mn 0 fx tenv senv venv IM.empty)
+ TC mn _ fx tenv senv venv _ m <- get
+ put (TC mn 0 fx tenv senv venv IM.empty m)
newUVar :: T EType
newUVar = EUVar <$> newUniq
@@ -505,8 +528,8 @@
newUniq :: T TRef
newUniq = T.do
- TC mn n fx tenv senv venv sub <- get
- put (TC mn (n+1) fx tenv senv venv sub)
+ TC mn n fx tenv senv venv sub m <- get
+ put (TC mn (n+1) fx tenv senv venv sub m)
T.return n
tLookupInst :: --XHasCallStack =>
@@ -573,8 +596,8 @@
extFix :: Ident -> Fixity -> T ()
extFix i fx = T.do
- TC mn n fenv tenv senv venv sub <- get
- put $ TC mn n (M.insert i fx fenv) tenv senv venv sub
+ TC mn n fenv tenv senv venv sub m <- get
+ put $ TC mn n (M.insert i fx fenv) tenv senv venv sub m
T.return ()
withExtVal :: forall a . --XHasCallStack =>
@@ -757,7 +780,7 @@
-- Kind check a type while already in type checking mode
tcTypeT :: --XHasCallStack =>
Expected -> EType -> T EType
-tcTypeT mk = tcExpr mk . dsType
+tcTypeT mk t = withTCMode TCType (tcExpr mk (dsType t))
-- Kind check a type while in value checking mode
tcType :: --XHasCallStack =>
@@ -778,7 +801,8 @@
data Expected = Infer TRef | Check EType
--Xderiving(Show)
-tInfer :: forall a . (Expected -> a -> T a) -> a -> T (Typed a)
+tInfer :: forall a . --XHasCallStack =>
+ (Expected -> a -> T a) -> a -> T (Typed a)
tInfer tc a = T.do
ref <- newUniq
a' <- tc (Infer ref) a
@@ -788,10 +812,12 @@
tCheck :: forall a . (Expected -> a -> T a) -> EType -> a -> T a
tCheck tc t = tc (Check t)
-tInferExpr :: Expr -> T (Typed Expr)
+tInferExpr :: --XHasCallStack =>
+ Expr -> T (Typed Expr)
tInferExpr = tInfer tcExpr
-tCheckExpr :: EType -> Expr -> T Expr
+tCheckExpr :: --XHasCallStack =>
+ EType -> Expr -> T Expr
tCheckExpr = tCheck tcExpr
tGetRefType :: --XHasCallStack =>
@@ -837,31 +863,55 @@
tcExprR mt ae =
let { loc = getSLocExpr ae } incase ae of
- EVar i ->
- if isUnderscore i then T.do
- -- this only happens with patterns translated into expressions
- t <- newUVar
- munify loc mt t
- T.return ae
- else T.do
- (e, t) <- tLookupInst "variable" i
- case mt of
- Check (EForall _ tt) -> T.do
- -- XXX This is wrong in many ways.
- -- Both t and tt may contain unification variables bound elsewhere.
- unify loc tt t
- T.return e
- _ -> T.do
- munify loc mt t
- T.return e
+ EVar i -> T.do
+ tcm <- gets tcMode
+ case tcm of
+ TCPat | isUnderscore i -> T.do
+ -- _ can be anything, so just ignore it
+ _ <- tGetExpTypeSet mt
+ T.return ae
+
+ | isConIdent i -> T.do
+ (p, pt) <- tLookupInst "constructor" i
+ -- We will only have an expected type for a non-nullary constructor
+ case mt of
+ Check ext -> subsCheck loc ext pt
+ Infer r -> tSetRefType 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
+ (p, t) <- tLookup "IMPOSSIBLE" i
+ case t of
+ EUVar r -> tSetRefType r ext
+ _ -> impossible
+ T.return p
+
+ _ -> T.do
+ -- Type checking an expression (or type)
+ T.when (isUnderscore i) impossible
+ (e, t) <- tLookup "variable" i
+ instSigma loc t mt
+ T.return e
+
EApp f a -> T.do
- (ef, tf) <- tInferExpr f
- (ta, tr) <- unArrow loc tf
- ea <- tCheckExpr ta a
- munify loc mt tr
- T.return (EApp ef ea)
+ (f', ft) <- tInferExpr f
+ (at, rt) <- unArrow loc ft
+ tcm <- gets tcMode
+ case tcm of
+ TCPat -> T.do
+ a' <- tCheckExpr at a
+ instPatSigmaE loc rt mt
+ T.return (EApp f' a')
+ _ -> T.do
+ a' <- checkSigma a at
+ instSigma loc rt mt
+ T.return (EApp f' a')
+
EOper e ies -> tcOper mt e ies
- ELam is e -> tcExprLam mt is e
+ ELam ps e -> tcExprLam mt ps e
ELit loc' l -> tcLit mt loc' l
ECase a arms -> T.do
(ea, ta) <- tInferExpr a
@@ -938,7 +988,7 @@
SBind p a -> T.do
v <- newUVar
ea <- tCheckExpr (tApp (tList loc) v) a
- tcPatE (Check v) p $ \ ep -> doStmts (SBind ep ea : rss) ss
+ tCheckPat v p $ \ ep -> doStmts (SBind ep ea : rss) ss
SThen a -> T.do
ea <- tCheckExpr (tBool (getSLocExpr a)) a
doStmts (SThen ea : rss) ss
@@ -955,15 +1005,22 @@
EListish (LFromThen e1 e2) -> tcExpr mt (enum loc "FromThen" [e1,e2])
EListish (LFromThenTo e1 e2 e3) -> tcExpr mt (enum loc "FromThenTo" [e1,e2,e3])
ESign e t -> T.do
- tt <- tcType (Check kType) t
- ee <- tCheckExpr tt e
- munify loc mt tt
- T.return ee
+ t' <- tcType (Check kType) t
+ tcm <- gets tcMode
+ case tcm of
+ TCPat -> T.do
+ instPatSigmaE loc t' mt
+ tCheckExpr t' e
+ _ -> T.do
+ instSigma loc t' mt
+ checkSigma e t'
EAt i e -> T.do
- (_, ti) <- tLookupInst "impossible!" i
+ (_, ti) <- tLookup "IMPOSSIBLE" i
e' <- tcExpr mt e
tt <- tGetExpType mt
- unify loc tt ti
+ case ti of
+ EUVar r -> tSetRefType r tt
+ _ -> impossible
T.return (EAt i e')
EForall vks t ->
withVks vks kType $ \ vvks _ -> T.do
@@ -985,7 +1042,8 @@
LPrim _ -> newUVar T.>>= lit -- pretend it is anything
LForImp _ -> impossible
-tcOper :: Expected -> Expr -> [(Ident, Expr)] -> T Expr
+tcOper :: --XHasCallStack =>
+ Expected -> Expr -> [(Ident, Expr)] -> T Expr
tcOper mt ae aies = T.do
let
appOp (f, ft) (e1, t1) (e2, t2) = T.do
@@ -1049,7 +1107,7 @@
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 : pps)
+ tCheckPat tp p $ \ pp -> tcPats tr ps $ \ tt pps -> ta tt (pp : pps)
tcExprLam :: Expected -> [EPat] -> Expr -> T Expr
tcExprLam mt aps expr = T.do
@@ -1082,7 +1140,7 @@
tcGuard :: forall a . EStmt -> (EStmt -> T a) -> T a
tcGuard (SBind p e) ta = T.do
(ee, tt) <- tInferExpr e
- tcPatE (Check tt) p $ \ pp -> ta (SBind pp ee)
+ tCheckPat tt p $ \ pp -> ta (SBind pp ee)
tcGuard (SThen e) ta = T.do
ee <- tCheckExpr (tBool (getSLocExpr e)) e
ta (SThen ee)
@@ -1091,18 +1149,12 @@
tcArm :: EType -> EType -> ECaseArm -> T ECaseArm
tcArm t tpat arm =
case arm of
- (p, alts) -> tcPatE (Check tpat) p $ \ pp -> T.do
+ (p, alts) -> tCheckPat tpat p $ \ pp -> T.do
aalts <- tcAlts t alts
T.return (pp, aalts)
-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 =
@@ -1154,6 +1206,7 @@
loop aps []
tcPatE _ p _ = --Xtrace ("tcPatE: " ++ show p) $impossible
+-}
instPatSigmaE :: --XHasCallStack =>
SLoc -> Sigma -> Expected -> T ()
@@ -1172,21 +1225,45 @@
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
+tCheckPat :: forall a . EType -> EPat -> (EPat -> T a) -> T a
+tCheckPat t p@(EVar v) ta | not (isConIdent v) = T.do -- simple special case
withExtVals [(v, t)] $ ta p
-tcPat t ap ta = T.do
+tCheckPat t ap ta = T.do
-- traceM $ "tcPat: " ++ show ap
- env <- T.mapM (\ v -> (v,) <$> newUVar) $ filter (not . isUnderscore) $ patVars ap
+ let vs = filter (not . isUnderscore) $ patVars ap
+ T.when (anySameBy eqIdent vs) $
+ tcError (getSLocIdent (head vs)) "Multiply defined"
+ env <- T.mapM (\ v -> (v,) <$> newUVar) vs
withExtVals env $ T.do
- pp <- tCheckExpr t ap
- () <- checkArity (getSLocExpr ap) 0 pp
+ pp <- withTCMode TCPat $ tCheckExpr t ap
+ () <- checkArity 0 pp
ta pp
-checkArity :: SLoc -> Int -> EPat -> T ()
-checkArity loc n (EApp f _) = checkArity loc (n+1) f
-checkArity loc n (ECon c) = if n == conArity c then T.return () else tcError loc ": con arity"
-checkArity _ _ _ = T.return ()
+checkArity :: Int -> EPat -> T ()
+checkArity n (EApp f a) = T.do
+ checkArity (n+1) f
+ checkArity 0 a
+checkArity n (ECon c) =
+ let a = conArity c
+ in if n < a then
+ tcError (getSLocCon c) "too few arguments"
+ else if n > a then
+ tcError (getSLocCon c) "too many arguments"
+ else
+ T.return ()
+checkArity n (EAt _ p) = checkArity n p
+checkArity n (ESign p _) = checkArity n p
+checkArity n p =
+ case p of
+ ETuple _ -> check0
+ EListish (LList _) -> check0
+ EVar _ -> check0
+ ELit _ _ -> check0
+ _ ->
+ --Xerror (show p)
+ impossible
+ 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
@@ -1218,7 +1295,7 @@
teqns <- withExtTyps iks $ tcEqns tfn eqns
T.return $ BFcn i teqns
BPat p a -> T.do
- (ep, tp) <- tInferExpr p
+ (ep, tp) <- withTCMode TCPat $ tInferExpr p -- pattern variables already bound
ea <- tCheckExpr tp a
T.return $ BPat ep ea
BSign _ _ -> T.return abind
@@ -1276,7 +1353,7 @@
-----------------------------------------------------
type Sigma = EType
-type Tau = EType
+--type Tau = EType
type Rho = EType
type TyVar = Ident
@@ -1318,10 +1395,10 @@
getMetaTyVars tys = T.do
tys' <- T.mapM zonkType tys
T.return (metaTvs tys')
+-}
getEnvTypes :: Tc [EType]
getEnvTypes = gets (map entryType . concat . M.elems . valueTable)
--}
zonkType :: EType -> Tc EType
zonkType (EForall ns ty) = T.do
@@ -1469,18 +1546,24 @@
res_tvs <- getMetaTyVars [exp_ty]
let forall_tvs = deleteFirstsBy eqInt res_tvs env_tvs
(e',) <$> quantify forall_tvs exp_ty
+-}
checkSigma :: Expr -> Sigma -> Tc Expr
checkSigma expr sigma = T.do
(skol_tvs, rho) <- skolemise sigma
- expr' <- checkRho expr rho
- env_tys <- getEnvTypes
- esc_tvs <- getFreeTyVars (sigma : env_tys)
- let bad_tvs = filter (\ i -> elemBy eqIdent i esc_tvs) skol_tvs
- check (null bad_tvs) $
- "Type not polymorphic enough"
- T.return expr'
+ expr' <- tCheckExpr rho expr
+ if null skol_tvs then
+ -- Fast special case
+ T.return expr'
+ else T.do
+ env_tys <- getEnvTypes
+ esc_tvs <- getFreeTyVars (sigma : env_tys)
+ let bad_tvs = filter (\ i -> elemBy eqIdent i esc_tvs) skol_tvs
+ T.when (not (null bad_tvs)) $
+ tcError (getSLocExpr expr) "Type not polymorphic enough"
+ T.return expr'
+{-checkRho :: Expr -> Rho -> Tc Expr
checkRho expr ty =
tcRho expr (Check ty)
@@ -1735,6 +1818,7 @@
T.return ts
-}
+{-unifyFun :: SLoc -> Rho -> Tc (Sigma, Rho)
-- (arg,res) <- unifyFunTy fun
-- unifies 'fun' with '(arg -> res)'
@@ -1746,6 +1830,7 @@
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
@@ -1761,13 +1846,13 @@
subsCheckRho :: SLoc -> Sigma -> Rho -> Tc ()
-- Invariant: the second argument is in weak-prenex form
subsCheckRho loc sigma1@(EForall _ _) rho2 = T.do -- Rule SPEC
- rho1 <- instantiate sigma1
+ rho1 <- tInst sigma1
subsCheckRho loc rho1 rho2
subsCheckRho loc rho1 rho2 | Just (a2, r2) <- getArrow rho2 = T.do -- Rule FUN
- (a1, r1) <- unifyFun loc rho1
+ (a1, r1) <- unArrow 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
+ (a2,r2) <- unArrow loc rho2
subsCheckFun loc a1 r1 a2 r2
subsCheckRho loc tau1 tau2 -- Rule MONO
= unify loc tau1 tau2 -- Revert to ordinary unification
@@ -1777,8 +1862,8 @@
subsCheck loc a2 a1
subsCheckRho loc r1 r2
-instantiate :: Sigma -> Tc Rho
-instantiate = tInst
+--instantiate :: Sigma -> Tc Rho
+--instantiate = tInst
{-instantiate :: Sigma -> Tc Rho
@@ -1798,3 +1883,11 @@
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 loc t1 (Check t2) = subsCheckRho loc t1 t2
+instSigma _ t1 (Infer r) = T.do
+ t1' <- tInst t1
+ tSetRefType r t1'
--- a/src/MicroHs/paper/TcTerm.hs
+++ b/src/MicroHs/paper/TcTerm.hs
@@ -103,8 +103,8 @@
check_arg (p,ty) = checkPat p ty
instPatSigma :: Sigma -> Expected Sigma -> Tc ()
-instPatSigma pat_ty (Infer ref) = writeTcRef ref pat_ty
instPatSigma pat_ty (Check exp_ty) = subsCheck exp_ty pat_ty
+instPatSigma pat_ty (Infer ref) = writeTcRef ref pat_ty
checkPat :: Pat -> Sigma -> Tc [(Name, Sigma)]
checkPat p exp_ty = tcPat p (Check exp_ty)
--
⑨