Parametrized datatypes through explify

18 files changed, 395 insertions, 198 deletions

diff --git a/src/corify.sml b/src/corify.sml
index 7e2f2493..6e49ccd5 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -429,7 +429,7 @@ structure St : sig
          L.PWild => (L'.PWild, loc)
        | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
        | L.PPrim p => (L'.PPrim p, loc)
-       | L.PCon (dk, pc, po) => (L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc)
+       | L.PCon (dk, pc, ts, po) => raise Fail "Corify PCon" (*(L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc)*)
        | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
 
  fun corifyExp st (e, loc) =
@@ -512,8 +512,8 @@ structure St : sig
          in
              ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
          end
-       | L.DDatatype (x, n, xncs) =>
-         let
+       | L.DDatatype (x, n, xs, xncs) => raise Fail "Corify DDatatype"
+         (*let
              val (st, n) = St.bindCon st x n
              val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
                                                     let
@@ -541,9 +541,9 @@ structure St : sig
                                  end) xncs
          in
              ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
-         end
-       | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
-         let
+         end*)
+       | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => raise Fail "Corify DDatatypeImp"
+         (*let
              val (st, n) = St.bindCon st x n
              val c = corifyCon st (L.CModProj (m1, ms, s), loc)
 
@@ -571,7 +571,7 @@ structure St : sig
                                end) xncs
          in
              ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st)
-         end
+         end*)
        | L.DVal (x, n, t, e) =>
          let
              val (st, n) = St.bindVal st x n
@@ -648,8 +648,8 @@ structure St : sig
                                          st)
                                     end
 
