ref: b5eab6d7b058d5520e07a1f996710cf573d498f2
parent: 1deadc8274c2a9b8504f056875148adc2314b412
author: Lennart Augustsson <lennart@augustsson.net>
date: Sun Sep 3 14:46:02 EDT 2023
Do kind checking.
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v3.2
-753
-(($A :0 ((_561 _514) (($B ((($S' ($C ((($C' ($S' _561)) (($B ($C _2)) _501)) (($B ($B (_561 _589))) ((($C' ($S' $C)) ((($C' ($C' $C)) ((($C' ($C' ($C' $S'))) (($B ($B ($B $C))) ((($C' ($C' ($C' ($C' $C)))) ((($C' ($C' ($C' ($C' ($S' $B))))) ((($C' ($C' ($C' ($C' ($C' $S))))) ((($C' ($C' ($C' $B))) (($B ($B ($B ($C' $C)))) ((($C' ($C' ($C' ($C' ($C' $S'))))) (($B ($B ($B ($B ($B $C))))) ((($C' ($C' ($C' ($C' ($C' ($C' $B)))))) ((($C' ($C' ($C' ($S' ($C' $B))))) (($B ($B ($B ($B $B')))) ((($C' ($C' ($C' ($C' $B)))) ((($S' $B) ($B' ($B' (($B $C') (($B ($S' _562)) ((($C' $B) (($B _650) (($B _579) ((($C' _688) _8) 0)))) (($B (_650 _582)) (($B (_595 "top level defns: ")) _543)))))))) ((($S' $B) ($B' (($B ($C' $B)) (($B $B') (($B ($B _562)) ((($C' $B) (($B _650) (($B _579) ((($C' _688) _8) 1)))) (_578 ($T (($B ($B (_650 _582))) ((($C' $B) (($B _595) _505)) (($B (_595 " = ")) _353))))))))))) ((($C' $B) ((($S' $C') (($B $C') (($B $C') _9))) ((($S' $B) (($B ($C' ($C' _562))) ((($C' $B) ($B' (($B _650) (($B _584) _11)))) (($B ($B (_595 _1))) (($B (($C' _595) _543)) (_595 (($O 10) $K))))))) (($B ($B (_561 _589))) ((($C' $B) ($B' (($B _650) (($B _579) ((($C' _688) _8) 0))))) (($B ($B (_650 _582))) (($B ($B (_595 "final pass "))) ((($C' ($C' _595)) (($B ($B (_556 6))) (($B ($B _543)) _682))) "ms")))))))) _3)))) _540))) (($B (($C' $C) (($B ($C _600)) _353))) (($C _613) (_630 0))))) (($B ($C $B)) (($B ($B ($C $B))) (($B ($B $BK)) (($B ($B ($B ($B (_595 "(($A :"))))) (($B ($B (($C' $B) (($B _595) _543)))) (($B ($B ($B (_595 (($O 32) $K))))) ((($C' $B) (($B ($C' _595)) ($B _353))) (($B (_595 ") ")) (($C _595) (($O 41) $K))))))))))))) (($B $Y) ((($C' ($C' $S)) ((($C' ($C' $S)) ((($C' $B) $P) ((($S' ($C' $B)) ($B _330)) $I))) ($BK $K))) $K))))) $T)) (($B (($S' _650) (($B _647) (($B (_650 _697)) (($B (_595 "main: findIdent: ")) _505))))) (($C' _533) _503)))) (($B ($B _537)) (($B (($C' _597) (($B $T) (($B ($C $B)) (($B ($B $BK)) ((($C' ($C' ($C' $O))) ($B (($C' $P) _503))) $K)))))) (($C _613) (_630 0)))))) (($B (_650 _329)) (($B (_650 _501)) (($B (_595 (($O 95) $K))) _543)))))) ($T $A))) ($T $K))) (($B $Y) $K)))))) (($S (($S ((($S' _7) (($B _612) (_599 (_554 "-v")))) ((_629 _554) "-r"))) (($B (_593 (($O 46) $K))) (($B _649) (_598 ((_617 _673) "-i")))))) (($B (_650 _624)) ((($C' _595) (($B _649) (_598 ((_617 _673) "-o")))) (($O "out.comb") $K))))) (($B (($S (($C ((($C' _684) _612) 1)) (_697 "Usage: uhs [-v] [-r] [-iPATH] [-oFILE] ModuleName"))) _624)) (_599 ((_651 _693) ((_651 (_554 (($O 45) $K))) (_610 1))))))) (_620 ((_651 _693) (_554 "--")))))) (($A :1 "v3.2\10&") (($A :2 ((($S' ($S' _561)) _16) (($B ($B ($B (_561 _589)))) ((($C' ($C' $B)) (($B ($B ($C' (($S' _562) (($B (_650 _580)) (($B (_650 (_611 1000000))) _192)))))) (($B ($B ($B ($B (_561 _589))))) ((($C' $B) (($B ($C' $B)) (($B ($B ($C' _562))) ((($C' $B) ($B' (($B _650) (($B _579) ((($C' _688) _8) 0))))) (($B ($B (_650 _582))) (($B ($B (_595 "combinator conversion "))) ((($C' ($C' _595)) (($B ($B (_556 6))) (($B ($B _543)) _682))) "ms"))))))) (($B ($B _563)) (($B $P) (($C _507) (_501 "main")))))))) (_597 ($T ((($C' ($C' $O)) ((($C' $B) $P) _356)) $K))))))) (($A :3 ($T (($C ((($C' $C') (($B ($S' ($B (_561 _514)))) (($B ($B ($B (($C' _515) ((($C' _677) (($B _612) (_620 ((_651 _693) (_554 "--"))))) 1))))) (($B ($B ($B (_650 _6)))) ($C $C))))) (($B ($B $Y)) (($B ($B ($B _492))) (($C' ($C' _597)) (($B ($B $T)) ((($C' ($C' ($C' ($C' $O)))) (($B ($B (($C' $B) $P))) ($B _4))) $K))))))) (($B (($S' _650) (($B _647) (($B (_650 _697)) (($B (_595 "not found ")) _505))))) ($C _493))))) (($A :4 ((($C' $C) ((($S' $C) ((($C' ($C' $S')) (($S $P) ((($S' ($C' $B)) (($B ($B _6)) _4)) _4))) ($BK $K))) ((($C' ($C' $C)) (($B (($C' $C) (($B ($P _6)) $K))) ((($C' $B) _4) _355))) (($B (_650 (_647 (_697 "primlookup")))) (($C (_633 _554)) _5))))) (_697 "trans: impossible"))) (($A :5 (($O (($P (($O 66) $K)) $B)) (($O (($P (($O 79) $K)) $O)) (($O (($P (($O 75) $K)) $K)) (($O (($P "C'") $C')) (($O (($P (($O 67) $K)) $C)) (($O (($P (($O 65) $K)) $A)) (($O (($P "S'") $S')) (($O (($P (($O 80) $K)) $P)) (($
\ No newline at end of file
+760
+(($A :0 ((_568 _521) (($B ((($S' ($C ((($C' ($S' _568)) (($B ($C _2)) _508)) (($B ($B (_568 _596))) ((($C' ($S' $C)) ((($C' ($C' $C)) ((($C' ($C' ($C' $S'))) (($B ($B ($B $C))) ((($C' ($C' ($C' ($C' $C)))) ((($C' ($C' ($C' ($C' ($S' $B))))) ((($C' ($C' ($C' ($C' ($C' $S))))) ((($C' ($C' ($C' $B))) (($B ($B ($B ($C' $C)))) ((($C' ($C' ($C' ($C' ($C' $S'))))) (($B ($B ($B ($B ($B $C))))) ((($C' ($C' ($C' ($C' ($C' ($C' $B)))))) ((($C' ($C' ($C' ($S' ($C' $B))))) (($B ($B ($B ($B $B')))) ((($C' ($C' ($C' ($C' $B)))) ((($S' $B) ($B' ($B' (($B $C') (($B ($S' _569)) ((($C' $B) (($B _657) (($B _586) ((($C' _695) _8) 0)))) (($B (_657 _589)) (($B (_602 "top level defns: ")) _550)))))))) ((($S' $B) ($B' (($B ($C' $B)) (($B $B') (($B ($B _569)) ((($C' $B) (($B _657) (($B _586) ((($C' _695) _8) 1)))) (_585 ($T (($B ($B (_657 _589))) ((($C' $B) (($B _602) _512)) (($B (_602 " = ")) _358))))))))))) ((($C' $B) ((($S' $C') (($B $C') (($B $C') _9))) ((($S' $B) (($B ($C' ($C' _569))) ((($C' $B) ($B' (($B _657) (($B _591) _11)))) (($B ($B (_602 _1))) (($B (($C' _602) _550)) (_602 (($O 10) $K))))))) (($B ($B (_568 _596))) ((($C' $B) ($B' (($B _657) (($B _586) ((($C' _695) _8) 0))))) (($B ($B (_657 _589))) (($B ($B (_602 "final pass "))) ((($C' ($C' _602)) (($B ($B (_563 6))) (($B ($B _550)) _689))) "ms")))))))) _3)))) _547))) (($B (($C' $C) (($B ($C _607)) _358))) (($C _620) (_637 0))))) (($B ($C $B)) (($B ($B ($C $B))) (($B ($B $BK)) (($B ($B ($B ($B (_602 "(($A :"))))) (($B ($B (($C' $B) (($B _602) _550)))) (($B ($B ($B (_602 (($O 32) $K))))) ((($C' $B) (($B ($C' _602)) ($B _358))) (($B (_602 ") ")) (($C _602) (($O 41) $K))))))))))))) (($B $Y) ((($C' ($C' $S)) ((($C' ($C' $S)) ((($C' $B) $P) ((($S' ($C' $B)) ($B _335)) $I))) ($BK $K))) $K))))) $T)) (($B (($S' _657) (($B _654) (($B (_657 _704)) (($B (_602 "main: findIdent: ")) _512))))) (($C' _540) _510)))) (($B ($B _544)) (($B (($C' _604) (($B $T) (($B ($C $B)) (($B ($B $BK)) ((($C' ($C' ($C' $O))) ($B (($C' $P) _510))) $K)))))) (($C _620) (_637 0)))))) (($B (_657 _334)) (($B (_657 _508)) (($B (_602 (($O 95) $K))) _550)))))) ($T $A))) ($T $K))) (($B $Y) $K)))))) (($S (($S ((($S' _7) (($B _619) (_606 (_561 "-v")))) ((_636 _561) "-r"))) (($B (_600 (($O 46) $K))) (($B _656) (_605 ((_624 _680) "-i")))))) (($B (_657 _631)) ((($C' _602) (($B _656) (_605 ((_624 _680) "-o")))) (($O "out.comb") $K))))) (($B (($S (($C ((($C' _691) _619) 1)) (_704 "Usage: uhs [-v] [-r] [-iPATH] [-oFILE] ModuleName"))) _631)) (_606 ((_658 _700) ((_658 (_561 (($O 45) $K))) (_617 1))))))) (_627 ((_658 _700) (_561 "--")))))) (($A :1 "v3.2\10&") (($A :2 ((($S' ($S' _568)) _16) (($B ($B ($B (_568 _596)))) ((($C' ($C' $B)) (($B ($B ($C' (($S' _569) (($B (_657 _587)) (($B (_657 (_618 1000000))) _191)))))) (($B ($B ($B ($B (_568 _596))))) ((($C' $B) (($B ($C' $B)) (($B ($B ($C' _569))) ((($C' $B) ($B' (($B _657) (($B _586) ((($C' _695) _8) 0))))) (($B ($B (_657 _589))) (($B ($B (_602 "combinator conversion "))) ((($C' ($C' _602)) (($B ($B (_563 6))) (($B ($B _550)) _689))) "ms"))))))) (($B ($B _570)) (($B $P) (($C _514) (_508 "main")))))))) (_604 ($T ((($C' ($C' $O)) ((($C' $B) $P) _361)) $K))))))) (($A :3 ($T (($C ((($C' $C') (($B ($S' ($B (_568 _521)))) (($B ($B ($B (($C' _522) ((($C' _684) (($B _619) (_627 ((_658 _700) (_561 "--"))))) 1))))) (($B ($B ($B (_657 _6)))) ($C $C))))) (($B ($B $Y)) (($B ($B ($B _499))) (($C' ($C' _604)) (($B ($B $T)) ((($C' ($C' ($C' ($C' $O)))) (($B ($B (($C' $B) $P))) ($B _4))) $K))))))) (($B (($S' _657) (($B _654) (($B (_657 _704)) (($B (_602 "not found ")) _512))))) ($C _500))))) (($A :4 ((($C' $C) ((($S' $C) ((($C' ($C' $S')) (($S $P) ((($S' ($C' $B)) (($B ($B _6)) _4)) _4))) ($BK $K))) ((($C' ($C' $C)) (($B (($C' $C) (($B ($P _6)) $K))) ((($C' $B) _4) _360))) (($B (_657 (_654 (_704 "primlookup")))) (($C (_640 _561)) _5))))) (_704 "trans: impossible"))) (($A :5 (($O (($P (($O 66) $K)) $B)) (($O (($P (($O 79) $K)) $O)) (($O (($P (($O 75) $K)) $K)) (($O (($P "C'") $C')) (($O (($P (($O 67) $K)) $C)) (($O (($P (($O 65) $K)) $A)) (($O (($P "S'") $S')) (($O (($P (($O 80) $K)) $P)) (($
\ No newline at end of file
--- a/src/MicroHs/Expr.hs
+++ b/src/MicroHs/Expr.hs
@@ -285,12 +285,15 @@
showEDef :: EDef -> String
showEDef def =
case def of
- Data lhs _ -> "data " ++ showLHS lhs ++ " = ..."
+ Data lhs cs -> "data " ++ showLHS lhs ++ " = " ++ intercalate " | " (map showConstr cs)
Newtype lhs c t -> "newtype " ++ showLHS lhs ++ " = " ++ showIdent c ++ " " ++ showEType t
Type lhs t -> "type " ++ showLHS lhs ++ " = " ++ showEType t
Fcn i eqns -> unlines (map (\ (Eqn ps alts) -> showIdent i ++ " " ++ unwords (map showEPat ps) ++ showAlts "=" alts) eqns)
Sign i t -> showIdent i ++ " :: " ++ showETypeScheme t
Import (ImportSpec q m mm) -> "import " ++ (if q then "qualified " else "") ++ showIdent m ++ maybe "" ((" as " ++) . unIdent) mm+
+showConstr :: Constr -> String
+showConstr (i, ts) = unwords (showIdent i : map showEType ts)
showLHS :: LHS -> String
showLHS lhs =
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -38,6 +38,7 @@
type ValueTable = M.Map [Entry]
type TypeTable = M.Map [Entry]
+type KindTable = M.Map [Entry]
type SynTable = M.Map ETypeScheme
typeCheck :: forall a . [(ImportSpec, TModule a)] -> EModule -> TModule [EDef]
@@ -217,11 +218,12 @@
TC mn n tenv _ venv m <- get
put (TC mn n tenv senv venv m)
--- Use the type table as the value table, and an empty type table
+-- 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 tt st vt m <- get
- put (TC mn n M.empty M.empty tt m)
+--BBB put (TC mn n M.empty M.empty tt m)
+ put (TC mn n primKindTable M.empty tt m)
a <- ta
TC mnr nr _ _ ttr mr <- get
put (TC mnr nr ttr st vt mr)
@@ -239,6 +241,25 @@
moduleOf :: Ident -> IdentModule
moduleOf = mkIdent . reverse . tail . dropWhile (neChar '.') . reverse . unIdent
+kTypeS :: ETypeScheme
+kTypeS = ETypeScheme [] kType
+
+kTypeTypeS :: ETypeScheme
+kTypeTypeS = ETypeScheme [] $ kArrow kType kType
+
+kTypeTypeTypeS :: ETypeScheme
+kTypeTypeTypeS = ETypeScheme [] $ kArrow kType $ kArrow kType kType
+
+primKindTable :: KindTable
+primKindTable =
+ let
+ entry i = Entry (EVar (mkIdent i))
+ in M.fromList [
+ (mkIdent "Primitives.Type", [entry "Primitives.Type" kTypeS]),
+ (mkIdent "Type", [entry "Primitives.Type" kTypeS]),
+ (mkIdent "->", [entry "Primitives.->" kTypeTypeTypeS])
+ ]
+
primTypes :: [(Ident, [Entry])]
primTypes =
let
@@ -247,21 +268,18 @@
let
i = tupleConstr n
in (i, [entry (unIdent i) $ ETypeScheme [] $ foldr kArrow kType (replicate n kType)])
- t = ETypeScheme [] kType
- tt = ETypeScheme [] $ kArrow kType kType
- ttt = ETypeScheme [] $ kArrow kType $ kArrow kType kType
in
- [(mkIdent "IO", [entry "Primitives.IO" tt]),
- (mkIdent "->", [entry "Primitives.->" ttt]),
- (mkIdent "Int", [entry "Primitives.Int" t]),
- (mkIdent "Word", [entry "Primitives.Word" t]),
- (mkIdent "Char", [entry "Primitives.Char" t]),
- (mkIdent "Handle", [entry "Primitives.Handle" t]),
- (mkIdent "Any", [entry "Primitives.Any" t]),
- (mkIdent "String", [entry "Data.Char.String" t]),
- (mkIdent "[]", [entry "Data.List.[]" tt]),
- (mkIdent "()", [entry "Data.Tuple.()" t]),
- (mkIdent "Bool", [entry "Data.Bool_Type.Bool" t])] ++
+ [(mkIdent "IO", [entry "Primitives.IO" kTypeTypeS]),
+ (mkIdent "->", [entry "Primitives.->" kTypeTypeTypeS]),
+ (mkIdent "Int", [entry "Primitives.Int" kTypeS]),
+ (mkIdent "Word", [entry "Primitives.Word" kTypeS]),
+ (mkIdent "Char", [entry "Primitives.Char" kTypeS]),
+ (mkIdent "Handle", [entry "Primitives.Handle" kTypeS]),
+ (mkIdent "Any", [entry "Primitives.Any" kTypeS]),
+ (mkIdent "String", [entry "Data.Char.String" kTypeS]),
+ (mkIdent "[]", [entry "Data.List.[]" kTypeTypeS]),
+ (mkIdent "()", [entry "Data.Tuple.()" kTypeS]),
+ (mkIdent "Bool", [entry "Data.Bool_Type.Bool" kTypeS])] ++
map tuple (enumFromTo 2 10)
primValues :: [(Ident, [Entry])]
@@ -299,9 +317,6 @@
kArrow :: EKind -> EKind -> EKind
kArrow = tArrow
-kType :: EKind
-kType = tConI "Type"
-
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
@@ -430,7 +445,8 @@
put (TC mn (n+1) tenv senv venv sub)
T.return (EUVar n)
-tLookupInst :: String -> Ident -> T (Expr, EType)
+tLookupInst :: --XHasCallStack =>
+ String -> Ident -> T (Expr, EType)
tLookupInst msg i = T.do
(e, s) <- tLookup msg i
-- traceM ("lookup " ++ show (i, s))@@ -437,7 +453,8 @@
t <- tInst s
T.return (e, t)
-tLookup :: String -> Ident -> T (Expr, ETypeScheme)
+tLookup :: --XHasCallStack =>
+ String -> Ident -> T (Expr, ETypeScheme)
tLookup msg i = T.do
env <- gets valueTable
case M.lookup i env of
@@ -537,19 +554,55 @@
tcDefsType :: [EDef] -> T [EDef]
tcDefsType ds = withTypeTable $ T.do
- T.mapM_ addTypeKind ds
- T.mapM (\ d -> T.do {tcReset; tcDefType d}) ds+ dsk <- T.mapM tcDefKind ds -- Check&rename kinds in all type definitions
+-- traceM ("tcDefs dsk=\n" ++ showEDefs dsk)+ T.mapM_ addTypeKind dsk -- Add the kind of each type to the environment
+ T.mapM tcDefType dsk
+tcDefKind :: EDef -> T EDef
+tcDefKind adef = T.do
+ tcReset
+ case adef of
+ Data (i, vks) cs -> withVks vks kType $ \ vvks _ -> T.return $ Data (i, vvks) cs
+ Newtype (i, vks) c t -> withVks vks kType $ \ vvks _ -> T.return $ Newtype (i, vvks) c t
+ Type (i, vks) at ->
+ case at of
+ ESign t k -> withVks vks k $ \ vvks kr -> T.return $ Type (i, vvks) (ESign t kr)
+ _ -> withVks vks kType $ \ vvks _ -> T.return $ Type (i, vvks) at
+ _ -> T.return adef
+
+-- Check&rename the given kinds, apply reconstruction at the end
+withVks :: forall a . [IdKind] -> EKind -> ([IdKind] -> EKind -> T a) -> T a
+withVks vks kr fun = T.do
+ (nvks, nkr) <-
+ withTypeTable $ T.do
+ let
+ loop r [] = T.do
+ (kkr, _) <- tcTypeT Nothing kr
+ T.return (reverse r, kkr)
+ loop r (IdKind i k : iks) = T.do
+ (kk, _) <- tcTypeT Nothing k
+ withExtVal i (ETypeScheme [] kk) $ loop (IdKind i kk : r) iks
+ loop [] vks
+ fun nvks nkr
+
addTypeKind :: EDef -> T ()
-addTypeKind adef =
+addTypeKind adef = T.do
+ tcReset
case adef of
Data lhs _ -> addLHSKind lhs kType
Newtype lhs _ _ -> addLHSKind lhs kType
- Type lhs _ -> addLHSKind lhs kType -- XXX
+ Type lhs t -> addLHSKind lhs (getTypeKind t)
_ -> T.return ()
+getTypeKind :: EType -> EKind
+getTypeKind (ESign _ k) = k
+getTypeKind _ = kType
+
addLHSKind :: LHS -> EKind -> T ()
-addLHSKind (i, vs) kret = extQVal i (ETypeScheme [] $ lhsKind vs kret)
+addLHSKind (i, vks) kret =
+-- trace ("addLHSKind " ++ showIdent i ++ " :: " ++ showExpr (lhsKind vks kret)) $+ extQVal i (ETypeScheme [] $ lhsKind vks kret)
lhsKind :: [IdKind] -> EKind -> EKind
lhsKind vks kret = foldr (\ (IdKind _ k) -> kArrow k) kret vks
@@ -565,29 +618,30 @@
_ -> T.return ()
tcDefType :: EDef -> T EDef
-tcDefType d =
+tcDefType d = T.do
+ tcReset
case d of
- Data lhs cs -> Data lhs <$> withVars (lhsKinds lhs) (T.mapM tcConstr cs)
- Newtype lhs c t -> Newtype lhs c <$> withVars (lhsKinds lhs) (fst <$> tcType (Just kType) t)
- Type lhs t -> Type lhs <$> withVars (lhsKinds lhs) (fst <$> tcType (Just kType) t)
+ Data lhs cs -> Data lhs <$> withVars (snd lhs) (T.mapM tcConstr cs)
+ Newtype lhs c t -> Newtype lhs c <$> withVars (snd lhs) (fst <$> tcTypeT (Just kType) t)
+ Type lhs t -> Type lhs <$> withVars (snd lhs) (fst <$> tcTypeT (Just kType) t)
Sign i t -> Sign i <$> tcTypeScheme (Just kType) t
_ -> T.return d
-tcTypeScheme :: Maybe EKind -> ETypeScheme -> T ETypeScheme
-tcTypeScheme mk (ETypeScheme vs t) =
- ETypeScheme vs <$> withVars (lhsKinds (impossible, vs)) (fst <$> tcType mk t)
+tcTypeScheme :: --XHasCallStack =>
+ Maybe EKind -> ETypeScheme -> T ETypeScheme
+tcTypeScheme mk (ETypeScheme vks t) =
+ withVks vks kType $ \ vvks _ ->
+ ETypeScheme vvks <$> withVars vvks (fst <$> tcTypeT mk t)
-lhsKinds :: LHS -> [(Ident, ETypeScheme)]
-lhsKinds (_, vks) = map (\ (IdKind i k) -> (i, ETypeScheme [] k)) vks
-
-withVars :: forall a . [(Ident, ETypeScheme)] -> T a -> T a
+withVars :: forall a . [IdKind] -> T a -> T a
withVars aiks ta =
case aiks of
[] -> ta
- (i,k) : iks -> withExtVal i k $ withVars iks ta
+ IdKind i k : iks -> T.do
+ withExtVal i (ETypeScheme [] k) $ withVars iks ta
tcConstr :: Constr -> T Constr
-tcConstr (i, ts) = pair i <$> T.mapM (\ t -> fst <$> tcType (Just kType) t) ts
+tcConstr (i, ts) = pair i <$> T.mapM (\ t -> fst <$> tcTypeT (Just kType) t) ts
tcDefsValue :: [EDef] -> T [EDef]
tcDefsValue ds = T.do
@@ -630,9 +684,23 @@
-- T.return (Fcn (qualIdent mn i, vs) (dropLam (length vs) et))
_ -> T.return adef
-tcType :: Maybe EKind -> EType -> T (Typed EType)
-tcType mk = tcExpr mk . dsType
+-- Kind check a type while already in type checking mode
+tcTypeT :: --XHasCallStack =>
+ Maybe EKind -> EType -> T (Typed EType)
+tcTypeT mk = tcExpr mk . dsType
+-- Kind check a type while in value checking mode
+tcType :: --XHasCallStack =>
+ Maybe EKind -> EType -> T (Typed EType)
+tcType mk = withTypeTable . tcTypeT mk
+
+{-+-- Sort check a kind while already in type cheking mode
+tcKind :: --XHasCallStack =>
+ EKind -> T EKind
+tcKind e = fst <$> withTypeTable (tcType (Just kType) e)
+-}
+
tcExpr :: --XHasCallStack =>
Maybe EType -> Expr -> T (Typed Expr)
tcExpr mt ae = T.do
@@ -761,7 +829,7 @@
munify (getSLocExpr ae) mt tr
T.return (ECompr ea rss, tr)
ESign e t -> T.do
- (tt, _) <- withTypeTable $ tcType (Just kType) t
+ (tt, _) <- tcType (Just kType) t
(ee, _) <- tcExpr (Just tt) e
munify (getSLocExpr ae) mt tt
T.return (ESign ee tt, tt)
--
⑨