# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1235337025 18000
# Node ID 588b9d16b00a8b3bac7c3b0f3d547bcbac750586
# Parent  d64533157f4024e4f88d515dbc97d37fae9ecebd
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top

diff -r d64533157f40 -r 588b9d16b00a lib/ur/top.ur
--- a/lib/ur/top.ur	Sat Feb 21 16:11:56 2009 -0500
+++ b/lib/ur/top.ur	Sun Feb 22 16:10:25 2009 -0500
@@ -1,3 +1,12 @@
+(** Row folding *)
+
+con folder = K ==> fn r :: {K} =>
+                      tf :: ({K} -> Type)
+                      -> (nm :: Name -> v :: K -> r :: {K} -> tf r
+                          -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
+                      -> tf [] -> tf r
+
+
 fun not b = if b then False else True
 
 con idT (t :: Type) = t
@@ -27,23 +36,23 @@
            (f : nm :: Name -> rest :: {Unit}
                 -> fn [[nm] ~ rest] =>
                       tf -> tr rest -> tr ([nm] ++ rest))
-           (i : tr []) =
+           (i : tr []) (r ::: {Unit}) (fold : folder r)=
     fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
-             (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
-                              [[nm] ~ rest] r =>
-                 f [nm] [rest] r.nm (acc (r -- nm)))
-             (fn _ => i)
+         (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+                          [[nm] ~ rest] r =>
+             f [nm] [rest] r.nm (acc (r -- nm)))
+         (fn _ => i)
 
 fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
            (f : nm :: Name -> rest :: {Unit}
                 -> fn [[nm] ~ rest] =>
                       tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
-           (i : tr []) =
+           (i : tr []) (r ::: {Unit}) (fold : folder r) =
     fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
-             (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
-                              [[nm] ~ rest] r1 r2 =>
-                 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
-             (fn _ _ => i)
+         (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+                          [[nm] ~ rest] r1 r2 =>
+             f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+         (fn _ _ => i)
 
 fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
            (f : nm :: Name -> rest :: {Unit}
@@ -54,134 +63,46 @@
                 <xml>{f [nm] [rest] v1 v2}{acc}</xml>)
             <xml/>
 
-fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
-           (f : nm :: Name -> t :: Type -> rest :: {Type}
+fun foldR K (tf :: K -> Type) (tr :: {K} -> Type)
+           (f : nm :: Name -> t :: K -> rest :: {K}
                 -> fn [[nm] ~ rest] =>
                       tf t -> tr rest -> tr ([nm = t] ++ rest))
-           (i : tr []) =
-    fold [fn r :: {Type} => $(map tf r) -> tr r]
-             (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest)
+           (i : tr []) (r ::: {K}) (fold : folder r) =
+    fold [fn r :: {K} => $(map tf r) -> tr r]
+             (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest)
                               [[nm] ~ rest] r =>
                  f [nm] [t] [rest] r.nm (acc (r -- nm)))
              (fn _ => i)
 
-fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
-            (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
-                 -> fn [[nm] ~ rest] =>
-                       tf t -> tr rest -> tr ([nm = t] ++ rest))
-            (i : tr []) =
-    fold [fn r :: {(Type * Type)} => $(map tf r) -> tr r]
-             (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                              (acc : _ -> tr rest) [[nm] ~ rest] r =>
-                 f [nm] [t] [rest] r.nm (acc (r -- nm)))
-             (fn _ => i)
-
-fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type)
-            (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                 -> fn [[nm] ~ rest] =>
-                       tf t -> tr rest -> tr ([nm = t] ++ rest))
-            (i : tr []) =
-    fold [fn r :: {(Type * Type * Type)} => $(map tf r) -> tr r]
-             (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
-                              (acc : _ -> tr rest) [[nm] ~ rest] r =>
-                 f [nm] [t] [rest] r.nm (acc (r -- nm)))
-             (fn _ => i)
-
-fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
-            (f : nm :: Name -> t :: Type -> rest :: {Type}
+fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type)
+            (f : nm :: Name -> t :: K -> rest :: {K}
                  -> fn [[nm] ~ rest] =>
                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-            (i : tr []) =
-    fold [fn r :: {Type} => $(map tf1 r) -> $(map tf2 r) -> tr r]
-             (fn (nm :: Name) (t :: Type) (rest :: {Type})
-                              (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
-                 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
-             (fn _ _ => i)
+            (i : tr []) (r ::: {K}) (fold : folder r) =
+    fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
+         (fn (nm :: Name) (t :: K) (rest :: {K})
+                          (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
+             f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+         (fn _ _ => i)
 
-fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
-             (tr :: {(Type * Type)} -> Type)
-             (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
-                  -> fn [[nm] ~ rest] =>
-                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-             (i : tr []) =
-    fold [fn r :: {(Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
-             (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                              (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
-                 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
-             (fn _ _ => i)
-
-fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
-             (tr :: {(Type * Type * Type)} -> Type)
-             (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                  -> fn [[nm] ~ rest] =>
-                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-             (i : tr []) =
-    fold [fn r :: {(Type * Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
-             (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
-                              (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
-                 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
-             (fn _ _ => i)
-
-fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
-            (f : nm :: Name -> t :: Type -> rest :: {Type}
+fun foldRX K (tf :: K -> Type) (ctx :: {Unit})
+            (f : nm :: Name -> t :: K -> rest :: {K}
                  -> fn [[nm] ~ rest] =>
                        tf t -> xml ctx [] []) =
-    foldTR [tf] [fn _ => xml ctx [] []]
-           (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc =>
-               <xml>{f [nm] [t] [rest] r}{acc}</xml>)
-           <xml/>
+    foldR [tf] [fn _ => xml ctx [] []]
+          (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc =>
+              <xml>{f [nm] [t] [rest] r}{acc}</xml>)
+          <xml/>
 
-fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
-             (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
-                  -> fn [[nm] ~ rest] =>
-                        tf t -> xml ctx [] []) =
-    foldT2R [tf] [fn _ => xml ctx [] []]
-            (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                             [[nm] ~ rest] r acc =>
-                <xml>{f [nm] [t] [rest] r}{acc}</xml>)
-            <xml/>
-
-fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit})
-             (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                  -> fn [[nm] ~ rest] =>
-                        tf t -> xml ctx [] []) =
-    foldT3R [tf] [fn _ => xml ctx [] []]
-            (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
-                             [[nm] ~ rest] r acc =>
-                <xml>{f [nm] [t] [rest] r}{acc}</xml>)
-            <xml/>
-
-fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
-             (f : nm :: Name -> t :: Type -> rest :: {Type}
+fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit})
+             (f : nm :: Name -> t :: K -> rest :: {K}
                   -> fn [[nm] ~ rest] =>
                         tf1 t -> tf2 t -> xml ctx [] []) =
-    foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
-            (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest]
-                             r1 r2 acc =>
-                <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
-            <xml/>
-
-fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
-              (ctx :: {Unit})
-              (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
-                   -> fn [[nm] ~ rest] =>
-                         tf1 t -> tf2 t -> xml ctx [] []) =
-    foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
-             (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
-                              [[nm] ~ rest] r1 r2 acc =>
-                 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
-             <xml/>
-
-fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
-              (ctx :: {Unit})
-              (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                   -> fn [[nm] ~ rest] =>
-                         tf1 t -> tf2 t -> xml ctx [] []) =
-    foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []]
-             (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
-                              [[nm] ~ rest] r1 r2 acc =>
-                 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
-             <xml/>
+    foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+           (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest]
+                            r1 r2 acc =>
+               <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
+           <xml/>
 
 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
            (q : sql_query tables exps) [tables ~ exps]
diff -r d64533157f40 -r 588b9d16b00a lib/ur/top.urs
--- a/lib/ur/top.urs	Sat Feb 21 16:11:56 2009 -0500
+++ b/lib/ur/top.urs	Sun Feb 22 16:10:25 2009 -0500
@@ -1,3 +1,12 @@
+(** Row folding *)
+
+con folder = K ==> fn r :: {K} =>
+                      tf :: ({K} -> Type)
+                      -> (nm :: Name -> v :: K -> r :: {K} -> tf r
+                          -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
+                      -> tf [] -> tf r
+
+
 val not : bool -> bool
 
 con idT = fn t :: Type => t
@@ -25,103 +34,46 @@
              -> (nm :: Name -> rest :: {Unit}
                  -> fn [[nm] ~ rest] =>
                        tf -> tr rest -> tr ([nm] ++ rest))
-             -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
+             -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r
 
 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
              -> (nm :: Name -> rest :: {Unit}
                  -> fn [[nm] ~ rest] =>
                        tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
-             -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
+             -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
 
 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
               -> (nm :: Name -> rest :: {Unit}
                   -> fn [[nm] ~ rest] =>
                         tf1 -> tf2 -> xml ctx [] [])
-              -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
+              -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
 
-val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
-             -> (nm :: Name -> t :: Type -> rest :: {Type}
+val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
+             -> (nm :: Name -> t :: K -> rest :: {K}
                  -> fn [[nm] ~ rest] =>
                        tf t -> tr rest -> tr ([nm = t] ++ rest))
-             -> tr [] -> r :: {Type} -> $(map tf r) -> tr r
+             -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
 
-val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
-              -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+             -> tr :: ({K} -> Type)
+             -> (nm :: Name -> t :: K -> rest :: {K}
+                 -> fn [[nm] ~ rest] =>
+                       tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+             -> tr []
+             -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
+
+val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
+             -> (nm :: Name -> t :: K -> rest :: {K}
+                 -> fn [[nm] ~ rest] =>
+                       tf t -> xml ctx [] [])
+             -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
+
+val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
+              -> (nm :: Name -> t :: K -> rest :: {K}
                   -> fn [[nm] ~ rest] =>
-                        tf t -> tr rest -> tr ([nm = t] ++ rest))
-              -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r
-
-val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
-              -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                  -> fn [[nm] ~ rest] =>
-                        tf t -> tr rest -> tr ([nm = t] ++ rest))
-              -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r
-
-val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
-              -> tr :: ({Type} -> Type)
-              -> (nm :: Name -> t :: Type -> rest :: {Type}
-                  -> fn [[nm] ~ rest] =>
-                        tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-              -> tr []
-              -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r
-                                                                    
-val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
-               -> tr :: ({(Type * Type)} -> Type)
-               -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
-                   -> fn [[nm] ~ rest] =>
-                         tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-               -> tr [] -> r :: {(Type * Type)}
-               -> $(map tf1 r) -> $(map tf2 r) -> tr r
-
-val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
-               -> tr :: ({(Type * Type * Type)} -> Type)
-               -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                   -> fn [[nm] ~ rest] =>
-                         tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-               -> tr [] -> r :: {(Type * Type * Type)}
-               -> $(map tf1 r) -> $(map tf2 r) -> tr r
-
-val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
-              -> (nm :: Name -> t :: Type -> rest :: {Type}
-                  -> fn [[nm] ~ rest] =>
-                        tf t -> xml ctx [] [])
-              -> r :: {Type} -> $(map tf r) -> xml ctx [] []
-
-val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
-               -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
-                   -> fn [[nm] ~ rest] =>
-                         tf t -> xml ctx [] [])
-               -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] []
-
-val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
-               -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                   -> fn [[nm] ~ rest] =>
-                         tf t -> xml ctx [] [])
-               -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] []
-
-val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
-               -> (nm :: Name -> t :: Type -> rest :: {Type}
-                   -> fn [[nm] ~ rest] =>
-                         tf1 t -> tf2 t -> xml ctx [] [])
-               -> r :: {Type}
-               -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
-
-val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
-                -> ctx :: {Unit}
-                -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
-                    -> fn [[nm] ~ rest] =>
-                          tf1 t -> tf2 t -> xml ctx [] [])
-                -> r :: {(Type * Type)}
-                -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
-
-
-val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
-                -> ctx :: {Unit}
-                -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
-                    -> fn [[nm] ~ rest] =>
-                          tf1 t -> tf2 t -> xml ctx [] [])
-                -> r :: {(Type * Type * Type)}
-                -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
+                        tf1 t -> tf2 t -> xml ctx [] [])
+              -> r ::: {K} -> folder r
+              -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
 
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
              -> sql_query tables exps
diff -r d64533157f40 -r 588b9d16b00a src/core.sml
--- a/src/core.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/core.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -96,7 +96,6 @@
        | EConcat of exp * con * exp * con
        | ECut of exp * con * { field : con, rest : con }
        | ECutMulti of exp * con * { rest : con }
-       | EFold of kind
 
        | ECase of exp * (pat * exp) list * { disc : con, result : con }
 
diff -r d64533157f40 -r 588b9d16b00a src/core_print.sml
--- a/src/core_print.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/core_print.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -342,7 +342,6 @@
                               string "---",
                               space,
                               p_con' true env c])
-      | EFold _ => string "fold"
 
       | ECase (e, pes, {disc, result}) =>
         parenIf par (box [string "case",
diff -r d64533157f40 -r 588b9d16b00a src/core_util.sml
--- a/src/core_util.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/core_util.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -454,10 +454,6 @@
       | (ECutMulti _, _) => LESS
       | (_, ECutMulti _) => GREATER
 
-      | (EFold _, EFold _) => EQUAL
-      | (EFold _, _) => LESS
-      | (_, EFold _) => GREATER
-
       | (ECase (e1, pes1, _), ECase (e2, pes2, _)) =>
         join (compare (e1, e2),
               fn () => joinL (fn ((p1, e1), (p2, e2)) =>
@@ -609,10 +605,6 @@
                                  S.map2 (mfc ctx rest,
                                       fn rest' =>
                                          (ECutMulti (e', c', {rest = rest'}), loc))))
-              | EFold k =>
-                S.map2 (mfk k,
-                         fn k' =>
-                            (EFold k', loc))
 
               | ECase (e, pes, {disc, result}) =>
                 S.bind2 (mfe ctx e,
diff -r d64533157f40 -r 588b9d16b00a src/corify.sml
--- a/src/corify.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/corify.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -592,7 +592,6 @@
                                                    {field = corifyCon st field, rest = corifyCon st rest}), loc)
       | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c,
                                                       {rest = corifyCon st rest}), loc)
-      | L.EFold k => (L'.EFold (corifyKind k), loc)
 
       | L.ECase (e, pes, {disc, result}) =>
         (L'.ECase (corifyExp st e,
diff -r d64533157f40 -r 588b9d16b00a src/elab.sml
--- a/src/elab.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -40,6 +40,9 @@
        | KError
        | KUnif of ErrorMsg.span * string * kind option ref
 
+       | KRel of int
+       | KFun of string * kind
+
 withtype kind = kind' located
 
 datatype explicitness =
@@ -62,6 +65,10 @@
        | CAbs of string * kind * con
        | CDisjoint of auto_instantiate * con * con * con
 
+       | CKAbs of string * con
+       | CKApp of con * kind
+       | TKFun of string * con
+
        | CName of string
 
        | CRecord of kind * (con * con) list
@@ -106,12 +113,14 @@
        | ECApp of exp * con
        | ECAbs of explicitness * 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
        | ECut of exp * con * { field : con, rest : con }
        | ECutMulti of exp * con * { rest : con }
-       | EFold of kind
 
        | ECase of exp * (pat * exp) list * { disc : con, result : con }
 
diff -r d64533157f40 -r 588b9d16b00a src/elab_env.sig
--- a/src/elab_env.sig	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_env.sig	Sun Feb 22 16:10:25 2009 -0500
@@ -47,6 +47,10 @@
            | Rel of int * 'a
            | Named of int * 'a
 
+    val pushKRel : env -> string -> env
+    val lookupKRel : env -> int -> string
+    val lookupK : env -> string -> int option
+
     val pushCRel : env -> string -> Elab.kind -> env
     val lookupCRel : env -> int -> string * Elab.kind
 
diff -r d64533157f40 -r 588b9d16b00a src/elab_env.sml
--- a/src/elab_env.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_env.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -45,8 +45,32 @@
 
 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,13 +80,27 @@
                                              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
 
+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 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 =>
@@ -76,7 +114,7 @@
                         | (bound, _) => bound}
 
 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
@@ -93,7 +131,7 @@
 val liftExp = liftExpInExp 0
 
 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
@@ -203,6 +241,9 @@
                                     print "\n")) cs)
 
 type env = {
+     renameK : int SM.map,
+     relK : string list,
+
      renameC : kind var' SM.map,
      relC : (string * kind) list,
      namedC : (string * kind * con option) IM.map,
@@ -234,6 +275,9 @@
     end
 
 val empty = {
+    renameK = SM.empty,
+    relK = [],
+
     renameC = SM.empty,
     relC = [],
     namedC = IM.empty,
@@ -261,12 +305,51 @@
       | CkProj _ => ck
       | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2)
 
+fun pushKRel (env : env) x =
+    let
+        val renameK = SM.map (fn n => n+1) (#renameK env)
+    in
+        {renameK = SM.insert (renameK, x, 0),
+         relK = x :: #relK env,
+
+         renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k)
+                            | x => x) (#renameC env),
+         relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
+         namedC = #namedC env,
+
+         datatypes = #datatypes env,
+         constructors = #constructors env,
+
+         classes = #classes env,
+
+         renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
+                            | Named' (n, c) => Named' (n, c)) (#renameE env),
+         relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
+         namedE = #namedE env,
+
+         renameSgn = #renameSgn env,
+         sgn = #sgn env,
+
+         renameStr = #renameStr env,
+         str = #str env
+        }
+    end
+
+fun lookupKRel (env : env) n =
+    (List.nth (#relK env, n))
+    handle Subscript => raise UnboundRel n
+
+fun lookupK (env : env) x = SM.find (#renameK env, x)
+
 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)),
+        {renameK = #renameK env,
+         relK = #relK env,
+
+         renameC = SM.insert (renameC, x, Rel' (0, k)),
          relC = (x, k) :: #relC env,
          namedC = #namedC env,
 
@@ -298,7 +381,10 @@
     handle Subscript => raise UnboundRel n
 
 fun pushCNamedAs (env : env) x n k co =
-    {renameC = SM.insert (#renameC env, x, Named' (n, k)),
+    {renameK = #renameK env,
+     relK = #relK env,
+
+     renameC = SM.insert (#renameC env, x, Named' (n, k)),
      relC = #relC env,
      namedC = IM.insert (#namedC env, n, (x, k, co)),
 
@@ -340,7 +426,10 @@
     let
         val dk = U.classifyDatatype xncs
     in
-        {renameC = #renameC env,
+        {renameK = #renameK env,
+         relK = #relK env,
+
+         renameC = #renameC env,
          relC = #relC env,
          namedC = #namedC env,
 
@@ -380,7 +469,10 @@
 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
 
 fun pushClass (env : env) n =
-    {renameC = #renameC env,
+    {renameK = #renameK env,
+     relK = #relK env,
+
+     renameC = #renameC env,
      relC = #relC env,
      namedC = #namedC env,
 
@@ -468,7 +560,10 @@
                                   CM.insert (classes, f, class)
                               end
     in
-        {renameC = #renameC env,
+        {renameK = #renameK env,
+         relK = #relK env,
+
+         renameC = #renameC env,
          relC = #relC env,
          namedC = #namedC env,
 
@@ -509,7 +604,10 @@
                                   CM.insert (classes, f, class)
                               end
     in
-        {renameC = #renameC env,
+        {renameK = #renameK env,
+         relK = #relK env,
+
+         renameC = #renameC env,
          relC = #relC env,
          namedC = #namedC env,
 
@@ -552,7 +650,10 @@
       | SOME (Named' x) => Named x
 
 fun pushSgnNamedAs (env : env) x n sgis =
-    {renameC = #renameC env,
+    {renameK = #renameK env,
+     relK = #relK env,
+
+     renameC = #renameC env,
      relC = #relC env,
      namedC = #namedC env,
 
@@ -868,7 +969,10 @@
       | _ => classes
 
 fun pushStrNamedAs (env : env) x n sgn =
-    {renameC = #renameC env,
+    {renameK = #renameK env,
+     relK = #relK env,
+
+     renameC = #renameC env,
      relC = #relC env,
      namedC = #namedC env,
 
diff -r d64533157f40 -r 588b9d16b00a src/elab_err.sig
--- a/src/elab_err.sig	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_err.sig	Sun Feb 22 16:10:25 2009 -0500
@@ -27,11 +27,16 @@
 
 signature ELAB_ERR = sig
 
+    datatype kind_error =
+             UnboundKind of ErrorMsg.span * string
+
+    val kindError : ElabEnv.env -> kind_error -> unit
+
     datatype kunify_error =
              KOccursCheckFailed of Elab.kind * Elab.kind
            | KIncompatible of Elab.kind * Elab.kind
 
-    val kunifyError : kunify_error -> unit
+    val kunifyError : ElabEnv.env -> kunify_error -> unit
 
     datatype con_error =
              UnboundCon of ErrorMsg.span * string
diff -r d64533157f40 -r 588b9d16b00a src/elab_err.sml
--- a/src/elab_err.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_err.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -36,7 +36,7 @@
 open Print
 structure P = ElabPrint
 
-val simplCon = U.Con.mapB {kind = fn k => k,
+val simplCon = U.Con.mapB {kind = fn _ => fn k => k,
                            con = fn env => fn c =>
                                               let
                                                   val c = (c, ErrorMsg.dummySpan)
@@ -46,25 +46,34 @@
                                                                     ("c'", P.p_con env c')];*)
                                                   #1 c'
                                               end,
-                           bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k
-                                   | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE}
+                           bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k
+                                   | (env, U.Con.NamedC (x, n, k)) => E.pushCNamedAs env x n k NONE
+                                   | (env, _) => env}
 
 val p_kind = P.p_kind
+             
+datatype kind_error =
+         UnboundKind of ErrorMsg.span * string
+
+fun kindError env err =
+    case err of
+        UnboundKind (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
 
 datatype kunify_error =
          KOccursCheckFailed of kind * kind
        | KIncompatible of kind * kind
 
-fun kunifyError err =
+fun kunifyError env err =
     case err of
         KOccursCheckFailed (k1, k2) =>
         eprefaces "Kind occurs check failed"
-        [("Kind 1", p_kind k1),
-         ("Kind 2", p_kind k2)]
+        [("Kind 1", p_kind env k1),
+         ("Kind 2", p_kind env k2)]
       | KIncompatible (k1, k2) =>
         eprefaces "Incompatible kinds"
-        [("Kind 1", p_kind k1),
-         ("Kind 2", p_kind k2)]
+        [("Kind 1", p_kind env k1),
+         ("Kind 2", p_kind env k2)]
 
 
 fun p_con env c = P.p_con env (simplCon env c)
@@ -89,9 +98,9 @@
       | WrongKind (c, k1, k2, kerr) =>
         (ErrorMsg.errorAt (#2 c) "Wrong kind";
          eprefaces' [("Constructor", p_con env c),
-                     ("Have kind", p_kind k1),
-                     ("Need kind", p_kind k2)];
-         kunifyError kerr)
+                     ("Have kind", p_kind env k1),
+                     ("Need kind", p_kind env k2)];
+         kunifyError env kerr)
       | DuplicateField (loc, s) =>
         ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
       | ProjBounds (c, n) =>
@@ -101,7 +110,7 @@
       | ProjMismatch (c, k) =>
         (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
          eprefaces' [("Constructor", p_con env c),
-                     ("Kind", p_kind k)])
+                     ("Kind", p_kind env k)])
 
 
 datatype cunify_error =
@@ -116,9 +125,9 @@
     case err of
         CKind (k1, k2, kerr) =>
         (eprefaces "Kind unification failure"
-                   [("Kind 1", p_kind k1),
-                    ("Kind 2", p_kind k2)];
-         kunifyError kerr)
+                   [("Kind 1", p_kind env k1),
+                    ("Kind 2", p_kind env k2)];
+         kunifyError env kerr)
       | COccursCheckFailed (c1, c2) =>
         eprefaces "Constructor occurs check failed"
                   [("Con 1", p_con env c1),
@@ -133,7 +142,7 @@
                    ("Con 2", p_con env c2)]
       | CKindof (k, c, expected) =>
         eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
-                  [("Kind", p_kind k),
+                  [("Kind", p_kind env k),
                    ("Con", p_con env c)]
       | CRecordFailure (c1, c2) =>
         eprefaces "Can't unify record constructors"
@@ -267,9 +276,9 @@
         (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
          eprefaces' [("Have", p_sgn_item env sgi1),
                      ("Need", p_sgn_item env sgi2),
-                     ("Kind 1", p_kind k1),
-                     ("Kind 2", p_kind k2)];
-         kunifyError kerr)
+                     ("Kind 1", p_kind env k1),
+                     ("Kind 2", p_kind env k2)];
+         kunifyError env kerr)
       | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
         (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
          eprefaces' [("Have", p_sgn_item env sgi1),
@@ -296,9 +305,9 @@
                      ("Field", PD.string x)])
       | WhereWrongKind (k1, k2, kerr) =>
         (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
-         eprefaces' [("Have", p_kind k1),
-                     ("Need", p_kind k2)];
-         kunifyError kerr)
+         eprefaces' [("Have", p_kind env k1),
+                     ("Need", p_kind env k2)];
+         kunifyError env kerr)
       | NotIncludable sgn =>
         (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
          eprefaces' [("Signature", p_sgn env sgn)])
@@ -337,10 +346,10 @@
          eprefaces' [("Signature", p_sgn env sgn)])
       | NotType (k, (k1, k2, ue)) =>
         (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
-         eprefaces' [("Kind", p_kind k),
-                     ("Subkind 1", p_kind k1),
-                     ("Subkind 2", p_kind k2)];
-         kunifyError ue)
+         eprefaces' [("Kind", p_kind env k),
+                     ("Subkind 1", p_kind env k1),
+                     ("Subkind 2", p_kind env k2)];
+         kunifyError env ue)
       | DuplicateConstructor (x, loc) =>
         ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
       | NotDatatype loc =>
diff -r d64533157f40 -r 588b9d16b00a src/elab_ops.sig
--- a/src/elab_ops.sig	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_ops.sig	Sun Feb 22 16:10:25 2009 -0500
@@ -27,6 +27,12 @@
 
 signature ELAB_OPS = sig
 
+    val liftKindInKind : int -> Elab.kind -> Elab.kind
+    val subKindInKind : int * Elab.kind -> Elab.kind -> Elab.kind
+
+    val liftKindInCon : int -> Elab.con -> Elab.con
+    val subKindInCon : int * Elab.kind -> Elab.con -> Elab.con
+
     val liftConInCon : int -> Elab.con -> Elab.con
     val subConInCon : int * Elab.con -> Elab.con -> Elab.con
     val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn
diff -r d64533157f40 -r 588b9d16b00a src/elab_ops.sml
--- a/src/elab_ops.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_ops.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -32,8 +32,64 @@
 structure E = ElabEnv
 structure U = ElabUtil
 
+fun liftKindInKind' by =
+    U.Kind.mapB {kind = fn bound => fn k =>
+                                       case k of
+                                         KRel xn =>
+                                         if xn < bound then
+                                             k
+                                         else
+                                             KRel (xn + by)
+                                       | _ => k,
+                bind = fn (bound, _) => bound + 1}
+
+fun subKindInKind' rep =
+    U.Kind.mapB {kind = fn (by, xn) => fn k =>
+                                          case k of
+                                              KRel xn' =>
+                                              (case Int.compare (xn', xn) of
+                                                   EQUAL => #1 (liftKindInKind' by 0 rep)
+                                                 | GREATER => KRel (xn' - 1)
+                                                 | LESS => k)
+                                            | _ => k,
+                 bind = fn ((by, xn), _) => (by+1, xn+1)}
+
+val liftKindInKind = liftKindInKind' 1
+
+fun subKindInKind (xn, rep) = subKindInKind' rep (0, xn)
+
+fun liftKindInCon by =
+    U.Con.mapB {kind = fn bound => fn k =>
+                                      case k of
+                                          KRel xn =>
+                                          if xn < bound then
+                                              k
+                                          else
+                                              KRel (xn + by)
+                                        | _ => k,
+                con = fn _ => fn c => c,
+                bind = fn (bound, U.Con.RelK _) => bound + 1
+                        | (bound, _) => bound}
+
+fun subKindInCon' rep =
+    U.Con.mapB {kind = fn (by, xn) => fn k =>
+                                         case k of
+                                             KRel xn' =>
+                                             (case Int.compare (xn', xn) of
+                                                  EQUAL => #1 (liftKindInKind' by 0 rep)
+                                                | GREATER => KRel (xn' - 1)
+                                                | LESS => k)
+                                           | _ => k,
+                con = fn _ => fn c => c,
+                bind = fn ((by, xn), U.Con.RelK _) => (by+1, xn+1)
+                        | (st, _) => st}
+
+val liftKindInCon = liftKindInCon 1
+
+fun subKindInCon (xn, rep) = subKindInCon' rep (0, xn)
+
 fun liftConInCon by =
-    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 =>
@@ -43,11 +99,11 @@
                                              CRel (xn + by)
                                        (*| CUnif _ => raise SynUnif*)
                                        | _ => c,
-                bind = fn (bound, U.Con.Rel _) => bound + 1
+                bind = fn (bound, U.Con.RelC _) => bound + 1
                         | (bound, _) => bound}
 
 fun subConInCon' rep =
-    U.Con.mapB {kind = fn k => k,
+    U.Con.mapB {kind = fn _ => fn k => k,
                 con = fn (by, xn) => fn c =>
                                         case c of
                                             CRel xn' =>
@@ -57,7 +113,7 @@
                                                | LESS => c)
                                           (*| CUnif _ => raise SynUnif*)
                                           | _ => c,
-                bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1)
+                bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1)
                         | (ctx, _) => ctx}
 
 val liftConInCon = liftConInCon 1
@@ -205,6 +261,11 @@
                    | _ => default ()
              end
            | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
+
+      | CKApp (c1, k) =>
+        (case hnormCon env c1 of
+             (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body)
+           | _ => cAll)
         
       | CConcat (c1, c2) =>
         (case (hnormCon env c1, hnormCon env c2) of
diff -r d64533157f40 -r 588b9d16b00a src/elab_print.sig
--- a/src/elab_print.sig	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_print.sig	Sun Feb 22 16:10:25 2009 -0500
@@ -28,7 +28,7 @@
 (* Pretty-printing Ur/Web *)
 
 signature ELAB_PRINT = sig
-    val p_kind : Elab.kind Print.printer
+    val p_kind : ElabEnv.env -> Elab.kind Print.printer
     val p_explicitness : Elab.explicitness Print.printer
     val p_con : ElabEnv.env -> Elab.con Print.printer
     val p_pat : ElabEnv.env -> Elab.pat Print.printer
diff -r d64533157f40 -r 588b9d16b00a src/elab_print.sml
--- a/src/elab_print.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_print.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -38,25 +38,36 @@
 
 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 ")"]
 
       | KError => string "<ERROR>"
-      | KUnif (_, _, ref (SOME k)) => p_kind' par k
+      | KUnif (_, _, ref (SOME k)) => p_kind' par env k
       | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
 
+      | 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 k = p_kind' false k
 
 fun p_explicitness e =
@@ -66,7 +77,7 @@
 
 fun p_con' par env (c, _) =
     case c of
-        TFun (t1, t2) => parenIf par (box [p_con' true env t1,
+        TFun (t1, t2) => parenIf true (box [p_con' true env t1,
                                            space,
                                            string "->",
                                            space,
@@ -75,20 +86,22 @@
                                                 space,
                                                 p_explicitness e,
                                                 space,
-                                                p_kind k,
+                                                p_kind env k,
                                                 space,
                                                 string "->",
                                                 space,
                                                 p_con (E.pushCRel env x k) c])
-      | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
-                                                       space,
-                                                       string "~",
-                                                       space,
-                                                       p_con env c2,
-                                                       space,
-                                                       string "=>",
-                                                       space,
-                                                       p_con env c3])
+      | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1,
+                                                        space,
+                                                        string (case ai of
+                                                                    Instantiate => "~"
+                                                                  | LeaveAlone => "~~"),
+                                                        space,
+                                                        p_con env c2,
+                                                        space,
+                                                        string "=>",
+                                                        space,
+                                                        p_con env c3])
       | TRecord (CRecord (_, xcs), _) => box [string "{",
                                               p_list (fn (x, c) =>
                                                          box [p_name env x,
@@ -134,7 +147,7 @@
                                              space,
                                              string "::",
                                              space,
-                                             p_kind k,
+                                             p_kind env k,
                                              space,
                                              string "=>",
                                              space,
@@ -152,7 +165,7 @@
                                               space,
                                               p_con env c]) xcs,
                               string "]::",
-                              p_kind k])
+                              p_kind env k])
         else
             parenIf par (box [string "[",
                               p_list (fn (x, c) =>
@@ -181,8 +194,24 @@
       | CError => string "<ERROR>"
       | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
       | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
-                                   p_kind k,
+                                   p_kind env k,
                                    string ">"]
+
+      | 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
 
@@ -286,7 +315,7 @@
                                                   space,
                                                   p_explicitness exp,
                                                   space,
-                                                  p_kind k,
+                                                  p_kind env k,
                                                   space,
                                                   string "=>",
                                                   space,
@@ -377,8 +406,6 @@
                               space,
                               p_con' true env c])
 
-      | EFold _ => string "fold"
-
       | ECase (e, pes, _) => parenIf par (box [string "case",
                                                space,
                                                p_exp env e,
@@ -415,6 +442,16 @@
                  string "end"]
         end
 
+      | 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
 
 and p_edecl env (dAll as (d, _)) =
@@ -478,14 +515,14 @@
                                     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,
@@ -540,14 +577,14 @@
                                       space,
                                       string "::",
                                       space,
-                                      p_kind k]
+                                      p_kind env k]
       | SgiClass (x, n, k, c) => box [string "class",
                                       space,
                                       p_named x n,
                                       space,
                                       string "::",
                                       space,
-                                      p_kind k,
+                                      p_kind env k,
                                       space,
                                       string "=",
                                       space,
@@ -627,7 +664,7 @@
                                   space,
                                   string "::",
                                   space,
-                                  p_kind k,
+                                  p_kind env k,
                                   space,
                                   string "=",
                                   space,
@@ -719,7 +756,7 @@
                                     space,
                                     string "::",
                                     space,
-                                    p_kind k,
+                                    p_kind env k,
                                     space,
                                     string "=",
                                     space,
diff -r d64533157f40 -r 588b9d16b00a src/elab_util.sig
--- a/src/elab_util.sig	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_util.sig	Sun Feb 22 16:10:25 2009 -0500
@@ -30,17 +30,24 @@
 val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind
 
 structure Kind : sig
+    val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * string -> 'context}
+                   -> ('context, Elab.kind, 'state, 'abort) Search.mapfolderB
     val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder
                   -> (Elab.kind, 'state, 'abort) Search.mapfolder
     val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
+    val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
+                bind : 'context * string -> 'context}
+               -> 'context -> (Elab.kind -> Elab.kind)
 end
 
 structure Con : sig
     datatype binder =
-             Rel of string * Elab.kind
-           | Named of string * int * Elab.kind
+             RelK of string
+           | RelC of string * Elab.kind
+           | NamedC of string * int * Elab.kind
 
-    val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
                    -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB
@@ -48,7 +55,7 @@
                    con : (Elab.con', 'state, 'abort) Search.mapfolder}
                   -> (Elab.con, 'state, 'abort) Search.mapfolder
 
-    val mapB : {kind : Elab.kind' -> Elab.kind',
+    val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
                 con : 'context -> Elab.con' -> Elab.con',
                 bind : 'context * binder -> 'context}
                -> 'context -> (Elab.con -> Elab.con)
@@ -58,7 +65,7 @@
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool} -> Elab.con -> bool
 
-    val foldB : {kind : Elab.kind' * 'state -> 'state,
+    val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
                  con : 'context * Elab.con' * 'state -> 'state,
                  bind : 'context * binder -> 'context}
                 -> 'context -> 'state -> Elab.con -> 'state
@@ -66,12 +73,13 @@
 
 structure Exp : sig
     datatype binder =
-             RelC of string * Elab.kind
+             RelK of string
+           | RelC of string * Elab.kind
            | NamedC of string * int * Elab.kind
            | RelE of string * Elab.con
            | NamedE of string * Elab.con
 
-    val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
                     bind : 'context * binder -> 'context}
@@ -80,7 +88,7 @@
                    con : (Elab.con', 'state, 'abort) Search.mapfolder,
                    exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
                   -> (Elab.exp, 'state, 'abort) Search.mapfolder
-    val mapB : {kind : Elab.kind' -> Elab.kind',
+    val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
                 con : 'context -> Elab.con' -> Elab.con',
                 exp : 'context -> Elab.exp' -> Elab.exp',
                 bind : 'context * binder -> 'context}
@@ -89,7 +97,7 @@
                   con : Elab.con' -> bool,
                   exp : Elab.exp' -> bool} -> Elab.exp -> bool
 
-    val foldB : {kind : Elab.kind' * 'state -> 'state,
+    val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
                  con : 'context * Elab.con' * 'state -> 'state,
                  exp : 'context * Elab.exp' * 'state -> 'state,
                  bind : 'context * binder -> 'context}
@@ -98,12 +106,13 @@
 
 structure Sgn : sig
     datatype binder =
-             RelC of string * Elab.kind
+             RelK of string
+           | RelC of string * Elab.kind
            | NamedC of string * int * Elab.kind
            | Str of string * Elab.sgn
            | Sgn of string * Elab.sgn
 
-    val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
                     sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
                     sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
@@ -127,14 +136,15 @@
 
 structure Decl : sig
     datatype binder =
-             RelC of string * Elab.kind
+             RelK of string
+           | RelC of string * Elab.kind
            | NamedC of string * int * Elab.kind
            | RelE of string * Elab.con
            | NamedE of string * Elab.con
            | Str of string * Elab.sgn
            | Sgn of string * Elab.sgn
 
-    val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+    val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
                     exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
                     sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
@@ -168,7 +178,7 @@
                   decl : Elab.decl' -> 'a option}
                  -> Elab.decl -> 'a option
 
-    val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state,
+    val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state,
                     con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
                     exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
                     sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
diff -r d64533157f40 -r 588b9d16b00a src/elab_util.sml
--- a/src/elab_util.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_util.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -43,44 +43,60 @@
 
 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))
 
               | KError => S.return2 kAll
 
-              | KUnif (_, _, ref (SOME k)) => mfk' k
+              | KUnif (_, _, ref (SOME k)) => mfk' ctx k
               | KUnif _ => S.return2 kAll
+
+              | 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 "ElabUtil.Kind.mapB: Impossible"
+
 fun exists f k =
     case mapfold (fn k => fn () =>
                              if f k then
@@ -95,12 +111,13 @@
 structure Con = struct
 
 datatype binder =
-         Rel of string * Elab.kind
-       | Named of string * int * Elab.kind
+         RelK of string
+       | RelC of string * Elab.kind
+       | NamedC of string * int * Elab.kind
 
 fun mapfoldB {kind = fk, con = fc, bind} =
     let
-        val mfk = Kind.mapfold fk
+        val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)}
 
         fun mfc ctx c acc =
             S.bindP (mfc' ctx c acc, fc ctx)
@@ -114,9 +131,9 @@
                               fn c2' =>
                                  (TFun (c1', c2'), loc)))
               | TCFun (e, 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 (e, x, k', c'), loc)))
               | CDisjoint (ai, c1, c2, c3) =>
@@ -142,16 +159,16 @@
                               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,
@@ -169,9 +186,9 @@
                               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)))
 
@@ -190,17 +207,32 @@
               | CError => S.return2 cAll
               | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
               | CUnif _ => S.return2 cAll
+
+              | 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
@@ -227,7 +259,7 @@
       | S.Continue _ => false
 
 fun foldB {kind, con, bind} ctx st c =
-    case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+    case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
                    con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
                    bind = bind} ctx c st of
         S.Continue (_, st) => st
@@ -238,20 +270,22 @@
 structure Exp = struct
 
 datatype binder =
-         RelC of string * Elab.kind
+         RelK of string
+       | RelC of string * Elab.kind
        | NamedC of string * int * Elab.kind
        | RelE of string * Elab.con
        | NamedE of string * Elab.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
@@ -288,7 +322,7 @@
                               fn c' =>
                                  (ECApp (e', c'), loc)))
               | ECAbs (expl, 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' =>
@@ -347,11 +381,6 @@
                                       fn rest' =>
                                          (ECutMulti (e', c', {rest = rest'}), loc))))
 
-              | EFold k =>
-                S.map2 (mfk k,
-                         fn k' =>
-                            (EFold k', loc))
-
               | ECase (e, pes, {disc, result}) =>
                 S.bind2 (mfe ctx e,
                          fn e' =>
@@ -406,6 +435,17 @@
                                        (ELet (des', e'), loc)))
                 end
 
+              | 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 mfed ctx (dAll as (d, loc)) =
             case d of
                 EDVal vi =>
@@ -432,7 +472,7 @@
     end
 
 fun mapfold {kind = fk, con = fc, exp = fe} =
-    mapfoldB {kind = fk,
+    mapfoldB {kind = fn () => fk,
               con = fn () => fc,
               exp = fn () => fe,
               bind = fn ((), _) => ()} ()
@@ -457,7 +497,7 @@
       | S.Continue _ => false
 
 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
@@ -465,7 +505,7 @@
       | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
 
 fun foldB {kind, con, exp, bind} ctx st e =
-    case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+    case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
                    con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
                    exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
                    bind = bind} ctx e st of
@@ -477,7 +517,8 @@
 structure Sgn = struct
 
 datatype binder =
-         RelC of string * Elab.kind
+         RelK of string
+       | RelC of string * Elab.kind
        | NamedC of string * int * Elab.kind
        | Str of string * Elab.sgn
        | Sgn of string * Elab.sgn
@@ -487,14 +528,15 @@
         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)
@@ -502,11 +544,11 @@
         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' =>
@@ -548,11 +590,11 @@
                                     fn c2' =>
                                        (SgiConstraint (c1', c2'), loc)))
               | SgiClassAbs (x, n, k) =>
-                S.map2 (kind k,
+                S.map2 (kind ctx k,
                         fn k' =>
                            (SgiClassAbs (x, n, k'), loc))
               | SgiClass (x, n, k, c) =>
-                S.bind2 (kind k,
+                S.bind2 (kind ctx k,
                       fn k' => 
                          S.map2 (con ctx c,
                               fn c' =>
@@ -608,7 +650,7 @@
     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,
@@ -627,7 +669,8 @@
 structure Decl = struct
 
 datatype binder =
-         RelC of string * Elab.kind
+         RelK of string
+       | RelC of string * Elab.kind
        | NamedC of string * int * Elab.kind
        | RelE of string * Elab.con
        | NamedE of string * Elab.con
@@ -636,13 +679,14 @@
 
 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, 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
@@ -651,7 +695,8 @@
         fun bind' (ctx, b) =
             let
                 val b' = case b of
-                             Exp.RelC x => RelC x
+                             Exp.RelK x => RelK x
+                           | Exp.RelC x => RelC x
                            | Exp.NamedC x => NamedC x
                            | Exp.RelE x => RelE x
                            | Exp.NamedE x => NamedE x
@@ -663,7 +708,8 @@
         fun bind' (ctx, b) =
             let
                 val b' = case b of
-                             Sgn.RelC x => RelC x
+                             Sgn.RelK x => RelK x
+                           | Sgn.RelC x => RelC x
                            | Sgn.NamedC x => NamedC x
                            | Sgn.Sgn x => Sgn x
                            | Sgn.Str x => Str x
@@ -760,7 +806,7 @@
         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' =>
@@ -825,7 +871,7 @@
               | DSequence _ => S.return2 dAll
 
               | DClass (x, n, k, c) =>
-                S.bind2 (mfk k,
+                S.bind2 (mfk ctx k,
                          fn k' =>
                             S.map2 (mfc ctx c,
                                  fn c' =>
@@ -849,7 +895,7 @@
     end
 
 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
-    mapfoldB {kind = kind,
+    mapfoldB {kind = fn () => kind,
               con = fn () => con,
               exp = fn () => exp,
               sgn_item = fn () => sgn_item,
@@ -938,7 +984,7 @@
       | S.Continue _ => NONE
 
 fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
-    case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)),
+    case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, x, st)),
                    con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
                    exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
                    sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
diff -r d64533157f40 -r 588b9d16b00a src/elaborate.sml
--- a/src/elaborate.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elaborate.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -61,7 +61,7 @@
 
  exception KUnify' of kunify_error
 
- fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
+ fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
      let
          fun err f = raise KUnify' (f (k1All, k2All))
      in
@@ -70,19 +70,27 @@
            | (L'.KUnit, L'.KUnit) => ()
 
            | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
-             (unifyKinds' d1 d2;
-              unifyKinds' r1 r2)
+             (unifyKinds' env d1 d2;
+              unifyKinds' env r1 r2)
            | (L'.KName, L'.KName) => ()
-           | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
+           | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2
            | (L'.KTuple ks1, L'.KTuple ks2) =>
-             ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2))
+             ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2))
               handle ListPair.UnequalLengths => err KIncompatible)
 
+           | (L'.KRel n1, L'.KRel n2) =>
+             if n1 = n2 then
+                 ()
+             else
+                 err KIncompatible
+           | (L'.KFun (x, k1), L'.KFun (_, k2)) =>
+             unifyKinds' (E.pushKRel env x) k1 k2
+
            | (L'.KError, _) => ()
            | (_, L'.KError) => ()
 
-           | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
-           | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
+           | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
+           | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
 
            | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
              if r1 = r2 then
@@ -106,12 +114,12 @@
 
  exception KUnify of L'.kind * L'.kind * kunify_error
 
- fun unifyKinds k1 k2 =
-     unifyKinds' k1 k2
+ fun unifyKinds env k1 k2 =
+     unifyKinds' env k1 k2
      handle KUnify' err => raise KUnify (k1, k2, err)
 
  fun checkKind env c k1 k2 =
-     unifyKinds k1 k2
+     unifyKinds env k1 k2
      handle KUnify (k1, k2, err) =>
             conError env (WrongKind (c, k1, k2, err))
 
@@ -172,16 +180,23 @@
 
  end
 
- fun elabKind (k, loc) =
+ fun elabKind env (k, loc) =
      case k of
          L.KType => (L'.KType, loc)
-       | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
+       | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc)
        | L.KName => (L'.KName, loc)
-       | L.KRecord k => (L'.KRecord (elabKind k), loc)
+       | L.KRecord k => (L'.KRecord (elabKind env k), loc)
        | L.KUnit => (L'.KUnit, loc)
-       | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
+       | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
        | L.KWild => kunif loc
 
+       | L.KVar s => (case E.lookupK env s of
+                          NONE =>
+                          (kindError env (UnboundKind (loc, s));
+                           kerror)
+                        | SOME n => (L'.KRel n, loc))
+       | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc)
+
  fun mapKind (dom, ran, loc)=
      (L'.KArrow ((L'.KArrow (dom, ran), loc),
                  (L'.KArrow ((L'.KRecord dom, loc),
@@ -192,11 +207,31 @@
          L'.KUnif (_, _, ref (SOME k)) => hnormKind k
        | _ => kAll
 
+ open ElabOps
+ val hnormCon = D.hnormCon
+
+ fun elabConHead (c as (_, loc)) k =
+     let
+         fun unravel (k, c) =
+             case hnormKind k of
+                 (L'.KFun (x, k'), _) =>
+                 let
+                     val u = kunif loc
+                             
+                     val k'' = subKindInKind (0, u) k'
+                 in
+                     unravel (k'', (L'.CKApp (c, u), loc))
+                 end
+               | _ => (c, k)
+    in
+         unravel (k, c)
+    end
+
  fun elabCon (env, denv) (c, loc) =
      case c of
          L.CAnnot (c, k) =>
          let
-             val k' = elabKind k
+             val k' = elabKind env k
              val (c', ck, gs) = elabCon (env, denv) c
          in
              checkKind env c' ck k';
@@ -215,13 +250,21 @@
        | L.TCFun (e, x, k, t) =>
          let
              val e' = elabExplicitness e
-             val k' = elabKind k
+             val k' = elabKind env k
              val env' = E.pushCRel env x k'
              val (t', tk, gs) = elabCon (env', D.enter denv) t
          in
              checkKind env t' tk ktype;
              ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
          end
+       | L.TKFun (x, t) =>
+         let
+             val env' = E.pushKRel env x
+             val (t', tk, gs) = elabCon (env', denv) t
+         in
+             checkKind env t' tk ktype;
+             ((L'.TKFun (x, t'), loc), ktype, gs)
+         end
        | L.CDisjoint (c1, c2, c) =>
          let
              val (c1', k1, gs1) = elabCon (env, denv) c1
@@ -253,9 +296,17 @@
               (conError env (UnboundCon (loc, s));
                (cerror, kerror, []))
             | E.Rel (n, k) =>
-              ((L'.CRel n, loc), k, [])
+              let
+                  val (c, k) = elabConHead (L'.CRel n, loc) k
+              in
+                  (c, k, [])
+              end
             | E.Named (n, k) =>
-              ((L'.CNamed n, loc), k, []))
+              let
+                  val (c, k) = elabConHead (L'.CNamed n, loc) k
+              in
+                  (c, k, [])
+              end)
        | L.CVar (m1 :: ms, s) =>
          (case E.lookupStr env m1 of
               NONE => (conError env (UnboundStrInCon (loc, m1));
@@ -292,7 +343,7 @@
          let
              val k' = case ko of
                           NONE => kunif loc
-                        | SOME k => elabKind k
+                        | SOME k => elabKind env k
              val env' = E.pushCRel env x k'
              val (t', tk, gs) = elabCon (env', D.enter denv) t
          in
@@ -300,6 +351,15 @@
               (L'.KArrow (k', tk), loc),
               gs)
          end
+       | L.CKAbs (x, t) =>
+         let
+             val env' = E.pushKRel env x
+             val (t', tk, gs) = elabCon (env', denv) t
+         in
+             ((L'.CKAbs (x, t'), loc),
+              (L'.KFun (x, tk), loc),
+              gs)
+         end
 
        | L.CName s =>
          ((L'.CName s, loc), kname, [])
@@ -392,7 +452,7 @@
 
        | L.CWild k =>
          let
-             val k' = elabKind k
+             val k' = elabKind env k
          in
              (cunif (loc, k'), k', [])
          end
@@ -431,8 +491,6 @@
 
  exception SynUnif = E.SynUnif
 
- open ElabOps
-
  type record_summary = {
       fields : (L'.con * L'.con) list,
       unifs : (L'.con * L'.con option ref) list,
@@ -499,7 +557,12 @@
        | L'.CError => kerror
        | L'.CUnif (_, k, _, _) => k
 
- val hnormCon = D.hnormCon
+       | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
+       | L'.CKApp (c, k) =>
+         (case hnormKind (kindof env c) of
+              (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
+            | k => raise CUnify' (CKindof (k, c, "kapp")))
+       | L'.TKFun _ => ktype
 
  fun deConstraintCon (env, denv) c =
      let
@@ -564,6 +627,10 @@
        | L'.CError => false
        | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit
 
+       | L'.CKAbs _ => false
+       | L'.CKApp _ => false
+       | L'.TKFun _ => false
+
  fun unifyRecordCons (env, denv) (c1, c2) =
      let
          fun rkindof c =
@@ -578,7 +645,7 @@
          val (r1, gs1) = recordSummary (env, denv) c1
          val (r2, gs2) = recordSummary (env, denv) c2
      in
-         unifyKinds k1 k2;
+         unifyKinds env k1 k2;
          unifySummaries (env, denv) (k1, r1, r2);
          gs1 @ gs2
      end
@@ -848,12 +915,13 @@
                  val (c2, gs2) = hnormCon (env, denv) c2
              in
                  let
+                     (*val () = prefaces "unifyCons'" [("old1", p_con env old1),
+                                                     ("old2", p_con env old2),
+                                                     ("c1", p_con env c1),
+                                                     ("c2", p_con env c2)]*)
+
                      val gs3 = unifyCons'' (env, denv) c1 c2
                  in
-                     (*prefaces "unifyCons'" [("c1", p_con env old1),
-                                            ("c2", p_con env old2),
-                                            ("t", PD.string (LargeReal.toString (Time.toReal
-                                                                                 (Time.- (Time.now (), befor)))))];*)
                      gs1 @ gs2 @ gs3
                  end
                  handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex)
@@ -878,7 +946,7 @@
              if expl1 <> expl2 then
                  err CExplicitness
              else
-                 (unifyKinds d1 d2;
+                 (unifyKinds env d1 d2;
                   let
                       val denv' = D.enter denv
                       (*val befor = Time.now ()*)
@@ -906,7 +974,7 @@
              (unifyCons' (env, denv) d1 d2;
               unifyCons' (env, denv) r1 r2)
            | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
-             (unifyKinds k1 k2;
+             (unifyKinds env k1 k2;
               unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
 
            | (L'.CName n1, L'.CName n2) =>
@@ -954,6 +1022,19 @@
              else
                  err CIncompatible
 
+           | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
+             (unifyKinds env dom1 dom2;
+              unifyKinds env ran1 ran2;
+              [])
+
+           | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) =>
+             unifyCons' (E.pushKRel env x, denv) c1 c2
+           | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) =>
+             (unifyKinds env k1 k2;
+              unifyCons' (env, denv) c1 c2)
+           | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
+             unifyCons' (E.pushKRel env x, denv) c1 c2
+
            | (L'.CError, _) => []
            | (_, L'.CError) => []
 
@@ -966,7 +1047,7 @@
              if r1 = r2 then
                  []
              else
-                 (unifyKinds k1 k2;
+                 (unifyKinds env k1 k2;
                   r1 := SOME c2All;
                   [])
 
@@ -983,11 +1064,6 @@
                  (r := SOME c1All;
                   [])
 
-           | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
-             (unifyKinds dom1 dom2;
-              unifyKinds ran1 ran2;
-              [])
-
            | _ => err CIncompatible
      end
 
@@ -1013,36 +1089,7 @@
          P.Int _ => !int
        | P.Float _ => !float
        | P.String _ => !string
-
- fun recCons (k, nm, v, rest, loc) =
-     (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
-                  rest), loc)
-
- fun foldType (dom, loc) =
-     (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
-                (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
-                                     (L'.TCFun (L'.Explicit, "v", dom,
-                                                (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
-                                                           (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
-                                                                     (L'.CDisjoint (L'.Instantiate,
-                                                                                    (L'.CRecord
-                                                                                         ((L'.KUnit, loc),
-                                                                                          [((L'.CRel 2, loc),
-                                                                                            (L'.CUnit, loc))]), loc),
-                                                                                    (L'.CRel 0, loc),
-                                                                                    (L'.CApp ((L'.CRel 3, loc),
-                                                                                              recCons (dom,
-                                                                                                       (L'.CRel 2, loc),
-                                                                                                       (L'.CRel 1, loc),
-                                                                                                       (L'.CRel 0, loc),
-                                                                                                       loc)), loc)),
-                                                                      loc)), loc)),
-                                                 loc)), loc)), loc),
-                          (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
-                                    (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
-                                               (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
-                           loc)), loc)), loc)
-
+                           
  datatype constraint =
           Disjoint of D.goal
         | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
@@ -1056,7 +1103,16 @@
                  val (t, gs) = hnormCon (env, denv) t
              in
                  case t of
-                     (L'.TCFun (L'.Implicit, x, k, t'), _) =>
+                     (L'.TKFun (x, t'), _) =>
+                     let
+                         val u = kunif loc
+
+                         val t'' = subKindInCon (0, u) t'
+                         val (e, t, gs') = unravel (t'', (L'.EKApp (e, u), loc))
+                     in
+                         (e, t, enD gs @ gs')
+                     end
+                   | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
                      let
                          val u = cunif (loc, k)
 
@@ -1575,7 +1631,7 @@
           | L.ECAbs (expl, x, k, e) =>
             let
                 val expl' = elabExplicitness expl
-                val k' = elabKind k
+                val k' = elabKind env k
 
                 val env' = E.pushCRel env x k'
                 val (e', et, gs) = elabExp (env', D.enter denv) e
@@ -1584,6 +1640,15 @@
                  (L'.TCFun (expl', x, k', et), loc),
                  gs)
             end
+          | L.EKAbs (x, e) =>
+            let
+                val env' = E.pushKRel env x
+                val (e', et, gs) = elabExp (env', denv) e
+            in
+                ((L'.EKAbs (x, e'), loc),
+                 (L'.TKFun (x, et), loc),
+                 gs)
+            end
 
           | L.EDisjoint (c1, c2, e) =>
             let
@@ -1710,13 +1775,6 @@
                  gs1 @ enD gs2 @ enD gs3 @ enD gs4)
             end
 
-          | L.EFold =>
-            let
-                val dom = kunif loc
-            in
-                ((L'.EFold dom, loc), foldType (dom, loc), [])
-            end
-
           | L.ECase (e, pes) =>
             let
                 val (e', et, gs1) = elabExp (env, denv) e
@@ -1781,6 +1839,7 @@
                         case e of
                             L.EAbs _ => true
                           | L.ECAbs (_, _, _, e) => allowable e
+                          | L.EKAbs (_, e) => allowable e
                           | L.EDisjoint (_, _, e) => allowable e
                           | _ => false
 
@@ -1859,7 +1918,7 @@
     case sgi of
         L.SgiConAbs (x, k) =>
         let
-            val k' = elabKind k
+            val k' = elabKind env k
 
             val (env', n) = E.pushCNamed env x k' NONE
         in
@@ -1870,7 +1929,7 @@
         let
             val k' = case ko of
                          NONE => kunif loc
-                       | SOME k => elabKind k
+                       | SOME k => elabKind env k
 
             val (c', ck, gs') = elabCon (env, denv) c
             val (env', n) = E.pushCNamed env x k' (SOME c')
@@ -1979,7 +2038,7 @@
             val (env', n) = E.pushENamed env x c'
             val c' = normClassConstraint env c'
         in
-            (unifyKinds ck ktype
+            (unifyKinds env ck ktype
              handle KUnify ue => strError env (NotType (ck, ue)));
 
             ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
@@ -2027,7 +2086,7 @@
 
       | L.SgiClassAbs (x, k) =>
         let
-            val k = elabKind k
+            val k = elabKind env k
             val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
             val (env, n) = E.pushCNamed env x k' NONE
             val env = E.pushClass env n
@@ -2037,7 +2096,7 @@
 
       | L.SgiClass (x, k, c) =>
         let
-            val k = elabKind k
+            val k = elabKind env k
             val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
             val (c', ck, gs) = elabCon (env, denv) c
             val (env, n) = E.pushCNamed env x k' (SOME c')
@@ -2149,7 +2208,7 @@
               | L'.SgnConst sgis =>
                 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
                                    x' = x andalso
-                                   (unifyKinds k ck
+                                   (unifyKinds env k ck
                                     handle KUnify x => sgnError env (WhereWrongKind x);
                                     true)
                                  | _ => false) sgis then
@@ -2355,7 +2414,7 @@
                                      fun found (x', n1, k1, co1) =
                                          if x = x' then
                                              let
-                                                 val () = unifyKinds k1 k2
+                                                 val () = unifyKinds env k1 k2
                                                      handle KUnify (k1, k2, err) =>
                                                             sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
                                                  val env = E.pushCNamedAs env x n1 k1 co1
@@ -2606,7 +2665,7 @@
                                      fun found (x', n1, k1, co) =
                                          if x = x' then
                                              let
-                                                 val () = unifyKinds k1 k2
+                                                 val () = unifyKinds env k1 k2
                                                      handle KUnify (k1, k2, err) =>
                                                             sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
 
@@ -2635,7 +2694,7 @@
                                      fun found (x', n1, k1, c1) =
                                          if x = x' then
                                              let
-                                                 val () = unifyKinds k1 k2
+                                                 val () = unifyKinds env k1 k2
                                                      handle KUnify (k1, k2, err) =>
                                                             sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
 
@@ -2702,6 +2761,9 @@
               | CAbs _ => false
               | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
 
+              | CKAbs _ => false
+              | TKFun _ => false
+
               | CName _ => true
 
               | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
@@ -2728,6 +2790,9 @@
               | CAbs _ => false
               | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
 
+              | CKAbs _ => false
+              | TKFun _ => false
+
               | CName _ => true
 
               | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
@@ -2777,6 +2842,9 @@
                        | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
                        | L'.KUnif _ => NONE
 
+                       | L'.KRel _ => NONE
+                       | L'.KFun _ => NONE
+
                  fun decompileCon env (c, loc) =
                      case c of
                          L'.CRel i =>
@@ -2914,7 +2982,7 @@
                 let
                     val k' = case ko of
                                  NONE => kunif loc
-                               | SOME k => elabKind k
+                               | SOME k => elabKind env k
 
                     val (c', ck, gs') = elabCon (env, denv) c
                     val (env', n) = E.pushCNamed env x k' (SOME c')
@@ -3047,6 +3115,7 @@
                         case e of
                             L.EAbs _ => true
                           | L.ECAbs (_, _, _, e) => allowable e
+                          | L.EKAbs (_, e) => allowable e
                           | L.EDisjoint (_, _, e) => allowable e
                           | _ => false
 
@@ -3264,7 +3333,7 @@
 
               | L.DClass (x, k, c) =>
                 let
-                    val k = elabKind k
+                    val k = elabKind env k
                     val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
                     val (c', ck, gs') = elabCon (env, denv) c
                     val (env, n) = E.pushCNamed env x k' (SOME c')
diff -r d64533157f40 -r 588b9d16b00a src/expl.sml
--- a/src/expl.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/expl.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -93,7 +93,6 @@
        | EConcat of exp * con * exp * con
        | ECut of exp * con * { field : con, rest : con }
        | ECutMulti of exp * con * { rest : con }
-       | EFold of kind
 
        | ECase of exp * (pat * exp) list * { disc : con, result : con }
 
diff -r d64533157f40 -r 588b9d16b00a src/expl_print.sml
--- a/src/expl_print.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/expl_print.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -351,7 +351,6 @@
                               string "---",
                               space,
                               p_con' true env c])
-      | EFold _ => string "fold"
 
       | EWrite e => box [string "write(",
                          p_exp env e,
diff -r d64533157f40 -r 588b9d16b00a src/expl_util.sml
--- a/src/expl_util.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/expl_util.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -311,10 +311,6 @@
                                  S.map2 (mfc ctx rest,
                                       fn rest' =>
                                          (ECutMulti (e', c', {rest = rest'}), loc))))
-              | EFold k =>
-                S.map2 (mfk k,
-                         fn k' =>
-                            (EFold k', loc))
 
               | EWrite e =>
                 S.map2 (mfe ctx e,
diff -r d64533157f40 -r 588b9d16b00a src/explify.sml
--- a/src/explify.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/explify.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -107,8 +107,6 @@
                                                      {field = explifyCon field, rest = explifyCon rest}), loc)
       | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (explifyExp e1, explifyCon c,
                                                       {rest = explifyCon rest}), loc)
-      | L.EFold k => (L'.EFold (explifyKind k), loc)
-
       | L.ECase (e, pes, {disc, result}) =>
         (L'.ECase (explifyExp e,
                    map (fn (p, e) => (explifyPat p, explifyExp e)) pes,
diff -r d64533157f40 -r 588b9d16b00a src/monoize.sml
--- a/src/monoize.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/monoize.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -2183,7 +2183,6 @@
           | L.EConcat _ => poly ()
           | L.ECut _ => poly ()
           | L.ECutMulti _ => poly ()
-          | L.EFold _ => poly ()
 
           | L.ECase (e, pes, {disc, result}) =>
             let
diff -r d64533157f40 -r 588b9d16b00a src/reduce.sml
--- a/src/reduce.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/reduce.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -214,20 +214,6 @@
                 in
                     case #1 e of
                         ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
-
-                      | EApp ((EApp ((ECApp ((EFold _, _), _), _), f), _), i) =>
-                        (case #1 c of
-                             CRecord (_, []) => i
-                           | CRecord (k, (nm, v) :: rest) =>
-                             let
-                                 val rest = (CRecord (k, rest), loc)
-                             in
-                                 exp (deKnown env)
-                                     (EApp ((ECApp ((ECApp ((ECApp (f, nm), loc), v), loc), rest), loc),
-                                            (ECApp (e, rest), loc)), loc)
-                             end
-                           | _ => (ECApp (e, c), loc))
-
                       | _ => (ECApp (e, c), loc)
                 end
 
@@ -334,8 +320,6 @@
                       | _ => default ()
                 end
 
-              | EFold _ => all
-
               | ECase (e, pes, {disc, result}) =>
                 let
                     fun patBinds (p, _) =
diff -r d64533157f40 -r 588b9d16b00a src/reduce_local.sml
--- a/src/reduce_local.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/reduce_local.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -107,8 +107,6 @@
       | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
       | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
 
-      | EFold _ => all
-
       | ECase (e, pes, others) =>
         let
             fun patBinds (p, _) =
diff -r d64533157f40 -r 588b9d16b00a src/source.sml
--- a/src/source.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/source.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -38,6 +38,9 @@
        | KTuple of kind list
        | KWild
 
+       | KFun of string * kind
+       | KVar of string
+
 withtype kind = kind' located
 
 datatype explicitness =
@@ -56,6 +59,9 @@
        | CAbs of string * kind option * con
        | CDisjoint of con * con * con
 
+       | CKAbs of string * con
+       | TKFun of string * con
+
        | CName of string
 
        | CRecord of (con * con) list
@@ -119,12 +125,13 @@
        | ECAbs of explicitness * string * kind * exp
        | EDisjoint of con * con * exp
 
+       | EKAbs of string * exp
+
        | ERecord of (con * exp) list
        | EField of exp * con
        | EConcat of exp * exp
        | ECut of exp * con
        | ECutMulti of exp * con
-       | EFold
 
        | EWild
 
diff -r d64533157f40 -r 588b9d16b00a src/source_print.sml
--- a/src/source_print.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/source_print.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -50,6 +50,13 @@
                           p_list_sep (box [space, string "*", space]) p_kind ks,
                           string ")"]
 
+      | KVar x => string x
+      | KFun (x, k) => box [string x,
+                            space,
+                            string "-->",
+                            space,
+                            p_kind k]
+
 and p_kind k = p_kind' false k
 
 fun p_explicitness e =
@@ -156,6 +163,17 @@
       | CProj (c, n) => box [p_con c,
                              string ".",
                              string (Int.toString n)]
+
+      | CKAbs (x, c) => box [string x,
+                             space,
+                             string "==>",
+                             space,
+                             p_con c]
+      | TKFun (x, c) => box [string x,
+                             space,
+                             string "-->",
+                             space,
+                             p_con c]
         
 and p_con c = p_con' false c
 
@@ -273,8 +291,6 @@
                                               string "---",
                                               space,
                                               p_con' true c])
-      | EFold => string "fold"
-
       | ECase (e, pes) => parenIf par (box [string "case",
                                             space,
                                             p_exp e,
@@ -300,6 +316,12 @@
                              newline,
                              string "end"]
 
+      | EKAbs (x, e) => box [string x,
+                             space,
+                             string "-->",
+                             space,
+                             p_exp e]
+
 and p_exp e = p_exp' false e
 
 and p_edecl (d, _) =
diff -r d64533157f40 -r 588b9d16b00a src/termination.sml
--- a/src/termination.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/termination.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -190,6 +190,7 @@
                                     in
                                         (p, ps, calls)
                                     end
+                                  | EKApp (e, _) => combiner calls e
                                   | _ =>
                                     let
                                         val (p, calls) = exp parent (penv, calls) e
@@ -239,6 +240,13 @@
                         in
                             (Rabble, calls)
                         end
+                      | EKApp _ => apps ()
+                      | EKAbs (_, e) =>
+                        let
+                            val (_, calls) = exp parent (penv, calls) e
+                        in
+                            (Rabble, calls)
+                        end
 
                       | ERecord xets =>
                         let
@@ -278,7 +286,6 @@
                         in
                             (Rabble, calls)
                         end
-                      | EFold _ => (Rabble, calls)
 
                       | ECase (e, pes, _) =>
                         let
diff -r d64533157f40 -r 588b9d16b00a src/unnest.sml
--- a/src/unnest.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/unnest.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -37,7 +37,7 @@
 structure IS = IntBinarySet
 
 fun liftExpInExp by =
-    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
@@ -51,7 +51,7 @@
                         | (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
@@ -65,7 +65,7 @@
                         | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
                         | (ctx, _) => ctx}
 
-val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
+val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st,
                           con = fn (cb, c, cvs) =>
                                    case c of
                                        CRel n =>
@@ -76,11 +76,11 @@
                                      | _ => cvs,
                           bind = fn (cb, b) =>
                                     case b of
-                                        U.Con.Rel _ => cb + 1
+                                        U.Con.RelC _ => cb + 1
                                       | _ => cb}
                          0 IS.empty
 
-fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st,
+fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st,
                              con = fn ((cb, eb), c, st as (cvs, evs)) =>
                                       case c of
                                           CRel n =>
@@ -124,7 +124,7 @@
     end
 
 fun squishCon cfv =
-    U.Con.mapB {kind = fn k => k,
+    U.Con.mapB {kind = fn _ => fn k => k,
                 con = fn cb => fn c =>
                                   case c of
                                       CRel n =>
@@ -135,12 +135,12 @@
                                     | _ => c,
                 bind = fn (cb, b) =>
                           case b of
-                              U.Con.Rel _ => cb + 1
+                              U.Con.RelC _ => cb + 1
                             | _ => cb}
                0
 
 fun squishExp (nr, cfv, efv) =
-    U.Exp.mapB {kind = fn k => k,
+    U.Exp.mapB {kind = fn _ => fn k => k,
                 con = fn (cb, eb) => fn c =>
                                         case c of
                                             CRel n =>
@@ -169,7 +169,7 @@
      decls : (string * int * con * exp) list
 }
 
-fun kind (k, st) = (k, st)
+fun kind (_, k, st) = (k, st)
 
 fun exp ((ks, ts), e as old, st : state) =
     case e of
diff -r d64533157f40 -r 588b9d16b00a src/urweb.grm
--- a/src/urweb.grm	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/urweb.grm	Sun Feb 22 16:10:25 2009 -0500
@@ -184,10 +184,10 @@
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
  | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
- | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS
+ | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS
  | DATATYPE | OF
  | TYPE | NAME
- | ARROW | LARROW | DARROW | STAR | SEMI
+ | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW
  | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE
  | LET | IN
  | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL
@@ -327,6 +327,8 @@
 
 %name Urweb
 
+%right KARROW
+%nonassoc DKARROW
 %right SEMI
 %nonassoc LARROW
 %nonassoc IF THEN ELSE
@@ -575,6 +577,8 @@
        | KUNIT                          (KUnit, s (KUNITleft, KUNITright))
        | UNDERUNDER                     (KWild, s (UNDERUNDERleft, UNDERUNDERright))
        | LPAREN ktuple RPAREN           (KTuple ktuple, s (LPARENleft, RPARENright))
+       | CSYMBOL                        (KVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+       | CSYMBOL KARROW kind            (KFun (CSYMBOL, kind), s (CSYMBOLleft, kindright))
 
 ktuple : kind STAR kind                 ([kind1, kind2])
        | kind STAR ktuple               (kind :: ktuple)
@@ -585,10 +589,12 @@
 cexp   : capps                          (capps)
        | cexp ARROW cexp                (TFun (cexp1, cexp2), s (cexp1left, cexp2right))
        | SYMBOL kcolon kind ARROW cexp  (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright))
+       | CSYMBOL KARROW cexp            (TKFun (CSYMBOL, cexp), s (CSYMBOLleft, cexpright))
 
        | cexp PLUSPLUS cexp             (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
 
        | FN cargs DARROW cexp           (#1 (cargs (cexp, (KWild, s (FNleft, cexpright)))))
+       | CSYMBOL DKARROW cexp           (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright))
 
        | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
 
@@ -651,7 +657,7 @@
                                                   ((CAbs (SYMBOL, SOME kind, c), loc),
                                                    (KArrow (kind, k), loc))
                                               end)
-       | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) =>
+       | LBRACK cexp TWIDDLE cexp RBRACK  (fn (c, k) =>
                                             let
                                                 val loc = s (LBRACKleft, RBRACKright)
                                             in
@@ -716,6 +722,7 @@
                                          in
                                              #1 (eargs (eexp, (CWild (KType, loc), loc)))
                                          end)
+       | CSYMBOL DKARROW eexp           (EKAbs (CSYMBOL, eexp), s (CSYMBOLleft, eexpright))
        | eexp COLON cexp                (EAnnot (eexp, cexp), s (eexpleft, cexpright))
        | eexp MINUSMINUS cexp           (ECut (eexp, cexp), s (eexpleft, cexpright))
        | eexp MINUSMINUSMINUS cexp      (ECutMulti (eexp, cexp), s (eexpleft, cexpright))
@@ -851,6 +858,13 @@
                                                 ((EDisjoint (cexp1, cexp2, e), loc),
                                                  (CDisjoint (cexp1, cexp2, t), loc))
                                             end)
+       | CSYMBOL                           (fn (e, t) =>
+                                               let
+                                                   val loc = s (CSYMBOLleft, CSYMBOLright)
+                                               in
+                                                   ((EKAbs (CSYMBOL, e), loc),
+                                                    (TKFun (CSYMBOL, t), loc))
+                                               end)
 
 eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
        | LPAREN etuple RPAREN           (let
@@ -895,7 +909,6 @@
                                                        (EField (e, ident), loc))
                                                    (EVar (#1 path, #2 path, DontInfer), s (pathleft, pathright)) idents
                                          end)
-       | FOLD                           (EFold, s (FOLDleft, FOLDright))
 
        | XML_BEGIN xml XML_END          (let
                                              val loc = s (XML_BEGINleft, XML_ENDright)
@@ -1070,7 +1083,7 @@
                                                       ()
                                                   else
                                                       ErrorMsg.errorAt pos "Begin and end tags don't match.";
-                                                  (EFold, pos))
+                                                  (EWild, pos))
                                          end)
        | LBRACE eexp RBRACE             (eexp)
        | LBRACE LBRACK eexp RBRACK RBRACE (let
diff -r d64533157f40 -r 588b9d16b00a src/urweb.lex
--- a/src/urweb.lex	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/urweb.lex	Sun Feb 22 16:10:25 2009 -0500
@@ -247,7 +247,9 @@
 <INITIAL> "}"         => (exitBrace ();
                           Tokens.RBRACE (pos yypos, pos yypos + size yytext));
 
+<INITIAL> "-->"       => (Tokens.KARROW (pos yypos, pos yypos + size yytext));
 <INITIAL> "->"        => (Tokens.ARROW (pos yypos, pos yypos + size yytext));
+<INITIAL> "==>"       => (Tokens.DKARROW (pos yypos, pos yypos + size yytext));
 <INITIAL> "=>"        => (Tokens.DARROW (pos yypos, pos yypos + size yytext));
 <INITIAL> "++"        => (Tokens.PLUSPLUS (pos yypos, pos yypos + size yytext));
 <INITIAL> "--"        => (Tokens.MINUSMINUS (pos yypos, pos yypos + size yytext));
@@ -291,7 +293,6 @@
 <INITIAL> "fun"       => (Tokens.FUN (pos yypos, pos yypos + size yytext));
 <INITIAL> "fn"        => (Tokens.FN (pos yypos, pos yypos + size yytext));
 <INITIAL> "map"       => (Tokens.MAP (pos yypos, pos yypos + size yytext));
-<INITIAL> "fold"      => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
 <INITIAL> "case"      => (Tokens.CASE (pos yypos, pos yypos + size yytext));
 <INITIAL> "if"        => (Tokens.IF (pos yypos, pos yypos + size yytext));
 <INITIAL> "then"      => (Tokens.THEN (pos yypos, pos yypos + size yytext));