Kind polymorphism through Explify

9 files changed, 246 insertions, 116 deletions

diff --git a/src/elab_print.sml b/src/elab_print.sml
index a0e1a54a..e5dda58e 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -68,7 +68,7 @@ fun p_kind' par env (k, _) =
                             space,
                             p_kind (E.pushKRel env x) k]
 
-and p_kind k = p_kind' false k
+and p_kind env = p_kind' false env
 
 fun p_explicitness e =
     case e of
diff --git a/src/expl.sml b/src/expl.sml
index 0101dd1f..d7138620 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -37,6 +37,9 @@ datatype kind' =
        | KTuple of kind list
        | KRecord of kind
 
+       | 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
@@ -88,6 +95,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/expl_env.sig b/src/expl_env.sig
index 00179e45..5ded0f02 100644
--- a/src/expl_env.sig
+++ b/src/expl_env.sig
@@ -42,6 +42,9 @@ signature EXPL_ENV = sig
            | Rel of int * 'a
            | Named of int * 'a
 
+    val pushKRel : env -> string -> env
+    val lookupKRel : env -> int -> string
+
     val pushCRel : env -> string -> Expl.kind -> env
     val lookupCRel : env -> int -> string * Expl.kind
 
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 0fefec2d..403a826a 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -45,8 +45,32 @@ exception UnboundNamed of int
 
 exception SynUnif
 
+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 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 =>
@@ -56,7 +80,7 @@ val liftConInCon =
                                              CRel (xn + 1)
                                        (*| CUnif _ => raise SynUnif*)
                                        | _ => c,
-                bind = fn (bound, U.Con.Rel _) => bound + 1
+                bind = fn (bound, U.Con.RelC _) => bound + 1
                         | (bound, _) => bound}
 
 val lift = liftConInCon 0
