demo/hello compiles with kind polymorphism

13 files changed, 420 insertions, 126 deletions

diff --git a/src/core.sml b/src/core.sml
index a28d93dd..b384c576 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -37,6 +37,9 @@ datatype kind' =
        | KUnit
        | KTuple of kind list
 
+       | KRel of int
+       | KFun of string * kind
+
 withtype kind = kind' located
 
 datatype con' =
@@ -50,6 +53,10 @@ datatype con' =
        | CApp of con * con
        | CAbs of string * kind * con
 
+       | CKAbs of string * con
+       | CKApp of con * kind
+       | TKFun of string * con
+
        | CName of string
 
        | CRecord of kind * (con * con) list
@@ -91,6 +98,9 @@ datatype exp' =
        | ECApp of exp * con
        | ECAbs of string * kind * exp
 
+       | EKAbs of string * exp
+       | EKApp of exp * kind
+
        | ERecord of (con * exp * con) list
        | EField of exp * con * { field : con, rest : con }
        | EConcat of exp * con * exp * con
diff --git a/src/core_env.sig b/src/core_env.sig
index 98e345cc..6b954c12 100644
--- a/src/core_env.sig
+++ b/src/core_env.sig
@@ -43,6 +43,9 @@ signature CORE_ENV = sig
     exception UnboundRel of int
     exception UnboundNamed of int
 
+    val pushKRel : env -> string -> env
+    val lookupKRel : env -> int -> string
+
     val pushCRel : env -> string -> Core.kind -> env
     val lookupCRel : env -> int -> string * Core.kind
 
diff --git a/src/core_env.sml b/src/core_env.sml
index 07162606..2c100aa5 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -36,8 +36,46 @@ structure IM = IntBinaryMap
 
 (* AST utility functions *)
 
+val liftKindInKind =
+    U.Kind.mapB {kind = fn bound => fn k =>
+                                       case k of
+                                           KRel xn =>
+                                           if xn < bound then
+                                               k
+                                           else
+                                               KRel (xn + 1)
+                                         | _ => k,
+                 bind = fn (bound, _) => bound + 1}
+
+val liftKindInCon =
+    U.Con.mapB {kind = fn bound => fn k =>
+                                      case k of
+                                          KRel xn =>
+                                          if xn < bound then
+                                              k
+                                          else
+                                              KRel (xn + 1)
+                                        | _ => k,
+                con = fn _ => fn c => c,
+                bind = fn (bound, U.Con.RelK _) => bound + 1
+                        | (bound, _) => bound}
+
+val liftKindInExp =
+    U.Exp.mapB {kind = fn bound => fn k =>
+                                      case k of
+                                          KRel xn =>
+                                          if xn < bound then
+                                              k
+                                          else
+                                              KRel (xn + 1)
+                                        | _ => k,
+                con = fn _ => fn c => c,
+                exp = fn _ => fn e => e,
+                bind = fn (bound, U.Exp.RelK _) => bound + 1
+                        | (bound, _) => bound}
+    
 val liftConInCon =
