shithub: MicroHs

Download patch

ref: 5c6de5290c87f5e78b5bf0433015660236326f26
parent: d424eefdba84b1a31e7c608859afb0b8b484bb63
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Wed Sep 20 09:23:03 EDT 2023

Make 'forall' part of Expr.

This is slightly slower and bigger, but paves the way for rank-N.

--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
 v3.4
-851
-(($A :0 ((_646 _595) (($B ((($S' ($C ((($C' ($S' _646)) (($B ($C _2)) _578)) (($B ($B (_646 _675))) ((($C' ($C' $C)) ((($C' ($S' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) ((($C' ($C' ($C' $B))) (($B ($B ($B ($C' $S)))) ((($C' ($C' ($C' ($C' $C)))) ((($C' ($C' ($C' ($C' ($C' $S'))))) (($B ($B ($B ($B ($B $C))))) ((($C' ($C' ($C' ($C' ($C' $C))))) ((($C' ($C' ($C' $B))) (($B ($B ($B ($C' ($C' $S'))))) ((($C' ($C' ($C' ($C' ($C' $C'))))) ((($C' ($C' ($C' ($S' ($C' $C'))))) (($B ($B ($B ($B $B')))) ((($S' $B) ($B' ($B' (($B ($S' $B)) (($B ($B _647)) ((($C' $B) (($B _744) (($B _665) ((($C' _780) _9) 0)))) (($B (_744 _668)) (($B (_681 "top level defns: ")) _626)))))))) ((($S' $B) ($B' (($B ($C' $B)) (($B $B') (($B ($B _647)) ((($C' $B) (($B _744) (($B _665) ((($C' _780) _9) 1)))) (_664 ($T (($B ($B (_744 _668))) ((($C' $B) (($B _681) ((($C' _681) _584) " = "))) (($C _403) $K))))))))))) ((($C' $B) ((($S' $C') (($B $C') (($B $C') _10))) ((($S' $B) (($B ($C' ($C' _647))) ((($C' $B) ($B' (($B _744) (($B _670) _12)))) (($B _681) ((($C' _681) (($B (_681 _1)) _626)) (($O 10) $K)))))) (($B ($B (_646 _675))) ((($C' $B) ($B' (($B _744) (($B _665) ((($C' _780) _9) 0))))) (($B ($B (_744 _668))) ((($C' ($C' _681)) (($B ($B (_681 "final pass            "))) (($B ($B (_640 6))) (($B ($B _626)) _774)))) "ms"))))))) _3))))) ((($C' ($C' $C)) (($B (($C' $C) (($B ($C _686)) _403))) (($C _699) (_715 0)))) $K))) (($B ($C $B)) (($B ($B ($C $B))) (($B ($B $BK)) (($B ($B (($C' $B) (($B _745) (($B _681) ((($C' _681) (($B (_681 "(($A :")) _626)) (($O 32) $K))))))) ((($C' $B) (($B ($C' _745)) ($B _403))) (($B (_745 (_681 ") "))) (($C _745) (_681 (($O 41) $K)))))))))))) $T)) (($B $Y) ((($C' ($C' $S)) ((($C' ($C' $S)) ((($C' $B) $P) ((($S' ($C' $B)) ($B _378)) $I))) ($BK $K))) $K))))) (($B (($S' _744) (($B _741) (($B (_744 _789)) (($B (_681 "main: findIdent: ")) _584))))) (($C' _614) _581)))) _621))) (($B ($B _618)) ((($C' $B) (($B _683) (($B $T) (($B ($C $B)) (($B ($B $BK)) ((($C' ($C' ($C' $O))) ($B (($C' $P) _581))) $K)))))) (($C _699) (_715 0))))))) ($T $A))) ($T $K))) $I)) (($B (_744 _377)) (($B (_744 _578)) (($B (_681 (($O 95) $K))) _626)))))))) (($S (($S ((($S' _8) (($B _698) (_685 (_638 "-v")))) ((_714 _638) "-r"))) (($B (_679 (($O 46) $K))) (($B _743) (_684 ((_703 _765) "-i")))))) (($B (_744 _710)) ((($C' _681) (($B _743) (_684 ((_703 _765) "-o")))) (($O "out.comb") $K))))) (($B (($S (($C ((($C' _776) _698) 1)) (_789 "Usage: mhs [-v] [-r] [-iPATH] [-oFILE] ModuleName"))) _710)) (_685 ((_745 _785) ((_745 (_638 (($O 45) $K))) (_696 1))))))) (_706 ((_745 _785) (_638 "--")))))) (($A :1 "v3.4\10&") (($A :2 ((($S' ($S' _646)) _17) (($B ($B ($B (_646 _675)))) ((($C' ($C' $B)) (($B ($B ($C' (($S' _646) (($B _648) (_737 _223)))))) (($B ($B ($B ($B $T)))) (($B ($B ($B ($B (_646 _675))))) ((($C' $B) (($B ($C' $B)) (($B ($B ($C' _647))) ((($C' $B) ($B' (($B _744) (($B _665) ((($C' _780) _9) 0))))) (($B ($B (_744 _668))) ((($C' ($C' _681)) (($B ($B (_681 "combinator conversion "))) (($B ($B (_640 6))) (($B ($B _626)) _774)))) "ms")))))) (($B ($B _648)) (($B $P) (($C _587) (_578 "main"))))))))) (_683 ($T ((($C' ($C' $O)) ((($C' $B) $P) _406)) $K))))))) (($A :3 (($B (_646 _595)) (($B (($C' _596) ((($C' _769) (($B _698) (_706 ((_745 _785) (_638 "--"))))) 1))) (($B (_744 _7)) _4)))) (($A :4 ($T (($C ((($C' $C') (($B $S) ($C $C))) (($B ($B $Y)) (($B ($B ($B _568))) (($C' ($C' _683)) (($B ($B $T)) ((($C' ($C' ($C' ($C' $O)))) (($B ($B (($C' $B) $P))) ($B _5))) $K))))))) (($B (($S' _744) (($B _741) (($B (_744 _789)) (($B (_681 "not found ")) _584))))) ($C _569))))) (($A :5 ((($C' $C) ((($S' $C) ((($C' ($C' $S')) (($S $P) ((($S' ($C' $B)) (($B ($B _7)) _5)) _5))) ($BK $K))) ((($C' ($S' $C)) ((($C' ($C' $C)) (($B (($C' $C) (($B ($P _7)) $K))) ((($C' $B) _5) _405))) ((($S' _744) (($B _741) (($B (_744 _789)) (_681 "primlookup: ")))) (($C (_720 _638)) _6)))) $K))) (_789 "trans: impossible"))) (($A :6 (($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)
\ No newline at end of file
+850
+(($A :0 ((_645 _594) (($B ((($S' ($C ((($C' ($S' _645)) (($B ($C _2)) _577)) (($B ($B (_645 _674))) ((($C' ($C' $C)) ((($C' ($S' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) ((($C' ($C' ($C' $B))) (($B ($B ($B ($C' $S)))) ((($C' ($C' ($C' ($C' $C)))) ((($C' ($C' ($C' ($C' ($C' $S'))))) (($B ($B ($B ($B ($B $C))))) ((($C' ($C' ($C' ($C' ($C' $C))))) ((($C' ($C' ($C' $B))) (($B ($B ($B ($C' ($C' $S'))))) ((($C' ($C' ($C' ($C' ($C' $C'))))) ((($C' ($C' ($C' ($S' ($C' $C'))))) (($B ($B ($B ($B $B')))) ((($S' $B) ($B' ($B' (($B ($S' $B)) (($B ($B _646)) ((($C' $B) (($B _743) (($B _664) ((($C' _779) _9) 0)))) (($B (_743 _667)) (($B (_680 "top level defns: ")) _625)))))))) ((($S' $B) ($B' (($B ($C' $B)) (($B $B') (($B ($B _646)) ((($C' $B) (($B _743) (($B _664) ((($C' _779) _9) 1)))) (_663 ($T (($B ($B (_743 _667))) ((($C' $B) (($B _680) ((($C' _680) _583) " = "))) (($C _403) $K))))))))))) ((($C' $B) ((($S' $C') (($B $C') (($B $C') _10))) ((($S' $B) (($B ($C' ($C' _646))) ((($C' $B) ($B' (($B _743) (($B _669) _12)))) (($B _680) ((($C' _680) (($B (_680 _1)) _625)) (($O 10) $K)))))) (($B ($B (_645 _674))) ((($C' $B) ($B' (($B _743) (($B _664) ((($C' _779) _9) 0))))) (($B ($B (_743 _667))) ((($C' ($C' _680)) (($B ($B (_680 "final pass            "))) (($B ($B (_639 6))) (($B ($B _625)) _773)))) "ms"))))))) _3))))) ((($C' ($C' $C)) (($B (($C' $C) (($B ($C _685)) _403))) (($C _698) (_714 0)))) $K))) (($B ($C $B)) (($B ($B ($C $B))) (($B ($B $BK)) (($B ($B (($C' $B) (($B _744) (($B _680) ((($C' _680) (($B (_680 "(($A :")) _625)) (($O 32) $K))))))) ((($C' $B) (($B ($C' _744)) ($B _403))) (($B (_744 (_680 ") "))) (($C _744) (_680 (($O 41) $K)))))))))))) $T)) (($B $Y) ((($C' ($C' $S)) ((($C' ($C' $S)) ((($C' $B) $P) ((($S' ($C' $B)) ($B _378)) $I))) ($BK $K))) $K))))) (($B (($S' _743) (($B _740) (($B (_743 _788)) (($B (_680 "main: findIdent: ")) _583))))) (($C' _613) _580)))) _620))) (($B ($B _617)) ((($C' $B) (($B _682) (($B $T) (($B ($C $B)) (($B ($B $BK)) ((($C' ($C' ($C' $O))) ($B (($C' $P) _580))) $K)))))) (($C _698) (_714 0))))))) ($T $A))) ($T $K))) $I)) (($B (_743 _377)) (($B (_743 _577)) (($B (_680 (($O 95) $K))) _625)))))))) (($S (($S ((($S' _8) (($B _697) (_684 (_637 "-v")))) ((_713 _637) "-r"))) (($B (_678 (($O 46) $K))) (($B _742) (_683 ((_702 _764) "-i")))))) (($B (_743 _709)) ((($C' _680) (($B _742) (_683 ((_702 _764) "-o")))) (($O "out.comb") $K))))) (($B (($S (($C ((($C' _775) _697) 1)) (_788 "Usage: mhs [-v] [-r] [-iPATH] [-oFILE] ModuleName"))) _709)) (_684 ((_744 _784) ((_744 (_637 (($O 45) $K))) (_695 1))))))) (_705 ((_744 _784) (_637 "--")))))) (($A :1 "v3.4\10&") (($A :2 ((($S' ($S' _645)) _17) (($B ($B ($B (_645 _674)))) ((($C' ($C' $B)) (($B ($B ($C' (($S' _645) (($B _647) (_736 _223)))))) (($B ($B ($B ($B $T)))) (($B ($B ($B ($B (_645 _674))))) ((($C' $B) (($B ($C' $B)) (($B ($B ($C' _646))) ((($C' $B) ($B' (($B _743) (($B _664) ((($C' _779) _9) 0))))) (($B ($B (_743 _667))) ((($C' ($C' _680)) (($B ($B (_680 "combinator conversion "))) (($B ($B (_639 6))) (($B ($B _625)) _773)))) "ms")))))) (($B ($B _647)) (($B $P) (($C _586) (_577 "main"))))))))) (_682 ($T ((($C' ($C' $O)) ((($C' $B) $P) _406)) $K))))))) (($A :3 (($B (_645 _594)) (($B (($C' _595) ((($C' _768) (($B _697) (_705 ((_744 _784) (_637 "--"))))) 1))) (($B (_743 _7)) _4)))) (($A :4 ($T (($C ((($C' $C') (($B $S) ($C $C))) (($B ($B $Y)) (($B ($B ($B _567))) (($C' ($C' _682)) (($B ($B $T)) ((($C' ($C' ($C' ($C' $O)))) (($B ($B (($C' $B) $P))) ($B _5))) $K))))))) (($B (($S' _743) (($B _740) (($B (_743 _788)) (($B (_680 "not found ")) _583))))) ($C _568))))) (($A :5 ((($C' $C) ((($S' $C) ((($C' ($C' $S')) (($S $P) ((($S' ($C' $B)) (($B ($B _7)) _5)) _5))) ($BK $K))) ((($C' ($S' $C)) ((($C' ($C' $C)) (($B (($C' $C) (($B ($P _7)) $K))) ((($C' $B) _5) _405))) ((($S' _743) (($B _740) (($B (_743 _788)) (_680 "primlookup: ")))) (($C (_719 _637)) _6)))) $K))) (_788 "trans: impossible"))) (($A :6 (($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)
\ No newline at end of file
--- a/src/MicroHs/Expr.hs
+++ b/src/MicroHs/Expr.hs
@@ -15,6 +15,7 @@
   EAlt,
   ECaseArm,
   EType, showEType,
+  ETypeScheme,
   EPat, patVars, isPVar, isPConApp,
   EKind, kType,
   IdKind(..), idKindIdent,
@@ -21,7 +22,6 @@
   LHS,
   Constr,
   ConTyInfo,
-  ETypeScheme(..),
   Con(..), conIdent, conArity, eqCon,
   tupleConstr, untupleConstr,
   subst,
@@ -56,7 +56,7 @@
   | Newtype LHS Ident EType
   | Type LHS EType
   | Fcn Ident [Eqn]
-  | Sign Ident ETypeScheme
+  | Sign Ident EType
   | Import ImportSpec
   | ForImp String Ident EType
   | Infix Fixity [Ident]
@@ -91,6 +91,7 @@
   | EUVar Int
   -- Constructors after type checking
   | ECon Con
+  | EForall [IdKind] Expr -- only in types
   --Xderiving (Show, Eq)
 
 data Con
@@ -154,7 +155,7 @@
 data EStmt = SBind EPat Expr | SThen Expr | SLet [EBind]
   --Xderiving (Show, Eq)
 
-data EBind = BFcn Ident [Eqn] | BPat EPat Expr | BSign Ident ETypeScheme
+data EBind = BFcn Ident [Eqn] | BPat EPat Expr | BSign Ident EType
   --Xderiving (Show, Eq)
 
 -- A single equation for a function
@@ -190,8 +191,8 @@
 --  * before desugaring: EApp, EVar, ETuple, EList
 type EType = Expr
 
-data ETypeScheme = ETypeScheme [IdKind] EType
-  --Xderiving (Show, Eq)
+-- A type starting with an EForall
+type ETypeScheme = EType
 
 data IdKind = IdKind Ident EKind
   --Xderiving (Show, Eq)
@@ -282,6 +283,7 @@
     EAt i e -> i : allVarsExpr e
     EUVar _ -> []
     ECon c -> [conIdent c]
+    EForall iks e -> map (\ (IdKind i _) -> i) iks ++ allVarsExpr e
 
 allVarsListish :: Listish -> [Ident]
 allVarsListish (LList es) = concatMap allVarsExpr es
@@ -356,7 +358,7 @@
     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
+    Sign i t -> showIdent i ++ " :: " ++ showEType t
     Import (ImportSpec q m mm mis) -> "import " ++ (if q then "qualified " else "") ++ showIdent m ++ maybe "" ((" as " ++) . unIdent) mm ++
       case mis of
         Nothing -> ""
@@ -414,6 +416,7 @@
     EAt i e -> showIdent i ++ "@" ++ showExpr e
     EUVar i -> "a" ++ showInt i
     ECon c -> showCon c
+    EForall iks e -> "forall " ++ unwords (map showIdKind iks) ++ " . " ++ showEType e
   where
     showApp as (EApp f a) = showApp (as ++ [a]) f
     showApp as (EVar i) | eqString op "->", [a, b] <- as = "(" ++ showExpr a ++ " -> " ++ showExpr b ++ ")"
@@ -451,7 +454,7 @@
   case ab of
     BFcn i eqns -> showEDef (Fcn i eqns)
     BPat p e -> showEPat p ++ " = " ++ showExpr e
-    BSign i t -> showIdent i ++ " :: " ++ showETypeScheme t
+    BSign i t -> showIdent i ++ " :: " ++ showEType t
 
 showCaseArm :: ECaseArm -> String
 showCaseArm arm =
@@ -466,12 +469,3 @@
 
 showEKind :: EKind -> String
 showEKind = showEType
-
-showETypeScheme :: ETypeScheme -> String
-showETypeScheme ts =
-  case ts of
-    ETypeScheme vs t ->
-      if null vs
-      then showEType t
-      else unwords ("forall" : map showIdKind vs ++ [".", showEType t])
-
--- a/src/MicroHs/Parse.hs
+++ b/src/MicroHs/Parse.hs
@@ -283,7 +283,7 @@
 pTypeScheme = P.do
   vs <- (pKeyword "forall" *> esome pIdKind <* pSymbol ".") <|< pure []
   t <- pType
-  pure $ ETypeScheme vs t
+  pure $ if null vs then t else EForall vs t
 
 --
 -- Partial copy of pExpr, but that includes '->'.
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -120,9 +120,10 @@
 
 constrsOf :: Ident -> [(Ident, [Entry])] -> [ValueExport]
 constrsOf qi ies =
-  [ ValueExport i e | (i, es) <- ies, e@(Entry (ECon _) (ETypeScheme _ t)) <- es, eqIdent (retTyCon t) qi ]
+  [ ValueExport i e | (i, es) <- ies, e@(Entry (ECon _) t) <- es, eqIdent (retTyCon t) qi ]
 
 retTyCon :: EType -> Ident
+retTyCon (EForall _ t) = retTyCon t
 retTyCon t =
   case getArrow t of
     Nothing -> getAppCon t
@@ -148,7 +149,7 @@
     con ci it vks (ic, ts) =
       let
         e = ECon $ ConData ci (qualIdent mn ic)
-      in ValueExport ic $ Entry e (ETypeScheme vks (foldr tArrow (tApps (qualIdent mn it) (map tVarK vks)) ts))
+      in ValueExport ic $ Entry e (EForall vks (foldr tArrow (tApps (qualIdent mn it) (map tVarK vks)) ts))
     cons i vks cs =
       let
         ci = [ (qualIdent mn c, length ts) | (c, ts) <- cs ]
@@ -156,14 +157,14 @@
     conn it vks ic t =
       let
         e = ECon $ ConNew (qualIdent mn ic)
-      in [ValueExport ic $ Entry e (ETypeScheme vks (tArrow t (tApps (qualIdent mn it) (map tVarK vks))))]
-    tentry i vks kret = Entry (EVar (qualIdent mn i)) (ETypeScheme [] $ lhsKind vks kret)
+      in [ValueExport ic $ Entry e (EForall vks (tArrow t (tApps (qualIdent mn it) (map tVarK vks))))]
+    tentry i vks kret = Entry (EVar (qualIdent mn i)) (lhsKind vks kret)
     ves = [ ValueExport i (Entry (EVar (qualIdent mn i)) ts) | Sign i ts <- tds ]
     tes =
       [ TypeExport i (tentry i vks kType) (cons i vks cs)  | Data    (i, vks) cs  <- tds ] ++
       [ TypeExport i (tentry i vks kType) (conn i vks c t) | Newtype (i, vks) c t <- tds ] ++
       [ TypeExport i (tentry i vks kType) []               | Type    (i, vks) _   <- tds ]   -- XXX kType is wrong
-    ses = [ (qualIdent mn i, ETypeScheme vs t) | Type (i, vs) t  <- tds ]
+    ses = [ (qualIdent mn i, EForall vs t) | Type (i, vs) t  <- tds ]
     fes = [ (qualIdent mn i, fx) | Infix fx is <- tds, i <- is ]
   in  TModule mn fes tes ses ves a
 
@@ -277,13 +278,13 @@
   in TC mn 1 fs xts ss xvs IM.empty
 
 kTypeS :: ETypeScheme
-kTypeS = ETypeScheme [] kType
+kTypeS = kType
 
 kTypeTypeS :: ETypeScheme
-kTypeTypeS = ETypeScheme [] $ kArrow kType kType
+kTypeTypeS = kArrow kType kType
 
 kTypeTypeTypeS :: ETypeScheme
-kTypeTypeTypeS = ETypeScheme [] $ kArrow kType $ kArrow kType kType
+kTypeTypeTypeS = kArrow kType $ kArrow kType kType
 
 primKindTable :: KindTable
 primKindTable =
@@ -304,7 +305,7 @@
     tuple n =
       let
         i = tupleConstr n
-      in  (i, [entry (unIdent i) $ ETypeScheme [] $ foldr kArrow kType (replicate n kType)])
+      in  (i, [entry (unIdent i) $ foldr kArrow kType (replicate n kType)])
   in  
       [
        -- The function arrow is bothersome to define in Primtives, so keep it here.
@@ -323,7 +324,7 @@
         vks = [IdKind (mkIdent ("a" ++ showInt i)) kType | i <- enumFromTo 1 n]
         ts = map tVarK vks
         r = tApps c ts
-      in  (c, [Entry (ECon $ ConData [(c, n)] c) $ ETypeScheme vks $ foldr tArrow r ts ])
+      in  (c, [Entry (ECon $ ConData [(c, n)] c) $ EForall vks $ foldr tArrow r ts ])
   in  map tuple (enumFromTo 2 10)
 
 type T a = TC TCState a
@@ -385,11 +386,13 @@
           syns <- gets synTable
           case M.lookup i syns of
             Nothing -> T.return $ foldl tApp t ts
-            Just (ETypeScheme vks tt) ->
+            Just (EForall vks tt) ->
               if length vks /= length ts then tcError (getSLocIdent i) $ ": bad synonym use: " --X ++ show (i, vks, ts)
               else expandSyn $ subst (zip (map idKindIdent vks) ts) tt
+            Just _ -> impossible
         EUVar _ -> T.return $ foldl tApp t ts
         ESign a _ -> expandSyn a   -- Throw away signatures, they don't affect unification
+        EForall iks tt | null ts -> EForall iks <$> expandSyn tt
         _ -> impossible
   in syn [] at
 
@@ -407,6 +410,7 @@
         Just t -> derefUVar t
     EVar _ -> T.return at
     ESign t k -> flip ESign k <$> derefUVar t
+    EForall iks t -> EForall iks <$> derefUVar t
     _ -> impossible
 
 unify :: --XHasCallStack =>
@@ -479,12 +483,13 @@
 tInst :: ETypeScheme -> T EType
 tInst as =
   case as of
-    ETypeScheme vks t ->
+    EForall vks t ->
       if null vks then T.return t
       else T.do
         let vs = map idKindIdent vks
         us <- T.mapM (const newUVar) (replicate (length vs) ())
         T.return (subst (zip vs us) t)
+    t -> T.return t
 
 extValE :: --XHasCallStack =>
            Ident -> ETypeScheme -> Expr -> T ()
@@ -545,7 +550,7 @@
 
 withExtTyps :: forall a . [IdKind] -> T a -> T a
 withExtTyps iks ta = T.do
-  let env = map (\ (IdKind v k) -> (v, ETypeScheme [] k)) iks
+  let env = map (\ (IdKind v k) -> (v, k)) iks
   venv <- gets typeTable
   extTyps env
   a <- ta
@@ -594,7 +599,7 @@
           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
+          withExtVal i kk $ loop (IdKind i kk : r) iks
       loop [] vks
   fun nvks nkr
 
@@ -614,7 +619,7 @@
 addLHSKind :: LHS -> EKind -> T ()
 addLHSKind (i, vks) kret =
 --  trace ("addLHSKind " ++ showIdent i ++ " :: " ++ showExpr (lhsKind vks kret)) $
-  extQVal i (ETypeScheme [] $ lhsKind vks kret)
+  extQVal i (lhsKind vks kret)
 
 lhsKind :: [IdKind] -> EKind -> EKind
 lhsKind vks kret = foldr (\ (IdKind _ k) -> kArrow k) kret vks
@@ -624,9 +629,9 @@
 addTypeSyn adef =
   case adef of
     Type (i, vs) t -> T.do
-      extSyn i (ETypeScheme vs t)
+      extSyn i (EForall vs t)
       mn <- gets moduleName
-      extSyn (qualIdent mn i) (ETypeScheme vs t)
+      extSyn (qualIdent mn i) (EForall vs t)
     _ -> T.return ()
 
 tcDefType :: EDef -> T EDef
@@ -636,22 +641,16 @@
     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 Nothing t)
-    Sign    i      t -> Sign    i     <$> tcTypeScheme (Just kType) t
+    Sign    i      t -> (Sign    i   . fst) <$> tcTypeT (Just kType) t
     ForImp  ie i   t -> (ForImp ie i . fst) <$> tcTypeT (Just kType) t
     _ -> T.return d
 
-tcTypeScheme :: --XHasCallStack =>
-                Maybe EKind -> ETypeScheme -> T ETypeScheme
-tcTypeScheme mk (ETypeScheme vks t) =
-  withVks vks kType $ \ vvks _ ->
-    ETypeScheme vvks <$> withVars vvks (fst <$> tcTypeT mk t)
-
 withVars :: forall a . [IdKind] -> T a -> T a
 withVars aiks ta =
   case aiks of
     [] -> ta
     IdKind i k : iks -> T.do
-      withExtVal i (ETypeScheme [] k) $ withVars iks ta
+      withExtVal i k $ withVars iks ta
 
 tcConstr :: Constr -> T Constr
 tcConstr (i, ts) = (i,) <$> T.mapM (\ t -> fst <$> tcTypeT (Just kType) t) ts
@@ -673,18 +672,21 @@
         cti = [ (qualIdent mn c, length ts) | (c, ts) <- cs ]
         tret = foldl tApp (tCon (qualIdent mn i)) (map tVarK vks)
         addCon (c, ts) =
-          extValE c (ETypeScheme vks $ foldr tArrow tret ts) (ECon $ ConData cti (qualIdent mn c))
+          extValE c (EForall vks $ foldr tArrow tret ts) (ECon $ ConData cti (qualIdent mn c))
       T.mapM_ addCon cs
     Newtype (i, vks) c t -> T.do
       let
         tret = foldl tApp (tCon (qualIdent mn i)) (map tVarK vks)
-      extValE c (ETypeScheme vks $ tArrow t tret) (ECon $ ConNew (qualIdent mn c))
+      extValE c (EForall vks $ tArrow t tret) (ECon $ ConNew (qualIdent mn c))
     ForImp _ i t -> T.do
-      let t' = ETypeScheme [] t
-      extQVal i t'
-      extVal (qualIdent mn i) t'
+      extQVal i t
+      extVal (qualIdent mn i) t
     _ -> T.return ()
 
+unForall :: EType -> ([IdKind], EType)
+unForall (EForall iks t) = (iks, t)
+unForall t = ([], t)
+
 tcDefValue :: --XHasCallStack =>
               EDef -> T EDef
 tcDefValue adef =
@@ -691,7 +693,8 @@
   case adef of
     Fcn i eqns -> T.do
 --      traceM $ "tcDefValue: " ++ showLHS (i, vs) ++ " = " ++ showExpr rhs
-      (_, ETypeScheme iks tfn) <- tLookup "no type signature" i
+      (_, tt) <- tLookup "no type signature" i
+      let (iks, tfn) = unForall tt
       mn <- gets moduleName
       teqns <- withExtTyps iks $ tcEqns tfn eqns
       T.return $ Fcn (qualIdent mn i) teqns
@@ -842,6 +845,10 @@
       (_, ti) <- tLookupInst "impossible!" i
       unify (getSLocExpr ae) t ti
       T.return (EAt i ee, t)
+    EForall vks t ->
+      withVks vks kType $ \ vvks _ -> T.do
+        (tt, k) <- withVars vvks (tcExpr mt t)
+        T.return (EForall vvks tt, k)
     _ -> impossible
 
 enum :: String -> [Expr] -> Expr
@@ -872,21 +879,20 @@
 --      traceM (showExpr (EApp (EApp f e1) e2))
       T.return (EApp (EApp f e1) e2, ftr2)
 
-    -- XXX clc should calc.  It's an ugly hack until we get mutual recursion
-    doOp clc (e1:e2:es) o os ies = T.do
+    doOp (e1:e2:es) o os ies = T.do
       e <- appOp o e2 e1
-      clc (e:es) os ies
-    doOp _ _ _ _ _ = impossible
+      calc (e:es) os ies
+    doOp _ _ _ _ = impossible
 
     calc :: [Typed Expr] -> [(Typed Expr, Fixity)] -> [((Typed Expr, Fixity), Expr)] -> T (Typed Expr) 
     calc [et@(_, t)] [] [] = T.do munify (getSLocExpr ae) mt t; T.return et
-    calc es ((o, _):os) [] = doOp calc es o os []
+    calc es ((o, _):os) [] = doOp es o os []
     calc es oos@((oy, (ay, py)):os) iies@((oo@(ox, (ax, px)), e) : ies) = T.do
 --      traceM (show ((unIdent (getIdent (fst o)), ay, py), (unIdent i, ax, px)))
       if px == py && (not (eqAssoc ax ay) || eqAssoc ax AssocNone) then
         tcError (getSLocExpr (fst ox)) "Ambiguous operator expression"
        else if px < py || eqAssoc ax AssocLeft && px == py then
-        doOp calc es oy os iies
+        doOp es oy os iies
        else T.do
         et <- tcExpr Nothing e
         calc (et:es) (oo : oos) ies
@@ -975,7 +981,7 @@
 tcPat ::forall a .  EType -> EPat -> (EPat -> T a) -> T a
 tcPat t ap ta = T.do
 --  traceM $ "tcPat: " ++ show ap
-  env <- T.mapM (\ v -> ((v,) . ETypeScheme []) <$> newUVar) $ filter (not . isUnderscore) $ patVars ap
+  env <- T.mapM (\ v -> (v,) <$> newUVar) $ filter (not . isUnderscore) $ patVars ap
   withExtVals env $ T.do
     (pp, _) <- tcExpr (Just t) ap
     () <- checkArity (getSLocExpr ap) 0 pp
@@ -1002,9 +1008,9 @@
   case M.lookup x tmap of
     Nothing -> T.do
       t <- newUVar
-      T.return (x, ETypeScheme [] t)
+      T.return (x, t)
     Just t -> T.do
-      tt <- withTypeTable $ tcTypeScheme (Just kType) t
+      tt <- fst <$> (withTypeTable $ tcTypeT (Just kType) t)
       T.return (x, tt)
 
 tcBind :: EBind -> T EBind
@@ -1011,7 +1017,8 @@
 tcBind abind =
   case abind of
     BFcn i eqns -> T.do
-      (_, ETypeScheme iks tfn) <- tLookup "impossible!" i
+      (_, tt) <- tLookup "impossible!" i
+      let (iks, tfn) = unForall tt
       teqns <- withExtTyps iks $ tcEqns tfn eqns
       T.return $ BFcn i teqns
     BPat p a -> T.do
@@ -1037,6 +1044,7 @@
     EListish (LList [t]) -> tApp tList (dsType t)
     ETuple ts -> tApps (tupleConstr (length ts)) (map dsType ts)
     ESign t k -> ESign (dsType t) k
+    EForall iks t -> EForall iks (dsType t)
     _ -> impossible
 
 tConI :: String -> EType
--