@@ -74,77 +98,82 @@ datatype 'a var =
        | Named of int * 'a
 
 type env = {
-     renameC : kind var' SM.map,
+     relK : string list,
+
      relC : (string * kind) list,
      namedC : (string * kind * con option) IM.map,
 
-     renameE : con var' SM.map,
      relE : (string * con) list,
      namedE : (string * con) IM.map,
 
-     renameSgn : (int * sgn) SM.map,
      sgn : (string * sgn) IM.map,
 
-     renameStr : (int * sgn) SM.map,
      str : (string * sgn) IM.map
 }
 
 val namedCounter = ref 0
 
 val empty = {
-    renameC = SM.empty,
+    relK = [],
+
     relC = [],
     namedC = IM.empty,
 
-    renameE = SM.empty,
     relE = [],
     namedE = IM.empty,
 
-    renameSgn = SM.empty,
     sgn = IM.empty,
 
-    renameStr = SM.empty,
     str = 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,
+
+     sgn = #sgn env,
+
+     str = #str env
+    }
+
+fun lookupKRel (env : env) n =
+    (List.nth (#relK env, n))
+    handle Subscript => raise UnboundRel n
+
 fun pushCRel (env : env) x k =
-    let
-        val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
-                               | x => x) (#renameC env)
-    in
-        {renameC = SM.insert (renameC, x, Rel' (0, k)),
-         relC = (x, k) :: #relC env,
-         namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
-
-         renameE = #renameE env,
-         relE = map (fn (x, c) => (x, lift c)) (#relE env),
-         namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
-
-         renameSgn = #renameSgn env,
-         sgn = #sgn env,
-
-         renameStr = #renameStr env,
-         str = #str env
-        }
-    end
+    {relK = #relK env,
+
+     relC = (x, k) :: #relC env,
+     namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
+
+     relE = map (fn (x, c) => (x, lift c)) (#relE env),
+     namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
+
+     sgn = #sgn env,
+
+     str = #str env
+    }
 
 fun lookupCRel (env : env) n =
     (List.nth (#relC env, n))
     handle Subscript => raise UnboundRel n
 
 fun pushCNamed (env : env) x n k co =
-    {renameC = SM.insert (#renameC env, x, Named' (n, k)),
+    {relK = #relK env,
+
      relC = #relC env,
      namedC = IM.insert (#namedC env, n, (x, k, co)),
 
-     renameE = #renameE env,
      relE = #relE env,
      namedE = #namedE env,
 
-     renameSgn = #renameSgn env,
      sgn = #sgn env,
      
-     renameStr = #renameStr env,
      str = #str env}
 
 fun lookupCNamed (env : env) n =
@@ -153,42 +182,33 @@ fun lookupCNamed (env : env) n =
       | SOME x => x
 
 fun pushERel (env : env) x t =
-    let
-        val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
-                               | x => x) (#renameE env)
-    in
-        {renameC = #renameC env,
-         relC = #relC env,
-         namedC = #namedC env,
+    {relK = #relK env,
+
+     relC = #relC env,
+     namedC = #namedC env,
 
-         renameE = SM.insert (renameE, x, Rel' (0, t)),
-         relE = (x, t) :: #relE env,
-         namedE = #namedE env,
+     relE = (x, t) :: #relE env,
+     namedE = #namedE env,
 
-         renameSgn = #renameSgn env,
-         sgn = #sgn env,
+     sgn = #sgn env,
 
-         renameStr = #renameStr env,
-         str = #str env}
-    end
+     str = #str env}
 
 fun lookupERel (env : env) n =
     (List.nth (#relE env, n))
     handle Subscript => raise UnboundRel n
 
 fun pushENamed (env : env) x n t =
-    {renameC = #renameC env,
+    {relK = #relK env,
+
      relC = #relC env,
      namedC = #namedC env,
 
-     renameE = SM.insert (#renameE env, x, Named' (n, t)),
      relE = #relE env,
      namedE = IM.insert (#namedE env, n, (x, t)),
 
-     renameSgn = #renameSgn env,
      sgn = #sgn env,
      
-     renameStr = #renameStr env,
      str = #str env}
 
 fun lookupENamed (env : env) n =
@@ -197,18 +217,16 @@ fun lookupENamed (env : env) n =
       | SOME x => x
 
 fun pushSgnNamed (env : env) x n sgis =
-    {renameC = #renameC env,
+    {relK = #relK env,
+
      relC = #relC env,
      namedC = #namedC env,
 
-     renameE = #renameE env,
      relE = #relE env,
      namedE = #namedE env,
 
-     renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
      sgn = IM.insert (#sgn env, n, (x, sgis)),
      
-     renameStr = #renameStr env,
      str = #str env}
 
 fun lookupSgnNamed (env : env) n =
@@ -217,18 +235,16 @@ fun lookupSgnNamed (env : env) n =
       | SOME x => x
 
 fun pushStrNamed (env : env) x n sgis =
-    {renameC = #renameC env,
+    {relK = #relK env,
+
      relC = #relC env,
      namedC = #namedC env,
 
-     renameE = #renameE env,
      relE = #relE env,
      namedE = #namedE env,
 
-     renameSgn = #renameSgn env,
      sgn = #sgn env,
 
-     renameStr = SM.insert (#renameStr env, x, (n, sgis)),
      str = IM.insert (#str env, n, (x, sgis))}
 
 fun lookupStrNamed (env : env) n =
diff --git a/src/expl_print.sig b/src/expl_print.sig
index 1e2c8fbb..8f1cee97 100644
--- a/src/expl_print.sig
+++ b/src/expl_print.sig
@@ -26,7 +26,7 @@
  *)
 
 signature EXPL_PRINT = sig
-    val p_kind : Expl.kind Print.printer
+    val p_kind : ExplEnv.env -> Expl.kind Print.printer
     val p_con : ExplEnv.env -> Expl.con Print.printer
     val p_exp : ExplEnv.env -> Expl.exp Print.printer
     val p_decl : ExplEnv.env -> Expl.decl Print.printer
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 313fef5c..e7fb51f6 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -38,22 +38,33 @@ structure E = ExplEnv
 
 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,
@@ -116,7 +127,7 @@ fun p_con' par env (c, _) =
                                             space,
                                             string "::",
                                             space,
-                                            p_kind k,
+                                            p_kind env k,
                                             space,
                                             string "=>",
                                             space,
@@ -134,7 +145,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) =>
@@ -158,6 +169,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
 
@@ -261,7 +287,7 @@ fun p_exp' par env (e, loc) =
                                              space,
                                              string "::",
                                              space,
-                                             p_kind k,
+                                             p_kind env k,
                                              space,
                                              string "=>",
                                              space,
@@ -397,6 +423,15 @@ fun p_exp' par env (e, loc) =
                                     newline,
                                     p_exp (E.pushERel env x t) e2]
 
+      | 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
@@ -438,14 +473,14 @@ fun p_sgn_item env (sgi, _) =
                                     space,
                                     string "::",
                                     space,
-                                    p_kind k]
+                                    p_kind env k]
       | SgiCon (x, n, k, c) => box [string "con",
                                     space,
                                     p_named x n,
                                     space,
                                     string "::",
                                     space,
-                                    p_kind k,
+                                    p_kind env k,
                                     space,
                                     string "=",
                                     space,
@@ -559,7 +594,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/expl_util.sig b/src/expl_util.sig
index 2a6c7abe..3e5c333f 100644
--- a/src/expl_util.sig
+++ b/src/expl_util.sig
@@ -28,17 +28,24 @@
 signature EXPL_UTIL = sig
 
 structure Kind : sig
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * string -> 'context}
+                   -> ('context, Expl.kind, 'state, 'abort) Search.mapfolderB
     val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder
                   -> (Expl.kind, 'state, 'abort) Search.mapfolder
     val exists : (Expl.kind' -> bool) -> Expl.kind -> bool
+    val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
+                bind : 'context * string -> 'context}
+               -> 'context -> (Expl.kind -> Expl.kind)
 end
 
 structure Con : sig
     datatype binder =
-             Rel of string * Expl.kind
-           | Named of string * Expl.kind
+             RelK of string
+           | RelC of string * Expl.kind
+           | NamedC of string * Expl.kind
 
-    val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
                    -> ('context, Expl.con, 'state, 'abort) Search.mapfolderB
@@ -46,7 +53,7 @@ structure Con : sig
                    con : (Expl.con', 'state, 'abort) Search.mapfolder}
                   -> (Expl.con, 'state, 'abort) Search.mapfolder
 
-    val mapB : {kind : Expl.kind' -> Expl.kind',
+    val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
                 con : 'context -> Expl.con' -> Expl.con',
                 bind : 'context * binder -> 'context}
                -> 'context -> (Expl.con -> Expl.con)
@@ -59,12 +66,13 @@ end
 
 structure Exp : sig
     datatype binder =
-             RelC of string * Expl.kind
+             RelK of string
+           | RelC of string * Expl.kind
            | NamedC of string * Expl.kind
            | RelE of string * Expl.con
            | NamedE of string * Expl.con
 
-    val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Expl.exp', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
@@ -80,12 +88,13 @@ end
 
 structure Sgn : sig
     datatype binder =
-             RelC of string * Expl.kind
+             RelK of string
+           | RelC of string * Expl.kind
            | NamedC of string * Expl.kind
            | Sgn of string * Expl.sgn
            | Str of string * Expl.sgn
 
-    val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
                     sgn_item : ('context, Expl.sgn_item', 'state, 'abort) Search.mapfolderB,
                     sgn : ('context, Expl.sgn', 'state, 'abort) Search.mapfolderB,
diff --git a/src/expl_util.sml b/src/expl_util.sml
index febf3586..9e150b87 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -33,39 +33,55 @@ structure S = Search
 
 structure Kind = struct
 
-fun mapfold f =
+fun mapfoldB {kind, bind} =
     let
-        fun mfk k acc =
-            S.bindP (mfk' k acc, f)
+        fun mfk ctx k acc =
+            S.bindP (mfk' ctx k acc, kind 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 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 "ExplUtil.Kind.mapB: Impossible"
+
 fun exists f k =
     case mapfold (fn k => fn () =>
                              if f k then
@@ -80,12 +96,13 @@ end
 structure Con = struct
 
 datatype binder =
-         Rel of string * Expl.kind
-       | Named of string * Expl.kind
+         RelK of string
+       | RelC of string * Expl.kind
+       | NamedC of string * Expl.kind
 
 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)
@@ -99,9 +116,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 =>
@@ -119,16 +136,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,
@@ -146,9 +163,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)))
 
@@ -163,17 +180,32 @@ 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 ((), _) => ()} ()
 
 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
@@ -204,20 +236,22 @@ end
 structure Exp = struct
 
 datatype binder =
-         RelC of string * Expl.kind
+         RelK of string
+       | RelC of string * Expl.kind
        | NamedC of string * Expl.kind
        | RelE of string * Expl.con
        | NamedE of string * Expl.con
 
 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
@@ -254,7 +288,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' =>
@@ -338,12 +372,23 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                      S.map2 (mfe (bind (ctx, RelE (x, t))) e2,
                                           fn e2' =>
                                              (ELet (x, t', e1', e2'), 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)))
     in
         mfe
     end
 
 fun mapfold {kind = fk, con = fc, exp = fe} =
-    mapfoldB {kind = fk,
+    mapfoldB {kind = fn () => fk,
               con = fn () => fc,
               exp = fn () => fe,
               bind = fn ((), _) => ()} ()
@@ -372,7 +417,8 @@ end
 structure Sgn = struct
 
 datatype binder =
-         RelC of string * Expl.kind
+         RelK of string
+       | RelC of string * Expl.kind
        | NamedC of string * Expl.kind
        | Str of string * Expl.sgn
        | Sgn of string * Expl.sgn
@@ -382,14 +428,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
         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
         val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
 
-        val kind = Kind.mapfold kind
+        val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
 
         fun sgi ctx si acc =
             S.bindP (sgi' ctx si acc, sgn_item ctx)
@@ -397,11 +444,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
         and sgi' ctx (siAll as (si, loc)) =
             case si of
                 SgiConAbs (x, n, k) =>
-                S.map2 (kind k,
+                S.map2 (kind ctx k,
                      fn k' =>
                         (SgiConAbs (x, n, k'), loc))
               | SgiCon (x, n, k, c) =>
-                S.bind2 (kind k,
+                S.bind2 (kind ctx k,
                      fn k' =>
                         S.map2 (con ctx c,
                              fn c' =>
@@ -482,7 +529,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
     end
 
 fun mapfold {kind, con, sgn_item, sgn} =
-    mapfoldB {kind = kind,
+    mapfoldB {kind = fn () => kind,
               con = fn () => con,
               sgn_item = fn () => sgn_item,
               sgn = fn () => sgn,
diff --git a/src/explify.sml b/src/explify.sml
index 5bce9268..b2564789 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -45,6 +45,9 @@ fun explifyKind (k, loc) =
       | L.KUnif (_, _, ref (SOME k)) => explifyKind k
       | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
 
+      | L.KRel n => (L'.KRel n, loc)
+      | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc)
+
 fun explifyCon (c, loc) =
     case c of
         L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
@@ -74,6 +77,10 @@ fun explifyCon (c, loc) =
       | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
       | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
 
+      | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc)
+      | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc)
+      | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc)
+
 fun explifyPatCon pc =
     case pc of
         L.PConVar n => L'.PConVar n
@@ -123,6 +130,9 @@ fun explifyExp (e, loc) =
                     | L.EDVal (x, t, e') => (L'.ELet (x, explifyCon t, explifyExp e', e), loc))
         (explifyExp e) des
 
+      | L.EKAbs (x, e) => (L'.EKAbs (x, explifyExp e), loc)
+      | L.EKApp (e, k) => (L'.EKApp (explifyExp e, explifyKind k), loc)
+
 fun explifySgi (sgi, loc) =
     case sgi of
         L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)