-    U.Con.mapB {kind = fn k => k,
+    U.Con.mapB {kind = fn _ => fn k => k,
                 con = fn bound => fn c =>
                                      case c of
                                          CRel xn =>
@@ -46,13 +84,13 @@ val liftConInCon =
                                          else
                                              CRel (xn + 1)
                                        | _ => c,
-                bind = fn (bound, U.Con.Rel _) => bound + 1
+                bind = fn (bound, U.Con.RelC _) => bound + 1
                         | (bound, _) => bound}
 
 val lift = liftConInCon 0
 
 val subConInCon =
-    U.Con.mapB {kind = fn k => k,
+    U.Con.mapB {kind = fn _ => fn k => k,
                 con = fn (xn, rep) => fn c =>
                                   case c of
                                       CRel xn' =>
@@ -61,12 +99,12 @@ val subConInCon =
                                          | GREATER => CRel (xn' - 1)
                                          | LESS => c)
                                     | _ => c,
-                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+                bind = fn ((xn, rep), U.Con.RelC _) => (xn+1, liftConInCon 0 rep)
                         | (ctx, _) => ctx}
 
 
 val liftConInExp =
-    U.Exp.mapB {kind = fn k => k,
+    U.Exp.mapB {kind = fn _ => fn k => k,
                 con = fn bound => fn c =>
                                      case c of
                                          CRel xn =>
@@ -80,7 +118,7 @@ val liftConInExp =
                         | (bound, _) => bound}
 
 val subConInExp =
-    U.Exp.mapB {kind = fn k => k,
+    U.Exp.mapB {kind = fn _ => fn k => k,
                 con = fn (xn, rep) => fn c =>
                                          case c of
                                              CRel xn' =>
@@ -94,7 +132,7 @@ val subConInExp =
                         | (ctx, _) => ctx}
 
 val liftExpInExp =
-    U.Exp.mapB {kind = fn k => k,
+    U.Exp.mapB {kind = fn _ => fn k => k,
                 con = fn _ => fn c => c,
                 exp = fn bound => fn e =>
                                      case e of
@@ -108,7 +146,7 @@ val liftExpInExp =
                         | (bound, _) => bound}
 
 val subExpInExp =
-    U.Exp.mapB {kind = fn k => k,
+    U.Exp.mapB {kind = fn _ => fn k => k,
                 con = fn _ => fn c => c,
                 exp = fn (xn, rep) => fn e =>
                                   case e of
@@ -128,6 +166,8 @@ exception UnboundRel of int
 exception UnboundNamed of int
 
 type env = {
+     relK : string list,
+
      relC : (string * kind) list,
      namedC : (string * kind * con option) IM.map,
 
@@ -139,6 +179,8 @@ type env = {
 }
 
 val empty = {
+    relK = [],
+
     relC = [],
     namedC = IM.empty,
 
@@ -149,8 +191,27 @@ val empty = {
     namedE = IM.empty
 }
 
+fun pushKRel (env : env) x =
+    {relK = x :: #relK env,
+
+     relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
+     namedC = #namedC env,
+
+     relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
+     namedE = #namedE env,
+
+     datatypes = #datatypes env,
+     constructors = #constructors env
+    }
+
+fun lookupKRel (env : env) n =
+    (List.nth (#relK env, n))
+    handle Subscript => raise UnboundRel n
+
 fun pushCRel (env : env) x k =
-    {relC = (x, k) :: #relC env,
+    {relK = #relK env,
+
+     relC = (x, k) :: #relC env,
      namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
 
      datatypes = #datatypes env,
@@ -164,7 +225,9 @@ fun lookupCRel (env : env) n =
     handle Subscript => raise UnboundRel n
 
 fun pushCNamed (env : env) x n k co =
-    {relC = #relC env,
+    {relK = #relK env,
+
+     relC = #relC env,
      namedC = IM.insert (#namedC env, n, (x, k, co)),
 
      datatypes = #datatypes env,
@@ -179,7 +242,9 @@ fun lookupCNamed (env : env) n =
       | SOME x => x
 
 fun pushDatatype (env : env) x n xs xncs =
-    {relC = #relC env,
+    {relK = #relK env,
+
+     relC = #relC env,
      namedC = #namedC env,
 
      datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)),
@@ -201,7 +266,9 @@ fun lookupConstructor (env : env) n =
       | SOME x => x
 
 fun pushERel (env : env) x t =
-    {relC = #relC env,
+    {relK = #relK env,
+
+     relC = #relC env,
      namedC = #namedC env,
 
      datatypes = #datatypes env,
@@ -215,7 +282,9 @@ fun lookupERel (env : env) n =
     handle Subscript => raise UnboundRel n
 
 fun pushENamed (env : env) x n t eo s =
-    {relC = #relC env,
+    {relK = #relK env,
+
+     relC = #relC env,
      namedC = #namedC env,
 
      datatypes = #datatypes env,
diff --git a/src/core_print.sig b/src/core_print.sig
index 38a51aef..64a73a46 100644
--- a/src/core_print.sig
+++ b/src/core_print.sig
@@ -28,7 +28,7 @@
 (* Pretty-printing Ur/Web internal language *)
 
 signature CORE_PRINT = sig
-    val p_kind : Core.kind Print.printer
+    val p_kind : CoreEnv.env -> Core.kind Print.printer
     val p_con : CoreEnv.env -> Core.con Print.printer
     val p_pat : CoreEnv.env -> Core.pat Print.printer
     val p_exp : CoreEnv.env -> Core.exp Print.printer
diff --git a/src/core_print.sml b/src/core_print.sml
index 504773ab..cc6e5428 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -38,22 +38,33 @@ structure E = CoreEnv
 
 val debug = ref false
 
-fun p_kind' par (k, _) =
+fun p_kind' par env (k, _) =
     case k of
         KType => string "Type"
-      | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
+      | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1,
                                              space,
                                              string "->",
                                              space,
-                                             p_kind k2])
+                                             p_kind env k2])
       | KName => string "Name"
-      | KRecord k => box [string "{", p_kind k, string "}"]
+      | KRecord k => box [string "{", p_kind env k, string "}"]
       | KUnit => string "Unit"
       | KTuple ks => box [string "(",
-                          p_list_sep (box [space, string "*", space]) p_kind ks,
+                          p_list_sep (box [space, string "*", space]) (p_kind env) ks,
                           string ")"]
 
-and p_kind k = p_kind' false k
+      | KRel n => ((if !debug then
+                         string (E.lookupKRel env n ^ "_" ^ Int.toString n)
+                     else
+                         string (E.lookupKRel env n))
+                    handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
+      | KFun (x, k) => box [string x,
+                            space,
+                            string "-->",
+                            space,
+                            p_kind (E.pushKRel env x) k]
+
+and p_kind env = p_kind' false env
 
 fun p_con' par env (c, _) =
     case c of
@@ -66,7 +77,7 @@ fun p_con' par env (c, _) =
                                              space,
                                              string "::",
                                              space,
-                                             p_kind k,
+                                             p_kind env k,
                                              space,
                                              string "->",
                                              space,
@@ -105,7 +116,7 @@ fun p_con' par env (c, _) =
                                             space,
                                             string "::",
                                             space,
-                                            p_kind k,
+                                            p_kind env k,
                                             space,
                                             string "=>",
                                             space,
@@ -123,7 +134,7 @@ fun p_con' par env (c, _) =
                                               space,
                                               p_con env c]) xcs,
                               string "]::",
-                              p_kind k])
+                              p_kind env k])
         else
             parenIf par (box [string "[",
                               p_list (fn (x, c) =>
@@ -147,6 +158,21 @@ fun p_con' par env (c, _) =
       | CProj (c, n) => box [p_con env c,
                              string ".",
                              string (Int.toString n)]
+
+      | CKAbs (x, c) => box [string x,
+                             space,
+                             string "==>",
+                             space,
+                             p_con (E.pushKRel env x) c]
+      | CKApp (c, k) => box [p_con env c,
+                             string "[[",
+                             p_kind env k,
+                             string "]]"]
+      | TKFun (x, c) => box [string x,
+                             space,
+                             string "-->",
+                             space,
+                             p_con (E.pushKRel env x) c]
         
 and p_con env = p_con' false env
 
@@ -252,7 +278,7 @@ fun p_exp' par env (e, _) =
                                              space,
                                              string "::",
                                              space,
-                                             p_kind k,
+                                             p_kind env k,
                                              space,
                                              string "=>",
                                              space,
@@ -402,6 +428,16 @@ fun p_exp' par env (e, _) =
                                           p_exp env e,
                                           string "]"]
 
+      | EKAbs (x, e) => box [string x,
+                             space,
+                             string "==>",
+                             space,
+                             p_exp (E.pushKRel env x) e]
+      | EKApp (e, k) => box [p_exp env e,
+                             string "[[",
+                             p_kind env k,
+                             string "]]"]
+
 and p_exp env = p_exp' false env
 
 fun p_named x n =
@@ -480,7 +516,7 @@ fun p_decl env (dAll as (d, _) : decl) =
                  space,
                  string "::",
                  space,
-                 p_kind k,
+                 p_kind env k,
                  space,
                  string "=",
                  space,
diff --git a/src/core_util.sig b/src/core_util.sig
index fc5a2bea..fabb9878 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -30,20 +30,27 @@ signature CORE_UTIL = sig
 structure Kind : sig
     val compare : Core.kind * Core.kind -> order
 
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * string -> 'context}
+                   -> ('context, Core.kind, 'state, 'abort) Search.mapfolderB
     val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder
                   -> (Core.kind, 'state, 'abort) Search.mapfolder
     val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind
     val exists : (Core.kind' -> bool) -> Core.kind -> bool
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
+                bind : 'context * string -> 'context}
+               -> 'context -> (Core.kind -> Core.kind)
 end
 
 structure Con : sig
     val compare : Core.con * Core.con -> order
 
     datatype binder =
-             Rel of string * Core.kind
-           | Named of string * int * Core.kind * Core.con option
+             RelK of string
+           | RelC of string * Core.kind
+           | NamedC of string * int * Core.kind * Core.con option
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
                    -> ('context, Core.con, 'state, 'abort) Search.mapfolderB
@@ -55,7 +62,7 @@ structure Con : sig
                con : Core.con' -> Core.con'}
               -> Core.con -> Core.con
 
-    val mapB : {kind : Core.kind' -> Core.kind',
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
                 con : 'context -> Core.con' -> Core.con',
                 bind : 'context * binder -> 'context}
                -> 'context -> (Core.con -> Core.con)
@@ -76,12 +83,13 @@ structure Exp : sig
     val compare : Core.exp * Core.exp -> order
 
     datatype binder =
-             RelC of string * Core.kind
+             RelK of string
+           | RelC of string * Core.kind
            | NamedC of string * int * Core.kind * Core.con option
            | RelE of string * Core.con
            | NamedE of string * int * Core.con * Core.exp option * string
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
@@ -95,7 +103,7 @@ structure Exp : sig
                con : Core.con' -> Core.con',
                exp : Core.exp' -> Core.exp'}
               -> Core.exp -> Core.exp
-    val mapB : {kind : Core.kind' -> Core.kind',
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
                 con : 'context -> Core.con' -> Core.con',
                 exp : 'context -> Core.exp' -> Core.exp',
                 bind : 'context * binder -> 'context}
@@ -106,7 +114,7 @@ structure Exp : sig
                 exp : Core.exp' * 'state -> 'state}
                -> 'state -> Core.exp -> 'state
 
-    val foldB : {kind : Core.kind' * 'state -> 'state,
+    val foldB : {kind : 'context * Core.kind' * 'state -> 'state,
                  con : 'context * Core.con' * 'state -> 'state,
                  exp : 'context * Core.exp' * 'state -> 'state,
                  bind : 'context * binder -> 'context}
@@ -116,7 +124,7 @@ structure Exp : sig
                   con : Core.con' -> bool,
                   exp : Core.exp' -> bool} -> Core.exp -> bool
 
-    val existsB : {kind : Core.kind' -> bool,
+    val existsB : {kind : 'context * Core.kind' -> bool,
                    con : 'context * Core.con' -> bool,
                    exp : 'context * Core.exp' -> bool,
                    bind : 'context * binder -> 'context}
@@ -126,7 +134,7 @@ structure Exp : sig
                    con : Core.con' * 'state -> Core.con' * 'state,
                    exp : Core.exp' * 'state -> Core.exp' * 'state}
                   -> 'state -> Core.exp -> Core.exp * 'state
-    val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state,
+    val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
                     con : 'context * Core.con' * 'state -> Core.con' * 'state,
                     exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
                     bind : 'context * binder -> 'context}
@@ -136,7 +144,7 @@ end
 structure Decl : sig
     datatype binder = datatype Exp.binder
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
                     decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
@@ -159,7 +167,7 @@ structure Decl : sig
                    exp : Core.exp' * 'state -> Core.exp' * 'state,
                    decl : Core.decl' * 'state -> Core.decl' * 'state}
                   -> 'state -> Core.decl -> Core.decl * 'state
-    val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state,
+    val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
                     con : 'context * Core.con' * 'state -> Core.con' * 'state,
                     exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
                     decl : 'context * Core.decl' * 'state -> Core.decl' * 'state,
@@ -177,7 +185,7 @@ structure File : sig
 
     datatype binder = datatype Exp.binder
 
-    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
                     decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
@@ -190,7 +198,7 @@ structure File : sig
                    decl : (Core.decl', 'state, 'abort) Search.mapfolder}
                   -> (Core.file, 'state, 'abort) Search.mapfolder
 
-    val mapB : {kind : Core.kind' -> Core.kind',
+    val mapB : {kind : 'context -> Core.kind' -> Core.kind',
                 con : 'context -> Core.con' -> Core.con',
                 exp : 'context -> Core.exp' -> Core.exp',
                 decl : 'context -> Core.decl' -> Core.decl',
diff --git a/src/core_util.sml b/src/core_util.sml
index d5f8dd05..b1d07b79 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -58,45 +58,69 @@ fun compare ((k1, _), (k2, _)) =
       | (_, KUnit) => GREATER
 
       | (KTuple ks1, KTuple ks2) => joinL compare (ks1, ks2)
+      | (KTuple _, _) => LESS
+      | (_, KTuple _) => GREATER
 
-fun mapfold f =
+      | (KRel n1, KRel n2) => Int.compare (n1, n2)
+      | (KRel _, _) => LESS
+      | (_, KRel _) => GREATER
+
+      | (KFun (_, k1), KFun (_, k2)) => compare (k1, k2)
+
+fun mapfoldB {kind = f, bind} =
     let
-        fun mfk k acc =
-            S.bindP (mfk' k acc, f)
+        fun mfk ctx k acc =
+            S.bindP (mfk' ctx k acc, f ctx)
 
-        and mfk' (kAll as (k, loc)) =
+        and mfk' ctx (kAll as (k, loc)) =
             case k of
                 KType => S.return2 kAll
 
               | KArrow (k1, k2) =>
-                S.bind2 (mfk k1,
+                S.bind2 (mfk ctx k1,
                       fn k1' =>
-                         S.map2 (mfk k2,
+                         S.map2 (mfk ctx k2,
                               fn k2' =>
                                  (KArrow (k1', k2'), loc)))
 
               | KName => S.return2 kAll
 
               | KRecord k =>
-                S.map2 (mfk k,
+                S.map2 (mfk ctx k,
                         fn k' =>
                            (KRecord k', loc))
 
               | KUnit => S.return2 kAll
 
               | KTuple ks =>
-                S.map2 (ListUtil.mapfold mfk ks,
+                S.map2 (ListUtil.mapfold (mfk ctx) ks,
                         fn ks' =>
                            (KTuple ks', loc))
+
+              | KRel _ => S.return2 kAll
+              | KFun (x, k) =>
+                S.map2 (mfk (bind (ctx, x)) k,
+                        fn k' =>
+                           (KFun (x, k'), loc))
     in
         mfk
     end
 
+fun mapfold fk =
+    mapfoldB {kind = fn () => fk,
+              bind = fn ((), _) => ()} ()
+
 fun map f k =
     case mapfold (fn k => fn () => S.Continue (f k, ())) k () of
-        S.Return () => raise Fail "Core_util.Kind.map"
+        S.Return () => raise Fail "CoreUtil.Kind.map"
       | S.Continue (k, ()) => k
 
+fun mapB {kind, bind} ctx k =
+    case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
+                   bind = bind} ctx k () of
+        S.Continue (k, ()) => k
+      | S.Return _ => raise Fail "CoreUtil.Kind.mapB: Impossible"
+
 fun exists f k =
     case mapfold (fn k => fn () =>
                              if f k then
@@ -194,14 +218,29 @@ fun compare ((c1, _), (c2, _)) =
 
       | (CProj (c1, n1), CProj (c2, n2)) => join (Int.compare (n1, n2),
                                                   fn () => compare (c1, c2))
+      | (CProj _, _) => LESS
+      | (_, CProj _) => GREATER
+
+      | (CKAbs (_, c1), CKAbs (_, c2)) => compare (c1, c2)
+      | (CKAbs _, _) => LESS
+      | (_, CKAbs _) => GREATER
+
+      | (CKApp (c1, k1), CKApp (c2, k2)) =>
+        join (compare (c1, c2),
+              fn () => Kind.compare (k1, k2))
+      | (CKApp _, _) => LESS
+      | (_, CKApp _) => GREATER
+
+      | (TKFun (_, c1), TKFun (_, c2)) => compare (c1, c2)
 
 datatype binder =
-         Rel of string * kind
-       | Named of string * int * kind * con option
+         RelK of string
+       | RelC of string * kind
+       | NamedC of string * int * kind * con option
 
 fun mapfoldB {kind = fk, con = fc, bind} =
     let
-        val mfk = Kind.mapfold fk
+        val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
 
         fun mfc ctx c acc =
             S.bindP (mfc' ctx c acc, fc ctx)
@@ -215,9 +254,9 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                               fn c2' =>
                                  (TFun (c1', c2'), loc)))
               | TCFun (x, k, c) =>
-                S.bind2 (mfk k,
+                S.bind2 (mfk ctx k,
                       fn k' =>
-                         S.map2 (mfc (bind (ctx, Rel (x, k))) c,
+                         S.map2 (mfc (bind (ctx, RelC (x, k))) c,
                               fn c' =>
                                  (TCFun (x, k', c'), loc)))
               | TRecord c =>
@@ -235,16 +274,16 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                               fn c2' =>
                                  (CApp (c1', c2'), loc)))
               | CAbs (x, k, c) =>
-                S.bind2 (mfk k,
+                S.bind2 (mfk ctx k,
                       fn k' =>
-                         S.map2 (mfc (bind (ctx, Rel (x, k))) c,
+                         S.map2 (mfc (bind (ctx, RelC (x, k))) c,
                               fn c' =>
                                  (CAbs (x, k', c'), loc)))
 
               | CName _ => S.return2 cAll
 
               | CRecord (k, xcs) =>
-                S.bind2 (mfk k,
+                S.bind2 (mfk ctx k,
                       fn k' =>
                          S.map2 (ListUtil.mapfold (fn (x, c) =>
                                                       S.bind2 (mfc ctx x,
@@ -262,9 +301,9 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
               | CMap (k1, k2) =>
-                S.bind2 (mfk k1,
+                S.bind2 (mfk ctx k1,
                          fn k1' =>
-                            S.map2 (mfk k2,
+                            S.map2 (mfk ctx k2,
                                     fn k2' =>
                                        (CMap (k1', k2'), loc)))
 
@@ -279,12 +318,27 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                 S.map2 (mfc ctx c,
                         fn c' =>
                            (CProj (c', n), loc))
+
+              | CKAbs (x, c) =>
+                S.map2 (mfc (bind (ctx, RelK x)) c,
+                        fn c' =>
+                           (CKAbs (x, c'), loc))
+              | CKApp (c, k) =>
+                S.bind2 (mfc ctx c,
+                      fn c' =>
+                         S.map2 (mfk ctx k,
+                                 fn k' =>
+                                    (CKApp (c', k'), loc)))
+              | TKFun (x, c) =>
+                S.map2 (mfc (bind (ctx, RelK x)) c,
+                        fn c' =>
+                           (TKFun (x, c'), loc))
     in
         mfc
     end
 
 fun mapfold {kind = fk, con = fc} =
-    mapfoldB {kind = fk,
+    mapfoldB {kind = fn () => fk,
               con = fn () => fc,
               bind = fn ((), _) => ()} ()
 
@@ -295,7 +349,7 @@ fun map {kind, con} c =
       | S.Continue (c, ()) => c
 
 fun mapB {kind, con, bind} ctx c =
-    case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+    case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
                    bind = bind} ctx c () of
         S.Continue (c, ()) => c
@@ -482,22 +536,34 @@ fun compare ((e1, _), (e2, _)) =
         join (Int.compare (n1, n2),
               fn () => join (joinL compare (es1, es2),
                              fn () => compare (e1, e2)))
+      | (EServerCall _, _) => LESS
+      | (_, EServerCall _) => GREATER
+
+      | (EKAbs (_, e1), EKAbs (_, e2)) => compare (e1, e2)
+      | (EKAbs _, _) => LESS
+      | (_, EKAbs _) => GREATER
+
+      | (EKApp (e1, k1), EKApp (e2, k2)) =>
+        join (compare (e1, e2),
+              fn () => Kind.compare (k1, k2))
 
 datatype binder =
-         RelC of string * kind
+         RelK of string
+       | RelC of string * kind
        | NamedC of string * int * kind * con option
        | RelE of string * con
        | NamedE of string * int * con * exp option * string
 
 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
     let
-        val mfk = Kind.mapfold fk
+        val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
 
         fun bind' (ctx, b) =
             let
                 val b' = case b of
-                             Con.Rel x => RelC x
-                           | Con.Named x => NamedC x
+                             Con.RelK x => RelK x
+                           | Con.RelC x => RelC x
+                           | Con.NamedC x => NamedC x
             in
                 bind (ctx, b')
             end
@@ -548,7 +614,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                               fn c' =>
                                  (ECApp (e', c'), loc)))
               | ECAbs (x, k, e) =>
-                S.bind2 (mfk k,
+                S.bind2 (mfk ctx k,
                       fn k' =>
                          S.map2 (mfe (bind (ctx, RelC (x, k))) e,
                               fn e' =>
@@ -660,6 +726,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                     S.map2 (mfc ctx t,
                                             fn t' =>
                                                (EServerCall (n, es', e', t'), loc))))
+
+              | EKAbs (x, e) =>
+                S.map2 (mfe (bind (ctx, RelK x)) e,
+                        fn e' =>
+                           (EKAbs (x, e'), loc))
+              | EKApp (e, k) =>
+                S.bind2 (mfe ctx e,
+                        fn e' =>
+                           S.map2 (mfk ctx k,
+                                   fn k' =>
+                                      (EKApp (e', k'), loc)))
                          
         and mfp ctx (pAll as (p, loc)) =
             case p of
@@ -704,13 +781,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
     end
 
 fun mapfold {kind = fk, con = fc, exp = fe} =
-    mapfoldB {kind = fk,
+    mapfoldB {kind = fn () => fk,
               con = fn () => fc,
               exp = fn () => fe,
               bind = fn ((), _) => ()} ()
 
 fun mapB {kind, con, exp, bind} ctx e =
-    case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+    case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
                    exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
                    bind = bind} ctx e () of
@@ -732,7 +809,7 @@ fun fold {kind, con, exp} s e =
       | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
 
 fun foldB {kind, con, exp, bind} ctx s e =
-    case mapfoldB {kind = fn k => fn s => S.Continue (k, kind (k, s)),
+    case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (k, kind (ctx, k, s)),
                   con = fn ctx => fn c => fn s => S.Continue (c, con (ctx, c, s)),
                   exp = fn ctx => fn e => fn s => S.Continue (e, exp (ctx, e, s)),
                   bind = bind} ctx e s of
@@ -759,11 +836,11 @@ fun exists {kind, con, exp} k =
       | S.Continue _ => false
 
 fun existsB {kind, con, exp, bind} ctx k =
-    case mapfoldB {kind = fn k => fn () =>
-                                     if kind k then
-                                         S.Return ()
-                                     else
-                                         S.Continue (k, ()),
+    case mapfoldB {kind = fn ctx => fn k => fn () =>
+                                               if kind (ctx, k) then
+                                                   S.Return ()
+                                               else
+                                                   S.Continue (k, ()),
                    con = fn ctx => fn c => fn () =>
                                               if con (ctx, c) then
                                                   S.Return ()
@@ -786,7 +863,7 @@ fun foldMap {kind, con, exp} s e =
       | S.Return _ => raise Fail "CoreUtil.Exp.foldMap: Impossible"
 
 fun foldMapB {kind, con, exp, bind} ctx s e =
-    case mapfoldB {kind = fn k => fn s => S.Continue (kind (k, s)),
+    case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
                    con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
                    exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
                    bind = bind} ctx e s of
@@ -801,13 +878,14 @@ datatype binder = datatype Exp.binder
 
 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
     let
-        val mfk = Kind.mapfold fk
+        val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
 
         fun bind' (ctx, b) =
             let
                 val b' = case b of
-                             Con.Rel x => RelC x
-                           | Con.Named x => NamedC x
+                             Con.RelK x => RelK x
+                           | Con.RelC x => RelC x
+                           | Con.NamedC x => NamedC x
             in
                 bind (ctx, b')
             end
@@ -821,7 +899,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
         and mfd' ctx (dAll as (d, loc)) =
             case d of
                 DCon (x, n, k, c) =>
-                S.bind2 (mfk k,
+                S.bind2 (mfk ctx k,
                       fn k' =>
                          S.map2 (mfc ctx c,
                               fn c' =>
@@ -877,7 +955,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
     end    
 
 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
-    mapfoldB {kind = fk,
+    mapfoldB {kind = fn () => fk,
               con = fn () => fc,
               exp = fn () => fe,
               decl = fn () => fd,
@@ -900,7 +978,7 @@ fun foldMap {kind, con, exp, decl} s d =
       | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
 
 fun foldMapB {kind, con, exp, decl, bind} ctx s d =
-    case mapfoldB {kind = fn k => fn s => S.Continue (kind (k, s)),
+    case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
                    con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
                    exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
                    decl = fn ctx => fn d => fn s => S.Continue (decl (ctx, d, s)),
@@ -1009,14 +1087,14 @@ fun mapfoldB (all as {bind, ...}) =
     end
 
 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
-    mapfoldB {kind = fk,
+    mapfoldB {kind = fn () => fk,
               con = fn () => fc,
               exp = fn () => fe,
               decl = fn () => fd,
               bind = fn ((), _) => ()} ()
 
 fun mapB {kind, con, exp, decl, bind} ctx ds =
-    case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+    case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
                    exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
                    decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
@@ -1025,7 +1103,7 @@ fun mapB {kind, con, exp, decl, bind} ctx ds =
       | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
 
 fun map {kind, con, exp, decl} ds =
-    mapB {kind = kind,
+    mapB {kind = fn () => kind,
           con = fn () => con,
           exp = fn () => exp,
           decl = fn () => decl,
diff --git a/src/corify.sml b/src/corify.sml
index 802baf66..9ca6c915 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -444,10 +444,14 @@ fun corifyKind (k, loc) =
       | L.KUnit => (L'.KUnit, loc)
       | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc)
 
+      | L.KRel n => (L'.KRel n, loc)
+      | L.KFun (x, k) => (L'.KFun (x, corifyKind k), loc)
+
 fun corifyCon st (c, loc) =
     case c of
         L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
       | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
+      | L.TKFun (x, t) => (L'.TKFun (x, corifyCon st t), loc)
       | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
 
       | L.CRel n => (L'.CRel n, loc)
@@ -468,6 +472,9 @@ fun corifyCon st (c, loc) =
       | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
       | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
 
+      | L.CKApp (c1, k) => (L'.CKApp (corifyCon st c1, corifyKind k), loc)
+      | L.CKAbs (x, c) => (L'.CKAbs (x, corifyCon st c), loc)
+
       | L.CName s => (L'.CName s, loc)
 
       | L.CRecord (k, xcs) =>
@@ -581,6 +588,8 @@ fun corifyExp st (e, loc) =
       | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
       | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
       | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
+      | L.EKApp (e1, k) => (L'.EKApp (corifyExp st e1, corifyKind k), loc)
+      | L.EKAbs (x, e1) => (L'.EKAbs (x, corifyExp st e1), loc)
 
       | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
                                               (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
diff --git a/src/defunc.sml b/src/defunc.sml
index 1e997983..7a17d1dc 100644
--- a/src/defunc.sml
+++ b/src/defunc.sml
@@ -39,7 +39,7 @@ val functionInside = U.Con.exists {kind = fn _ => false,
                                           | CFfi ("Basis", "transaction") => true
                                           | _ => false}
 
-val freeVars = U.Exp.foldB {kind = fn (_, xs) => xs,
+val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs,
                             con = fn (_, _, xs) => xs,
                             exp = fn (bound, e, xs) =>
                                      case e of
@@ -70,7 +70,7 @@ fun positionOf (v : int, ls) =
     end
 
 fun squish fvs =
-    U.Exp.mapB {kind = fn k => k,
+    U.Exp.mapB {kind = fn _ => fn k => k,
                 con = fn _ => fn c => c,
                 exp = fn bound => fn e =>
                                      case e of
@@ -211,12 +211,13 @@ fun exp (env, e, st) =
 
 fun bind (env, b) =
     case b of
-        U.Decl.RelC (x, k) => E.pushCRel env x k
+        U.Decl.RelK x => E.pushKRel env x
+      | U.Decl.RelC (x, k) => E.pushCRel env x k
       | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co
       | U.Decl.RelE (x, t) => E.pushERel env x t
       | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
 
-fun doDecl env = U.Decl.foldMapB {kind = fn x => x,
+fun doDecl env = U.Decl.foldMapB {kind = default,
                                   con = default,
                                   exp = exp,
                                   decl = default,
diff --git a/src/especialize.sml b/src/especialize.sml
index 7abc0582..6486842b 100644
--- a/src/especialize.sml
+++ b/src/especialize.sml
@@ -43,7 +43,7 @@ structure KM = BinaryMapFn(K)
 structure IM = IntBinaryMap
 structure IS = IntBinarySet
 
-val freeVars = U.Exp.foldB {kind = fn (_, xs) => xs,
+val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs,
                             con = fn (_, _, xs) => xs,
                             exp = fn (bound, e, xs) =>
                                      case e of
@@ -80,7 +80,7 @@ fun positionOf (v : int, ls) =
     end
 
 fun squish fvs =
-    U.Exp.mapB {kind = fn k => k,
+    U.Exp.mapB {kind = fn _ => fn k => k,
                 con = fn _ => fn c => c,
                 exp = fn bound => fn e =>
                                      case e of
@@ -110,7 +110,6 @@ type state = {
      decls : (string * int * con * exp * string) list
 }
 
-fun id x = x
 fun default (_, x, st) = (x, st)
 
 fun specialize' file =
@@ -281,9 +280,9 @@ fun specialize' file =
                         end
             end
 
-        and specExp env = U.Exp.foldMapB {kind = id, con = default, exp = exp, bind = bind} env
+        and specExp env = U.Exp.foldMapB {kind = default, con = default, exp = exp, bind = bind} env
 
-        val specDecl = U.Decl.foldMapB {kind = id, con = default, exp = exp, decl = default, bind = bind}
+        val specDecl = U.Decl.foldMapB {kind = default, con = default, exp = exp, decl = default, bind = bind}
 
         fun doDecl (d, (st : state, changed)) =
             let
diff --git a/src/monoize.sml b/src/monoize.sml
index 96ef2c6a..892ae81f 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -211,6 +211,10 @@ fun monoType env =
 
                   | L.CTuple _ => poly ()
                   | L.CProj _ => poly ()
+
+                  | L.CKAbs _ => poly ()
+                  | L.CKApp _ => poly ()
+                  | L.TKFun _ => poly ()
             end
     in
         mt env IM.empty
@@ -2265,6 +2269,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
             in
                 ((L'.EServerCall (call, ek, t), loc), fm)
             end
+
+          | L.EKAbs _ => poly ()
+          | L.EKApp _ => poly ()
     end
 
 fun monoDecl (env, fm) (all as (d, loc)) =
diff --git a/src/reduce.sml b/src/reduce.sml
index 77718b66..8664d38d 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -34,60 +34,104 @@ open Core
 structure IM = IntBinaryMap
 
 datatype env_item =
-         UnknownC
+         UnknownK
+       | KnownK of kind
+
+       | UnknownC
        | KnownC of con
 
        | UnknownE
        | KnownE of exp
 
-       | Lift of int * int
+       | Lift of int * int * int
 
 type env = env_item list
 
 fun ei2s ei =
     case ei of
-        UnknownC => "UC"
+        UnknownK => "UK"
+      | KnownK _ => "KK"
+      | UnknownC => "UC"
       | KnownC _ => "KC"
       | UnknownE => "UE"
       | KnownE _ => "KE"
-      | Lift (n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")"
+      | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")"
 
 fun e2s env = String.concatWith " " (map ei2s env)
 
 val deKnown = List.filter (fn KnownC _ => false
                             | KnownE _ => false
+                            | KnownK _ => false
                             | _ => true)
 
-fun conAndExp (namedC, namedE) =
+fun kindConAndExp (namedC, namedE) =
     let
+        fun kind env (all as (k, loc)) =
+            case k of
+                KType => all
+              | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc)
+              | KName => all
+              | KRecord k => (KRecord (kind env k), loc)
+              | KUnit => all
+              | KTuple ks => (KTuple (map (kind env) ks), loc)
+
+              | KRel n =>
+                let
+                    fun find (n', env, nudge, lift) =
+                        case env of
+                            [] => raise Fail "Reduce.kind: KRel"
+                          | UnknownC :: rest => find (n', rest, nudge, lift)
+                          | KnownC _ :: rest => find (n', rest, nudge, lift)
+                          | UnknownE :: rest => find (n', rest, nudge, lift)
+                          | KnownE _ :: rest => find (n', rest, nudge, lift)
+                          | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift')
+                          | UnknownK :: rest =>
+                            if n' = 0 then
+                                (KRel (n + nudge), loc)
+                            else
+                                find (n' - 1, rest, nudge, lift + 1)
+                          | KnownK k :: rest =>
+                            if n' = 0 then
+                                kind (Lift (lift, 0, 0) :: rest) k
+                            else
+                                find (n' - 1, rest, nudge - 1, lift)
+                in
+                    find (n, env, 0, 0)
+                end
+              | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc)
+
         fun con env (all as (c, loc)) =
             ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
             case c of
                 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
-              | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
+              | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc)
+              | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc)
               | TRecord c => (TRecord (con env c), loc)
 
               | CRel n =>
                 let
-                    fun find (n', env, nudge, lift) =
+                    fun find (n', env, nudge, liftK, liftC) =
                         case env of
                             [] => raise Fail "Reduce.con: CRel"
-                          | UnknownE :: rest => find (n', rest, nudge, lift)
-                          | KnownE _ :: rest => find (n', rest, nudge, lift)
-                          | Lift (lift', _) :: rest => find (n', rest, nudge + lift', lift + lift')
+                          | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC)
+                          | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC)
+                          | UnknownE :: rest => find (n', rest, nudge, liftK, liftC)
+                          | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC)
+                          | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC',
+                                                                      liftK + liftK', liftC + liftC')
                           | UnknownC :: rest =>
                             if n' = 0 then
                                 (CRel (n + nudge), loc)
                             else
-                                find (n' - 1, rest, nudge, lift + 1)
+                                find (n' - 1, rest, nudge, liftK, liftC + 1)
                           | KnownC c :: rest =>
                             if n' = 0 then
-                                con (Lift (lift, 0) :: rest) c
+                                con (Lift (liftK, liftC, 0) :: rest) c
                             else
-                                find (n' - 1, rest, nudge - 1, lift)
+                                find (n' - 1, rest, nudge - 1, liftK, liftC)
                 in
                     (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
-                    find (n, env, 0, 0)
+                    find (n, env, 0, 0, 0)
                 end
               | CNamed n =>
                 (case IM.find (namedC, n) of
@@ -105,20 +149,32 @@ fun conAndExp (namedC, namedE) =
 
                       | CApp ((CMap (dom, ran), _), f) =>
                         (case #1 c2 of
-                             CRecord (_, []) => (CRecord (ran, []), loc)
+                             CRecord (_, []) => (CRecord (kind env ran, []), loc)
                            | CRecord (_, (x, c) :: rest) =>
                              con (deKnown env)
                                  (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
-                                           (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
+                                           (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc)
                            | _ => (CApp (c1, c2), loc))                           
 
                       | _ => (CApp (c1, c2), loc)
                 end
-              | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
+              | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc)
+
+              | CKApp (c1, k) =>
+                let
+                    val c1 = con env c1
+                in
+                    case #1 c1 of
+                        CKAbs (_, b) =>
+                        con (KnownK k :: deKnown env) b
+
+                      | _ => (CKApp (c1, kind env k), loc)
+                end
+              | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc)
 
               | CName _ => all
 
-              | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
+              | CRecord (k, xcs) => (CRecord (kind env k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
               | CConcat (c1, c2) =>
                 let
                     val c1 = con env c1
@@ -126,10 +182,10 @@ fun conAndExp (namedC, namedE) =
                 in
                     case (#1 c1, #1 c2) of
                         (CRecord (k, xcs1), CRecord (_, xcs2)) =>
-                        (CRecord (k, xcs1 @ xcs2), loc)
+                        (CRecord (kind env k, xcs1 @ xcs2), loc)
                       | _ => (CConcat (c1, c2), loc)
                 end
-              | CMap _ => all
+              | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc)
 
               | CUnit => all
 
@@ -164,27 +220,30 @@ fun conAndExp (namedC, namedE) =
                 EPrim _ => all
               | ERel n =>
                 let
-                    fun find (n', env, nudge, liftC, liftE) =
+                    fun find (n', env, nudge, liftK, liftC, liftE) =
                         case env of
                             [] => raise Fail "Reduce.exp: ERel"
-                          | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE)
-                          | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE)
-                          | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE',
-                                                                   liftC + liftC', liftE + liftE')
+                          | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE)
+                          | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
+                          | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE)
+                          | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
+                          | Lift (liftK', liftC', liftE') :: rest =>
+                            find (n', rest, nudge + liftE',
+                                  liftK + liftK', liftC + liftC', liftE + liftE')
                           | UnknownE :: rest =>
                             if n' = 0 then
                                 (ERel (n + nudge), loc)
                             else
-                                find (n' - 1, rest, nudge, liftC, liftE + 1)
+                                find (n' - 1, rest, nudge, liftK, liftC, liftE + 1)
                           | KnownE e :: rest =>
                             if n' = 0 then
                                 ((*print "SUBSTITUTING\n";*)
-                                exp (Lift (liftC, liftE) :: rest) e)
+                                exp (Lift (liftK, liftC, liftE) :: rest) e)
                             else
-                                find (n' - 1, rest, nudge - 1, liftC, liftE)
+                                find (n' - 1, rest, nudge - 1, liftK, liftC, liftE)
                 in
                     (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
-                    find (n, env, 0, 0, 0)
+                    find (n, env, 0, 0, 0, 0)
                 end
               | ENamed n =>
                 (case IM.find (namedE, n) of
@@ -217,7 +276,18 @@ fun conAndExp (namedC, namedE) =
                       | _ => (ECApp (e, c), loc)
                 end
 
-              | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
+              | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc)
+
+              | EKApp (e, k) =>
+                let
+                    val e = exp env e
+                in
+                    case #1 e of
+                        EKAbs (_, b) => exp (KnownK k :: deKnown env) b
+                      | _ => (EKApp (e, kind env k), loc)
+                end
+
+              | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc)
 
               | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
               | EField (e, c, {field, rest}) =>
@@ -353,11 +423,12 @@ fun conAndExp (namedC, namedE) =
 
               | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, con env t), loc))
     in
-        {con = con, exp = exp}
+        {kind = kind, con = con, exp = exp}
     end
 
-fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c
-fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env e
+fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k
+fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c
+fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e
 
 fun reduce file =
     let
@@ -365,6 +436,7 @@ fun reduce file =
             case #1 d of
                 DCon (x, n, k, c) =>
                 let
+                    val k = kind namedC [] k
                     val c = con namedC [] c
                 in
                     ((DCon (x, n, k, c), loc),
diff --git a/src/reduce_local.sml b/src/reduce_local.sml
index 25b1023a..8b963e1b 100644
--- a/src/reduce_local.sml
+++ b/src/reduce_local.sml
@@ -85,9 +85,11 @@ fun exp env (all as (e, loc)) =
       | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
 
       | ECApp (e, c) => (ECApp (exp env e, c), loc)
-
       | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
 
+      | EKApp (e, k) => (EKApp (exp env e, k), loc)
+      | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
+
       | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc)
       | EField (e, c, others) =>
         let