-                                  | L.SgiDatatype (x, n, xnts) =>
-                                    let
+                                  | L.SgiDatatype (x, n, xs, xnts) => raise Fail "Corify FFI SgiDatatype"
+                                    (*let
                                         val dk = ExplUtil.classifyDatatype xnts
                                         val (st, n') = St.bindCon st x n
                                         val (xnts, (ds', st, cmap, conmap)) =
@@ -698,7 +698,7 @@ structure St : sig
                                         cmap,
                                         conmap,
                                         st)
-                                   end
+                                   end*)
 
                                  | L.SgiVal (x, _, c) =>
                                    (ds,
@@ -811,8 +811,8 @@ and corifyStr ((str, _), st) =
 fun maxName ds = foldl (fn ((d, _), n) =>
                            case d of
                                L.DCon (_, n', _, _) => Int.max (n, n')
-                             | L.DDatatype (_, n', _) => Int.max (n, n')
-                             | L.DDatatypeImp (_, n', _, _, _, _) => Int.max (n, n')
+                             | L.DDatatype (_, n', _, _) => Int.max (n, n')
+                             | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n')
                              | L.DVal (_, n', _, _) => Int.max (n, n')
                              | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
                              | L.DSgn (_, n', _) => Int.max (n, n')
diff --git a/src/elab.sml b/src/elab.sml
index 2bf64f5a..c04b5d23 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -83,7 +83,7 @@ datatype pat' =
          PWild
        | PVar of string * con
        | PPrim of Prim.t
-       | PCon of datatype_kind * patCon * pat option
+       | PCon of datatype_kind * patCon * con list * pat option
        | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
@@ -112,8 +112,8 @@ withtype exp = exp' located
 datatype sgn_item' =
          SgiConAbs of string * int * kind
        | SgiCon of string * int * kind * con
-       | SgiDatatype of string * int * (string * int * con option) list
-       | SgiDatatypeImp of string * int * int * string list * string * (string * int * con option) list
+       | SgiDatatype of string * int * string list * (string * int * con option) list
+       | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | SgiVal of string * int * con
        | SgiStr of string * int * sgn
        | SgiSgn of string * int * sgn
@@ -132,8 +132,8 @@ and sgn = sgn' located
 
 datatype decl' =
          DCon of string * int * kind * con
-       | DDatatype of string * int * (string * int * con option) list
-       | DDatatypeImp of string * int * int * string list * string * (string * int * con option) list
+       | DDatatype of string * int * string list * (string * int * con option) list
+       | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | DVal of string * int * con * exp
        | DValRec of (string * int * con * exp) list
        | DSgn of string * int * sgn
diff --git a/src/elab_env.sig b/src/elab_env.sig
index f341bed2..6f0febcc 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -51,13 +51,14 @@ signature ELAB_ENV = sig
 
     val lookupC : env -> string -> Elab.kind var
 
-    val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env
+    val pushDatatype : env -> int -> string list -> (string * int * Elab.con option) list -> env
     type datatyp
     val lookupDatatype : env -> int -> datatyp
     val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option
+    val datatypeArgs : datatyp -> string list
     val constructors : datatyp -> (string * int * Elab.con option) list
 
-    val lookupConstructor : env -> string -> (Elab.datatype_kind * int * Elab.con option * int) option
+    val lookupConstructor : env -> string -> (Elab.datatype_kind * int * string list * Elab.con option * int) option
 
     val pushERel : env -> string -> Elab.con -> env
     val lookupERel : env -> int -> string * Elab.con
@@ -87,9 +88,9 @@ signature ELAB_ENV = sig
 
     val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option
     val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
-                          -> (string * int * Elab.con option) list option
+                          -> (string list * (string * int * Elab.con option) list) option
     val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
-                             -> (Elab.datatype_kind * int * Elab.con option * Elab.con) option
+                             -> (Elab.datatype_kind * int * string list * Elab.con option * Elab.con) option
     val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
     val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
     val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 23b29155..eac0c662 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -73,7 +73,7 @@ datatype 'a var =
        | Rel of int * 'a
        | Named of int * 'a
 
-type datatyp = (string * con option) IM.map
+type datatyp = string list * (string * con option) IM.map
 
 type env = {
      renameC : kind var' SM.map,
@@ -81,7 +81,7 @@ type env = {
      namedC : (string * kind * con option) IM.map,
 
      datatypes : datatyp IM.map,
-     constructors : (datatype_kind * int * con option * int) SM.map,
+     constructors : (datatype_kind * int * string list * con option * int) SM.map,
 
      renameE : con var' SM.map,
      relE : (string * con) list,
@@ -188,7 +188,7 @@ fun lookupC (env : env) x =
       | SOME (Rel' x) => Rel x
       | SOME (Named' x) => Named x
 
-fun pushDatatype (env : env) n xncs =
+fun pushDatatype (env : env) n xs xncs =
     let
         val dk = U.classifyDatatype xncs
     in
@@ -197,10 +197,10 @@ fun pushDatatype (env : env) n xncs =
          namedC = #namedC env,
 
          datatypes = IM.insert (#datatypes env, n,
-                                foldl (fn ((x, n, to), cons) =>
-                                          IM.insert (cons, n, (x, to))) IM.empty xncs),
+                                (xs, foldl (fn ((x, n, to), cons) =>
+                                               IM.insert (cons, n, (x, to))) IM.empty xncs)),
          constructors = foldl (fn ((x, n', to), cmap) =>
-                                  SM.insert (cmap, x, (dk, n', to, n)))
+                                  SM.insert (cmap, x, (dk, n', xs, to, n)))
                               (#constructors env) xncs,
 
          renameE = #renameE env,
@@ -219,14 +219,15 @@ fun lookupDatatype (env : env) n =
         NONE => raise UnboundNamed n
       | SOME x => x
 
-fun lookupDatatypeConstructor dt n =
+fun lookupDatatypeConstructor (_, dt) n =
     case IM.find (dt, n) of
         NONE => raise UnboundNamed n
       | SOME x => x
 
 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
 
-fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
+fun datatypeArgs (xs, _) = xs
+fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
 
 fun pushERel (env : env) x t =
     let
@@ -362,20 +363,40 @@ fun sgiBinds env (sgi, loc) =
     case sgi of
         SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
       | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
-      | SgiDatatype (x, n, xncs) =>
+      | SgiDatatype (x, n, xs, xncs) =>
         let
             val env = pushCNamedAs env x n (KType, loc) NONE
         in
-            foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
-                    | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
+                      in
+                          pushENamedAs env x' n' t
+                      end)
             env xncs
         end
-      | SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
+      | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
         let
             val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
         in
-            foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
-                    | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
+                      in
+                          pushENamedAs env x' n' t
+                      end)
             env xncs
         end
       | SgiVal (x, n, t) => pushENamedAs env x n t
@@ -394,8 +415,8 @@ fun sgnSeek f sgis =
                     let
                         val cons =
                             case sgi of
-                                SgiDatatype (x, n, _) => IM.insert (cons, n, x)
-                              | SgiDatatypeImp (x, n, _, _, _, _) => IM.insert (cons, n, x)
+                                SgiDatatype (x, n, _, _) => IM.insert (cons, n, x)
+                              | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
                               | _ => cons
                     in
                         SOME (v, (sgns, strs, cons))
@@ -404,8 +425,8 @@ fun sgnSeek f sgis =
                     case sgi of
                         SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
                       | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
-                      | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
-                      | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
                       | SgiVal _ => seek (sgis, sgns, strs, cons)
                       | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
                       | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
@@ -552,8 +573,8 @@ fun projectCon env {sgn, str, field} =
         SgnConst sgis =>
         (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
                         | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
-                        | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
-                        | SgiDatatypeImp (x, _, m1, ms, x', _) =>
+                        | SgiDatatype (x, _, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
+                        | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
                           if x = field then
                               SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
                           else
@@ -567,30 +588,31 @@ fun projectCon env {sgn, str, field} =
 fun projectDatatype env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
-        (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE
-                        | SgiDatatypeImp (x, _, _, _, _, xncs) => if x = field then SOME xncs else NONE
+        (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
+                        | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
                         | _ => NONE) sgis of
              NONE => NONE
-           | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
+           | SOME ((xs, xncs), subs) => SOME (xs,
+                                              map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
       | _ => NONE
 
 fun projectConstructor env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         let
-            fun consider (n, xncs) =
+            fun consider (n, xs, xncs) =
                 ListUtil.search (fn (x, n', to) =>
                                     if x <> field then
                                         NONE
                                     else
-                                        SOME (U.classifyDatatype xncs, n', to, (CNamed n, #2 str))) xncs
+                                        SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
         in
-            case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs)
-                           | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs)
+            case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs)
+                           | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
                            | _ => NONE) sgis of
                 NONE => NONE
-              | SOME ((dk, n, to, t), subs) => SOME (dk, n, Option.map (sgnSubCon (str, subs)) to,
-                                                     sgnSubCon (str, subs) t)
+              | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to,
+                                                         sgnSubCon (str, subs) t)
         end
       | _ => NONE
 
@@ -598,18 +620,25 @@ fun projectVal env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         let
-            fun seek (n, xncs) =
+            fun seek (n, xs, xncs) =
                 ListUtil.search (fn (x, _, to) =>
                                     if x = field then
-                                        SOME (case to of
-                                                  NONE => (CNamed n, #2 sgn)
-                                                | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
+                                        SOME (let
+                                                  val t =
+                                                      case to of
+                                                          NONE => (CNamed n, #2 sgn)
+                                                        | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn)
+                                                  val k = (KType, #2 sgn)
+                                              in
+                                                  foldr (fn (x, t) => (TCFun (Explicit, x, k, t), #2 sgn))
+                                                  t xs
+                                              end)
                                     else
                                         NONE) xncs
         in
             case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
-                           | SgiDatatype (_, n, xncs) => seek (n, xncs)
-                           | SgiDatatypeImp (_, n, _, _, _, xncs) => seek (n, xncs)
+                           | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs)
+                           | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
                            | _ => NONE) sgis of
                 NONE => NONE
               | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
@@ -632,8 +661,8 @@ fun sgnSeekConstraints (str, sgis) =
                     end
                   | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
-                  | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
-                  | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
                   | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
                   | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
@@ -650,26 +679,44 @@ fun projectConstraints env {sgn, str} =
 fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
-      | DDatatype (x, n, xncs) =>
+      | DDatatype (x, n, xs, xncs) =>
         let
             val env = pushCNamedAs env x n (KType, loc) NONE
-            val env = pushDatatype env n xncs
+            val env = pushDatatype env n xs xncs
         in
-            foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
-                    | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
-            env xncs
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
+                      in
+                          pushENamedAs env x' n' t
+                      end)
+                  env xncs
         end
-      | DDatatypeImp (x, n, m, ms, x', xncs) =>
+      | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
         let
             val t = (CModProj (m, ms, x'), loc)
             val env = pushCNamedAs env x n (KType, loc) (SOME t)
-            val env = pushDatatype env n xncs
+            val env = pushDatatype env n xs xncs
 
             val t = (CNamed n, loc)
         in
-            foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t
-                    | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc))
-            env xncs
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
+                      in
+                          pushENamedAs env x' n' t
+                      end)
+                  env xncs
         end
       | DVal (x, n, t, _) => pushENamedAs env x n t
       | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 122c6c02..ceea43a9 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -216,8 +216,8 @@ fun p_pat' par env (p, _) =
         PWild => string "_"
       | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
-      | PCon (_, pc, NONE) => p_patCon env pc
-      | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc,
+      | PCon (_, pc, _, NONE) => p_patCon env pc
+      | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc,
                                                   space,
                                                   p_pat' true env p])
       | PRecord xps =>
@@ -364,13 +364,16 @@ fun p_named x n =
     else
         string x
 
-fun p_datatype env (x, n, cons) =
+fun p_datatype env (x, n, xs, cons) =
     let
-        val env = E.pushCNamedAs env x n (KType, ErrorMsg.dummySpan) NONE
+        val k = (KType, ErrorMsg.dummySpan)
+        val env = E.pushCNamedAs env x n k NONE
+        val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
     in
         box [string "datatype",
              space,
              string x,
+             p_list_sep (box []) (fn x => box [space, string x]) xs,
              space,
              string "=",
              space,
@@ -401,7 +404,7 @@ fun p_sgn_item env (sgi, _) =
                                     space,
                                     p_con env c]
       | SgiDatatype x => p_datatype env x
-      | SgiDatatypeImp (x, _, m1, ms, x', _) =>
+      | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
                 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
@@ -523,7 +526,7 @@ fun p_decl env (dAll as (d, _) : decl) =
                                   space,
                                   p_con env c]
       | DDatatype x => p_datatype env x
-      | DDatatypeImp (x, _, m1, ms, x', _) =>
+      | DDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
                 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
diff --git a/src/elab_util.sml b/src/elab_util.sml
index d8dd16b8..1c67fbb2 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -396,7 +396,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                         S.map2 (con ctx c,
                              fn c' =>
                                 (SgiCon (x, n, k', c'), loc)))
-              | SgiDatatype (x, n, xncs) =>
+              | SgiDatatype (x, n, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
                                                  NONE => S.return2 (x, n, c)
@@ -404,8 +404,8 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  S.map2 (con ctx c,
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
-                           (SgiDatatype (x, n, xncs'), loc))
-              | SgiDatatypeImp (x, n, m1, ms, s, xncs) =>
+                           (SgiDatatype (x, n, xs, xncs'), loc))
+              | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
                                                  NONE => S.return2 (x, n, c)
@@ -413,7 +413,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  S.map2 (con ctx c,
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
-                           (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc))
+                           (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
               | SgiVal (x, n, c) =>
                 S.map2 (con ctx c,
                      fn c' =>
@@ -445,9 +445,9 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    bind (ctx, NamedC (x, k))
                                                  | SgiCon (x, _, k, _) =>
                                                    bind (ctx, NamedC (x, k))
-                                                 | SgiDatatype (x, n, xncs) =>
+                                                 | SgiDatatype (x, n, _, xncs) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
-                                                 | SgiDatatypeImp (x, _, _, _, _, _) =>
+                                                 | SgiDatatypeImp (x, _, _, _, _, _, _) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
                                                  | SgiVal _ => ctx
                                                  | SgiStr (x, _, sgn) =>
@@ -553,7 +553,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                               (case #1 d of
                                                    DCon (x, _, k, _) =>
                                                    bind (ctx, NamedC (x, k))
-                                                 | DDatatype (x, n, xncs) =>
+                                                 | DDatatype (x, n, xs, xncs) =>
                                                    let
                                                        val ctx = bind (ctx, NamedC (x, (KType, loc)))
                                                    in
@@ -563,12 +563,21 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                                          case co of
                                                                              NONE => CNamed n
                                                                            | SOME t => TFun (t, (CNamed n, loc))
+
+                                                                     val k = (KType, loc)
+                                                                     val t = (t, loc)
+                                                                     val t = foldr (fn (x, t) =>
+                                                                                       (TCFun (Explicit,
+                                                                                               x,
+                                                                                               k,
+                                                                                               t), loc))
+                                                                             t xs
                                                                  in
-                                                                     bind (ctx, NamedE (x, (t, loc)))
+                                                                     bind (ctx, NamedE (x, t))
                                                                  end)
                                                        ctx xncs
                                                    end
-                                                 | DDatatypeImp (x, n, m, ms, x', _) =>
+                                                 | DDatatypeImp (x, n, m, ms, x', _, _) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
                                                  | DVal (x, _, c, _) =>
                                                    bind (ctx, NamedE (x, c))
@@ -616,7 +625,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                             S.map2 (mfc ctx c,
                                     fn c' =>
                                        (DCon (x, n, k', c'), loc)))
-              | DDatatype (x, n, xncs) =>
+              | DDatatype (x, n, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
                                                  NONE => S.return2 (x, n, c)
@@ -624,8 +633,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                  S.map2 (mfc ctx c,
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
-                           (DDatatype (x, n, xncs'), loc))
-              | DDatatypeImp (x, n, m1, ms, s, xncs) =>
+                           (DDatatype (x, n, xs, xncs'), loc))
+              | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
                                                  NONE => S.return2 (x, n, c)
@@ -633,7 +642,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                  S.map2 (mfc ctx c,
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
-                           (DDatatypeImp (x, n, m1, ms, s, xncs'), loc))
+                           (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
               | DVal vi =>
                 S.map2 (mfvi ctx vi,
                      fn vi' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index c999f844..94c51701 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -933,19 +933,32 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
         val pterror = (perror, terror)
         val rerror = (pterror, (env, bound))
 
-        fun pcon (pc, po, to, dn, dk) =
+        fun pcon (pc, po, xs, to, dn, dk) =
             case (po, to) of
                 (NONE, SOME _) => (expError env (PatHasNoArg loc);
                                    rerror)
               | (SOME _, NONE) => (expError env (PatHasArg loc);
                                    rerror)
-              | (NONE, NONE) => (((L'.PCon (dk, pc, NONE), loc), dn),
-                                 (env, bound))
+              | (NONE, NONE) =>
+                let
+                    val k = (L'.KType, loc)
+                    val unifs = map (fn _ => cunif (loc, k)) xs
+                    val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
+                in
+                    (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
+                     (env, bound))
+                end
               | (SOME p, SOME t) =>
                 let
                     val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
+
+                    val k = (L'.KType, loc)
+                    val unifs = map (fn _ => cunif (loc, k)) xs
+                    val t = ListUtil.foldli (fn (i, u, t) => subConInCon (i, u) t) t unifs
+                    val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
                 in
-                    (((L'.PCon (dk, pc, SOME p'), loc), dn),
+                    ignore (checkPatCon (env, denv) p' pt t);
+                    (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
                      (env, bound))
                 end
     in
@@ -969,7 +982,7 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
             (case E.lookupConstructor env x of
                  NONE => (expError env (UnboundConstructor (loc, [], x));
                           rerror)
-               | SOME (dk, n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc), dk))
+               | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk))
           | L.PCon (m1 :: ms, x, po) =>
             (case E.lookupStr env m1 of
                  NONE => (expError env (UnboundStrInExp (loc, m1));
@@ -985,7 +998,7 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
                      case E.projectConstructor env {str = str, sgn = sgn, field = x} of
                          NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
                                   rerror)
-                       | SOME (dk, _, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn, dk)
+                       | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk)
                  end)
 
           | L.PRecord (xps, flex) =>
@@ -1035,7 +1048,7 @@ fun exhaustive (env, denv, t, ps) =
                 in
                     case E.projectConstructor env {str = str, sgn = sgn, field = x} of
                         NONE => raise Fail "exhaustive: Can't project constructor"
-                      | SOME (_, n, _, _) => n
+                      | SOME (_, n, _, _, _) => n
                 end
 
         fun coverage (p, _) =
@@ -1043,8 +1056,8 @@ fun exhaustive (env, denv, t, ps) =
                 L'.PWild => Wild
               | L'.PVar _ => Wild
               | L'.PPrim _ => None
-              | L'.PCon (_, pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
-              | L'.PCon (_, pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
+              | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
+              | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
               | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
                                                     SM.insert (fmap, x, coverage p)) SM.empty xps]
 
@@ -1158,8 +1171,13 @@ fun exhaustive (env, denv, t, ps) =
                                               (total, gs' @ gs)
                                           end)
                               (true, gs) cons
+
+                    fun unapp t =
+                        case t of
+                            L'.CApp ((t, _), _) => unapp t
+                          | _ => t
                 in
-                    case t of
+                    case unapp t of
                         L'.CNamed n =>
                         let
                             val dt = E.lookupDatatype env n
@@ -1173,7 +1191,7 @@ fun exhaustive (env, denv, t, ps) =
                         in
                             case E.projectDatatype env {str = str, sgn = sgn, field = x} of
                                 NONE => raise Fail "isTotal: Can't project datatype"
-                              | SOME cons => dtype cons
+                              | SOME (_, cons) => dtype cons
                         end
                       | L'.CError => (true, gs)
                       | _ => raise Fail "isTotal: Not a datatype"
@@ -1206,7 +1224,11 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                  (expError env (UnboundExp (loc, s));
                   (eerror, cerror, []))
                | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
-               | E.Named (n, t) => ((L'.ENamed n, loc), t, []))
+               | E.Named (n, t) =>
+                 if Char.isUpper (String.sub (s, 0)) then
+                     elabHead (env, denv) (L'.ENamed n, loc) t
+                 else
+                     ((L'.ENamed n, loc), t, []))
           | L.EVar (m1 :: ms, s) =>
             (case E.lookupStr env m1 of
                  NONE => (expError env (UnboundStrInExp (loc, m1));
@@ -1572,11 +1594,13 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
         end
 
-      | L.SgiDatatype (x, xcs) =>
+      | L.SgiDatatype (x, xs, xcs) =>
         let
             val k = (L'.KType, loc)
-            val (env, n) = E.pushCNamed env x k NONE
+            val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+            val (env, n) = E.pushCNamed env x k' NONE
             val t = (L'.CNamed n, loc)
+            val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs
 
             val (xcs, (used, env, gs)) =
                 ListUtil.foldlMap
@@ -1591,6 +1615,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
                                                checkKind env t' tk k;
                                                (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
                                            end
+                        val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
 
                         val (env, n') = E.pushENamed env x t
                     in
@@ -1601,8 +1626,10 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
                         ((x, n', to), (SS.add (used, x), env, gs'))
                     end)
                 (SS.empty, env, []) xcs
+
+            val env = E.pushDatatype env n xs xcs
         in
-            ([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs))
+            ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
         end
 
       | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
@@ -1625,12 +1652,14 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
                      (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
                           NONE => (conError env (UnboundDatatype (loc, s));
                                    ([], (env, denv, gs)))
-                        | SOME xncs =>
+                        | SOME (xs, xncs) =>
                           let
                               val k = (L'.KType, loc)
+                              val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+
                               val t = (L'.CModProj (n, ms, s), loc)
-                              val (env, n') = E.pushCNamed env x k (SOME t)
-                              val env = E.pushDatatype env n' xncs
+                              val (env, n') = E.pushCNamed env x k' (SOME t)
+                              val env = E.pushDatatype env n' xs xncs
 
                               val t = (L'.CNamed n', loc)
                               val env = foldl (fn ((x, n, to), env) =>
@@ -1638,11 +1667,15 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
                                                       val t = case to of
                                                                   NONE => t
                                                                 | SOME t' => (L'.TFun (t', t), loc)
+
+                                                      val t = foldr (fn (x, t) =>
+                                                                        (L'.TCFun (L'.Implicit, x, k, t), loc))
+                                                              t xs
                                                   in
                                                       E.pushENamedAs env x n t
                                                   end) env xncs
                           in
-                              ([(L'.SgiDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs))
+                              ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
                           end)
                    | _ => (strError env (NotDatatype loc);
                            ([], (env, denv, [])))
@@ -1720,7 +1753,7 @@ and elabSgn (env, denv) (sgn, loc) =
                                    else
                                        ();
                                    (SS.add (cons, x), vals, sgns, strs))
-                                | L'.SgiDatatype (x, _, xncs) =>
+                                | L'.SgiDatatype (x, _, _, xncs) =>
                                   let
                                       val vals = foldl (fn ((x, _, _), vals) =>
                                                            (if SS.member (vals, x) then
@@ -1736,7 +1769,7 @@ and elabSgn (env, denv) (sgn, loc) =
                                           ();
                                       (SS.add (cons, x), vals, sgns, strs)
                                   end
-                                | L'.SgiDatatypeImp (x, _, _, _, _, _) =>
+                                | L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
                                   (if SS.member (cons, x) then
                                        sgnError env (DuplicateCon (loc, x))
                                    else
@@ -1828,8 +1861,8 @@ fun selfify env {str, strs, sgn} =
       | L'.SgnConst sgis =>
         (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
                               (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
-                            | (L'.SgiDatatype (x, n, xncs), loc) =>
-                              (L'.SgiDatatypeImp (x, n, str, strs, x, xncs), loc)
+                            | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
+                              (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
                             | (L'.SgiStr (x, n, sgn), loc) =>
                               (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
                             | x => x) sgis), #2 sgn)
@@ -1878,10 +1911,10 @@ fun dopen (env, denv) {str, strs, sgn} =
                                               end
                                             | L'.SgiCon (x, n, k, c) =>
                                               (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
-                                            | L'.SgiDatatype (x, n, xncs) =>
-                                              (L'.DDatatypeImp (x, n, str, strs, x, xncs), loc)
-                                            | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
-                                              (L'.DDatatypeImp (x, n, m1, ms, x', xncs), loc)
+                                            | L'.SgiDatatype (x, n, xs, xncs) =>
+                                              (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
+                                            | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
+                                              (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)
                                             | L'.SgiVal (x, n, t) =>
                                               (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
                                             | L'.SgiStr (x, n, sgn) =>
@@ -1998,9 +2031,20 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                      case sgi1 of
                                          L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
                                        | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
-                                       | L'.SgiDatatype (x', n1, _) => found (x', n1, (L'.KType, loc), NONE)
-                                       | L'.SgiDatatypeImp (x', n1, m1, ms, s, _) =>
-                                         found (x', n1, (L'.KType, loc), SOME (L'.CModProj (m1, ms, s), loc))
+                                       | L'.SgiDatatype (x', n1, xs, _) =>
+                                         let
+                                             val k = (L'.KType, loc)
+                                             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+                                         in
+                                             found (x', n1, k', NONE)
+                                         end
+                                       | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
+                                         let
+                                             val k = (L'.KType, loc)
+                                             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+                                         in
+                                             found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
+                                         end
                                        | _ => NONE
                                  end)
 
@@ -2023,15 +2067,18 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          NONE
                                    | _ => NONE)
 
-                      | L'.SgiDatatype (x, n2, xncs2) =>
+                      | L'.SgiDatatype (x, n2, xs2, xncs2) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  let
-                                     fun found (n1, xncs1) =
+                                     fun found (n1, xs1, xncs1) =
                                          let
                                              fun mismatched ue =
                                                  (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
                                                   SOME (env, denv))
 
+                                             val k = (L'.KType, loc)
+                                             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
+
                                              fun good () =
                                                  let
                                                      val env = E.sgiBinds env sgi2All
@@ -2044,6 +2091,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                      SOME (env, denv)
                                                  end
 
+                                             val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
                                              fun xncBad ((x1, _, t1), (x2, _, t2)) =
                                                  String.compare (x1, x2) <> EQUAL
                                                  orelse case (t1, t2) of
@@ -2052,7 +2100,8 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                             not (List.null (unifyCons (env, denv) t1 t2))
                                                           | _ => true
                                          in
-                                             (if length xncs1 <> length xncs2
+                                             (if xs1 <> xs2
+                                                 orelse length xncs1 <> length xncs2
                                                  orelse ListPair.exists xncBad (xncs1, xncs2) then
                                                   mismatched NONE
                                               else
@@ -2061,33 +2110,34 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          end
                                  in
                                      case sgi1 of
-                                         L'.SgiDatatype (x', n1, xncs1) =>
+                                         L'.SgiDatatype (x', n1, xs, xncs1) =>
                                          if x' = x then
-                                             found (n1, xncs1)
+                                             found (n1, xs, xncs1)
                                          else
                                              NONE
-                                       | L'.SgiDatatypeImp (x', n1, _, _, _, xncs1) =>
+                                       | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
                                          if x' = x then
-                                             found (n1, xncs1)
+                                             found (n1, xs, xncs1)
                                          else
                                              NONE
                                        | _ => NONE
                                  end)
 
-                      | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, _) =>
+                      | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  case sgi1 of
-                                     L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _) =>
+                                     L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
                                      if x = x' then
                                          let
                                              val k = (L'.KType, loc)
+                                             val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
                                              val t1 = (L'.CModProj (m11, ms1, s1), loc)
                                              val t2 = (L'.CModProj (m12, ms2, s2), loc)
 
                                              fun good () =
                                                  let
-                                                     val env = E.pushCNamedAs env x n1 k (SOME t1)
-                                                     val env = E.pushCNamedAs env x n2 k (SOME t2)
+                                                     val env = E.pushCNamedAs env x n1 k' (SOME t1)
+                                                     val env = E.pushCNamedAs env x n2 k' (SOME t2)
                                                  in
                                                      SOME (env, denv)
                                                  end
@@ -2213,11 +2263,17 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
 
             ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
         end
-      | L.DDatatype (x, xcs) =>
+      | L.DDatatype (x, xs, xcs) =>
         let
             val k = (L'.KType, loc)
-            val (env, n) = E.pushCNamed env x k NONE
+            val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+            val (env, n) = E.pushCNamed env x k' NONE
             val t = (L'.CNamed n, loc)
+            val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs
+
+            val (env', denv') = foldl (fn (x, (env', denv')) =>
+                                          (E.pushCRel env' x k,
+                                           D.enter denv')) (env, denv) xs
 
             val (xcs, (used, env, gs)) =
                 ListUtil.foldlMap
@@ -2227,11 +2283,12 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                                            NONE => (NONE, t, gs)
                                          | SOME t' =>
                                            let
-                                               val (t', tk, gs') = elabCon (env, denv) t'
+                                               val (t', tk, gs') = elabCon (env', denv') t'
                                            in
-                                               checkKind env t' tk k;
+                                               checkKind env' t' tk k;
                                                (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
                                            end
+                        val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
 
                         val (env, n') = E.pushENamed env x t
                     in
@@ -2243,9 +2300,9 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                     end)
                 (SS.empty, env, []) xcs
 
-            val env = E.pushDatatype env n xcs
+            val env = E.pushDatatype env n xs xcs
         in
-            ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs))
+            ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
         end
 
       | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
@@ -2268,12 +2325,13 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                      (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
                           NONE => (conError env (UnboundDatatype (loc, s));
                                    ([], (env, denv, gs)))
-                        | SOME xncs =>
+                        | SOME (xs, xncs) =>
                           let
                               val k = (L'.KType, loc)
+                              val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
                               val t = (L'.CModProj (n, ms, s), loc)
-                              val (env, n') = E.pushCNamed env x k (SOME t)
-                              val env = E.pushDatatype env n' xncs
+                              val (env, n') = E.pushCNamed env x k' (SOME t)
+                              val env = E.pushDatatype env n' xs xncs
 
                               val t = (L'.CNamed n', loc)
                               val env = foldl (fn ((x, n, to), env) =>
@@ -2281,11 +2339,15 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
                                                       val t = case to of
                                                                   NONE => t
                                                                 | SOME t' => (L'.TFun (t', t), loc)
+
+                                                      val t = foldr (fn (x, t) =>
+                                                                        (L'.TCFun (L'.Implicit, x, k, t), loc))
+                                                              t xs
                                                   in
                                                       E.pushENamedAs env x n t
                                                   end) env xncs
                           in
-                              ([(L'.DDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs))
+                              ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
                           end)
                    | _ => (strError env (NotDatatype loc);
                            ([], (env, denv, [])))
@@ -2544,7 +2606,7 @@ and elabStr (env, denv) (str, loc) =
                               in
                                   ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
                               end
-                            | L'.SgiDatatype (x, n, xncs) =>
+                            | L'.SgiDatatype (x, n, xs, xncs) =>
                               let
                                   val (cons, x) =
                                       if SS.member (cons, x) then
@@ -2561,9 +2623,9 @@ and elabStr (env, denv) (str, loc) =
                                                   ((x, n, t), SS.add (vals, x)))
                                       vals xncs
                               in
-                                  ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs)
+                                  ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
                               end
-                            | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
+                            | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
                               let
                                   val (cons, x) =
                                       if SS.member (cons, x) then
@@ -2571,7 +2633,7 @@ and elabStr (env, denv) (str, loc) =
                                       else
                                           (SS.add (cons, x), x)
                               in
-                                  ((L'.SgiDatatypeImp (x, n, m1, ms, x', xncs), loc) :: sgis, cons, vals, sgns, strs)
+                                  ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
                               end
                             | L'.SgiVal (x, n, c) =>
                               let
diff --git a/src/expl.sml b/src/expl.sml
index 9fea3f19..4ba835ea 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -69,7 +69,7 @@ datatype pat' =
          PWild
        | PVar of string * con
        | PPrim of Prim.t
-       | PCon of datatype_kind * patCon * pat option
+       | PCon of datatype_kind * patCon * con list * pat option
        | PRecord of (string * pat * con) list
 
 withtype pat = pat' located
@@ -98,8 +98,8 @@ withtype exp = exp' located
 datatype sgn_item' =
          SgiConAbs of string * int * kind
        | SgiCon of string * int * kind * con
-       | SgiDatatype of string * int * (string * int * con option) list
-       | SgiDatatypeImp of string * int * int * string list * string * (string * int * con option) list
+       | SgiDatatype of string * int * string list * (string * int * con option) list
+       | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | SgiVal of string * int * con
        | SgiSgn of string * int * sgn
        | SgiStr of string * int * sgn
@@ -116,8 +116,8 @@ and sgn = sgn' located
 
 datatype decl' =
          DCon of string * int * kind * con
-       | DDatatype of string * int * (string * int * con option) list
-       | DDatatypeImp of string * int * int * string list * string * (string * int * con option) list
+       | DDatatype of string * int * string list * (string * int * con option) list
+       | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
        | DVal of string * int * con * exp
        | DValRec of (string * int * con * exp) list
        | DSgn of string * int * sgn
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 359c92a3..9d715c1b 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -239,24 +239,42 @@ fun lookupStrNamed (env : env) n =
 fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
-      | DDatatype (x, n, xncs) =>
+      | DDatatype (x, n, xs, xncs) =>
         let
             val env = pushCNamed env x n (KType, loc) NONE
         in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
-                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
-            env xncs
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+                      in
+                          pushENamed env x' n' t
+                      end)
+                  env xncs
         end
-      | DDatatypeImp (x, n, m, ms, x', xncs) =>
+      | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
         let
             val t = (CModProj (m, ms, x'), loc)
             val env = pushCNamed env x n (KType, loc) (SOME t)
 
             val t = (CNamed n, loc)
         in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' t
-                    | ((x', n', SOME t'), env) => pushENamed env x' n' (TFun (t', t), loc))
-            env xncs
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+                      in
+                          pushENamed env x' n' t
+                      end)
+                  env xncs
         end
       | DVal (x, n, t, _) => pushENamed env x n t
       | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
@@ -269,21 +287,42 @@ fun sgiBinds env (sgi, loc) =
     case sgi of
         SgiConAbs (x, n, k) => pushCNamed env x n k NONE
       | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
-      | SgiDatatype (x, n, xncs) =>
+      | SgiDatatype (x, n, xs, xncs) =>
         let
             val env = pushCNamed env x n (KType, loc) NONE
         in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
-                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
-            env xncs
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+                      in
+                          pushENamed env x' n' t
+                      end)
+                  env xncs
         end
-      | SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
+      | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
         let
-            val env = pushCNamed env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
+            val t = (CModProj (m1, ms, x'), loc)
+            val env = pushCNamed env x n (KType, loc) (SOME t)
+
+            val t = (CNamed n, loc)
         in
-            foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
-                    | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
-            env xncs
+            foldl (fn ((x', n', to), env) =>
+                      let
+                          val t =
+                              case to of
+                                  NONE => (CNamed n, loc)
+                                | SOME t => (TFun (t, (CNamed n, loc)), loc)
+                          val k = (KType, loc)
+                          val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+                      in
+                          pushENamed env x' n' t
+                      end)
+                  env xncs
         end
       | SgiVal (x, n, t) => pushENamed env x n t
       | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 1056dfe4..60075a70 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -181,10 +181,10 @@ fun p_pat' par env (p, _) =
         PWild => string "_"
       | PVar (s, _) => string s
       | PPrim p => Prim.p_t p
-      | PCon (_, pc, NONE) => p_patCon env pc
-      | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc,
-                                                  space,
-                                                  p_pat' true env p])
+      | PCon (_, pc, _, NONE) => p_patCon env pc
+      | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc,
+                                                     space,
+                                                     p_pat' true env p])
       | PRecord xps =>
         box [string "{",
              p_list_sep (box [string ",", space]) (fn (x, p, _) =>
@@ -329,13 +329,16 @@ fun p_named x n =
     else
         string x
 
-fun p_datatype env (x, n, cons) =
+fun p_datatype env (x, n, xs, cons) =
     let
-        val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE
+        val k = (KType, ErrorMsg.dummySpan)
+        val env = E.pushCNamed env x n k NONE
+        val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
     in
         box [string "datatype",
              space,
              string x,
+             p_list_sep (box []) (fn x => box [space, string x]) xs,
              space,
              string "=",
              space,
@@ -368,7 +371,7 @@ fun p_sgn_item env (sgi, _) =
                                     space,
                                     p_con env c]
       | SgiDatatype x => p_datatype env x
-      | SgiDatatypeImp (x, _, m1, ms, x', _) =>
+      | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
                 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
@@ -482,7 +485,7 @@ fun p_decl env (dAll as (d, _) : decl) =
                                   space,
                                   p_con env c]
       | DDatatype x => p_datatype env x
-      | DDatatypeImp (x, _, m1, ms, x', _) =>
+      | DDatatypeImp (x, _, m1, ms, x', _, _) =>
         let
             val m1x = #1 (E.lookupStrNamed env m1)
                 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 481a96b0..8ec85b19 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -373,7 +373,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                         S.map2 (con ctx c,
                              fn c' =>
                                 (SgiCon (x, n, k', c'), loc)))
-              | SgiDatatype (x, n, xncs) =>
+              | SgiDatatype (x, n, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
                                                  NONE => S.return2 (x, n, c)
@@ -381,8 +381,8 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  S.map2 (con ctx c,
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
-                           (SgiDatatype (x, n, xncs'), loc))
-              | SgiDatatypeImp (x, n, m1, ms, s, xncs) =>
+                           (SgiDatatype (x, n, xs, xncs'), loc))
+              | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
                 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
                                              case c of
                                                  NONE => S.return2 (x, n, c)
@@ -390,7 +390,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  S.map2 (con ctx c,
                                                       fn c' => (x, n, SOME c'))) xncs,
                         fn xncs' =>
-                           (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc))
+                           (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
               | SgiVal (x, n, c) =>
                 S.map2 (con ctx c,
                      fn c' =>
@@ -416,9 +416,9 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                    bind (ctx, NamedC (x, k))
                                                  | SgiCon (x, _, k, _) =>
                                                    bind (ctx, NamedC (x, k))
-                                                 | SgiDatatype (x, n, xncs) =>
+                                                 | SgiDatatype (x, n, _, xncs) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
-                                                 | SgiDatatypeImp (x, _, _, _, _, _) =>
+                                                 | SgiDatatypeImp (x, _, _, _, _, _, _) =>
                                                    bind (ctx, NamedC (x, (KType, loc)))
                                                  | SgiVal _ => ctx
                                                  | SgiStr (x, _, sgn) =>
diff --git a/src/explify.sml b/src/explify.sml
index 847fbc60..9fe24ebe 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -81,7 +81,7 @@ fun explifyPat (p, loc) =
         L.PWild => (L'.PWild, loc)
       | L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc)
       | L.PPrim p => (L'.PPrim p, loc)
-      | L.PCon (dk, pc, po) => (L'.PCon (dk, explifyPatCon pc, Option.map explifyPat po), loc)
+      | L.PCon (dk, pc, cs, po) => (L'.PCon (dk, explifyPatCon pc, map explifyCon cs, Option.map explifyPat po), loc)
       | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc)
 
 fun explifyExp (e, loc) =
@@ -113,11 +113,12 @@ fun explifySgi (sgi, loc) =
     case sgi of
         L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
       | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.SgiDatatype (x, n, xncs) => SOME (L'.SgiDatatype (x, n, map (fn (x, n, co) =>
-                                                                          (x, n, Option.map explifyCon co)) xncs), loc)
-      | L.SgiDatatypeImp (x, n, m1, ms, s, xncs) =>
-        SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) =>
-                                                          (x, n, Option.map explifyCon co)) xncs), loc)
+      | L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
+                                                                map (fn (x, n, co) =>
+                                                                        (x, n, Option.map explifyCon co)) xncs), loc)
+      | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
+        SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>
+                                                              (x, n, Option.map explifyCon co)) xncs), loc)
       | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
       | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
       | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
@@ -135,11 +136,13 @@ and explifySgn (sgn, loc) =
 fun explifyDecl (d, loc : EM.span) =
     case d of
         L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
-      | L.DDatatype (x, n, xncs) => SOME (L'.DDatatype (x, n, map (fn (x, n, co) =>
-                                                                      (x, n, Option.map explifyCon co)) xncs), loc)
-      | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
-        SOME (L'.DDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) =>
-                                                        (x, n, Option.map explifyCon co)) xncs), loc)
+      | L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
+                                                            map (fn (x, n, co) =>
+                                                                    (x, n, Option.map explifyCon co)) xncs), loc)
+      | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
+        SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
+                               map (fn (x, n, co) =>
+                                       (x, n, Option.map explifyCon co)) xncs), loc)
       | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
       | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc)
 
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 3c3b87d5..0e25c217 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -64,6 +64,7 @@ fun uppercaseFirst "" = ""
  | vali of string * con option * exp
  | valis of (string * con option * exp) list
 
+ | dargs of string list
  | barOpt of unit
  | dcons of (string * con option) list
  | dcon of string * con option
@@ -142,9 +143,11 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
-       | DATATYPE SYMBOL EQ barOpt dcons(DDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright))
-       | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path
-                (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+       | DATATYPE SYMBOL dargs EQ barOpt dcons(DDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
+       | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
+                (case dargs of
+                     [] => (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+                   | _ => raise Fail "Arguments specified for imported datatype")
        | VAL vali                       (DVal vali, s (VALleft, valiright))
        | VAL REC valis                  (DValRec valis, s (VALleft, valisright))
 
@@ -169,6 +172,9 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
        | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
        | EXPORT spath                   (DExport spath, s (EXPORTleft, spathright))
 
+dargs  :                                ([])
+       | SYMBOL dargs                   (SYMBOL :: dargs)
+
 barOpt :                                ()
        | BAR                            ()
 
@@ -207,9 +213,11 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
        | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
-       | DATATYPE SYMBOL EQ barOpt dcons(SgiDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright))
-       | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path
-                (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+       | DATATYPE SYMBOL dargs EQ barOpt dcons(SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
+       | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
+                (case dargs of
+                     [] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+                   | _ => raise Fail "Arguments specified for imported datatype")
        | VAL SYMBOL COLON cexp          (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
 
        | STRUCTURE CSYMBOL COLON sgn    (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
diff --git a/src/list_util.sig b/src/list_util.sig
index 7bc4452c..33474b01 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -41,5 +41,6 @@ signature LIST_UTIL = sig
     val search : ('a -> 'b option) -> 'a list -> 'b option
 
     val mapi : (int * 'a -> 'b) -> 'a list -> 'b list
+    val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b
 
 end
diff --git a/src/list_util.sml b/src/list_util.sml
index 976e4708..616efcf0 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -146,4 +146,14 @@ fun mapi f =
         m 0 []
     end
 
+fun foldli f =
+    let
+        fun m i acc ls =
+            case ls of
+                [] => acc
+              | h :: t => m (i + 1) (f (i, h, acc)) t
+    in
+        m 0
+    end
+
 end
diff --git a/src/source.sml b/src/source.sml
index d58feb94..505dd172 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -71,7 +71,7 @@ withtype con = con' located
 datatype sgn_item' =
          SgiConAbs of string * kind
        | SgiCon of string * kind option * con
-       | SgiDatatype of string * (string * con option) list
+       | SgiDatatype of string * string list * (string * con option) list
        | SgiDatatypeImp of string * string list * string
        | SgiVal of string * con
        | SgiStr of string * sgn
@@ -120,7 +120,7 @@ withtype exp = exp' located
 
 datatype decl' =
          DCon of string * kind option * con
-       | DDatatype of string * (string * con option) list
+       | DDatatype of string * string list * (string * con option) list
        | DDatatypeImp of string * string list * string
        | DVal of string * con option * exp
        | DValRec of (string * con option * exp) list
diff --git a/src/source_print.sml b/src/source_print.sml
index 960f3ac5..15bb6015 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -278,10 +278,11 @@ fun p_exp' par (e, _) =
 
 and p_exp e = p_exp' false e
 
-fun p_datatype (x, cons) =
+fun p_datatype (x, xs, cons) =
     box [string "datatype",
          space,
          string x,
+         p_list_sep (box []) (fn x => box [space, string x]) xs,
          space,
          string "=",
          space,
diff --git a/tests/datatypeP.lac b/tests/datatypeP.lac
new file mode 100644
index 00000000..12389322
--- /dev/null
+++ b/tests/datatypeP.lac
@@ -0,0 +1,10 @@
+datatype option a = None | Some of a
+
+val none : option int = None
+val some_1 : option int = Some 1
+
+val f = fn t ::: Type => fn x : option t =>
+        case x of None => None | Some x => Some (Some x)
+
+val none_again = f none
+val some_1_again = f some_1