Initial conversion to arbitrary-kind classes

9 files changed, 212 insertions, 143 deletions

diff --git a/src/elab.sml b/src/elab.sml
index d997b7ec..8e44c43c 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -136,8 +136,8 @@ datatype sgn_item' =
        | SgiStr of string * int * sgn
        | SgiSgn of string * int * sgn
        | SgiConstraint of con * con
-       | SgiClassAbs of string * int
-       | SgiClass of string * int * con
+       | SgiClassAbs of string * int * kind
+       | SgiClass of string * int * kind * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -163,7 +163,7 @@ datatype decl' =
        | DExport of int * sgn * str
        | DTable of int * string * int * con
        | DSequence of int * string * int
-       | DClass of string * int * con
+       | DClass of string * int * kind * con
        | DDatabase of string
        | DCookie of int * string * int * con
 
diff --git a/src/elab_env.sml b/src/elab_env.sml
index d1084d0c..53c934dd 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -604,8 +604,8 @@ fun sgiSeek (sgi, (sgns, strs, cons)) =
       | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
       | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
       | SgiConstraint _ => (sgns, strs, cons)
-      | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x))
-      | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
+      | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
+      | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
 
 fun sgnSeek f sgis =
     let
@@ -788,8 +788,8 @@ fun enrichClasses env classes (m1, ms) sgn =
                                    fmap,
                                    pushSgnNamedAs env x n sgn)
 
-                                | SgiClassAbs xn => found xn
-                                | SgiClass (x, n, _) => found (x, n)
+                                | SgiClassAbs (x, n, _) => found (x, n)
+                                | SgiClass (x, n, _, _) => found (x, n)
                                 | SgiVal (x, n, (CApp (f, a), _)) =>
                                   let
                                       fun unravel c =
@@ -946,8 +946,8 @@ fun sgiBinds env (sgi, loc) =
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
       | SgiConstraint _ => env
 
-      | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE
-      | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c)
+      | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE
+      | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c)
 
 fun sgnSubCon x =
     ElabUtil.Con.map {kind = id,
@@ -998,14 +998,14 @@ fun projectCon env {sgn, str, field} =
                               end
                           else
                               NONE
-                        | SgiClassAbs (x, _) => if x = field then
-                                                    SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE)
-                                                else
-                                                    NONE
-                        | SgiClass (x, _, c) => if x = field then
-                                                    SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), SOME c)
-                                                else
-                                                    NONE
+                        | SgiClassAbs (x, _, k) => if x = field then
+                                                       SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), NONE)
+                                                   else
+                                                       NONE
+                        | SgiClass (x, _, k, c) => if x = field then
+                                                       SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), SOME c)
+                                                   else
+                                                       NONE
                         | _ => NONE) sgis of
              NONE => NONE
            | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
@@ -1101,8 +1101,8 @@ fun sgnSeekConstraints (str, sgis) =
                   | 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)
-                  | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
-                  | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
     in
         seek (sgis, IM.empty, IM.empty, IM.empty, [])
     end
@@ -1189,9 +1189,9 @@ fun declBinds env (d, loc) =
         in
             pushENamedAs env x n t
         end
-      | DClass (x, n, c) =>
+      | DClass (x, n, k, c) =>
         let
-            val k = (KArrow ((KType, loc), (KType, loc)), loc)
+            val k = (KArrow (k, (KType, loc)), loc)
             val env = pushCNamedAs env x n k (SOME c)
         in
             pushClass env n
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 2f652737..0e6c9767 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -534,16 +534,24 @@ fun p_sgn_item env (sgi, _) =
                                        string "~",
                                        space,
                                        p_con env c2]
-      | SgiClassAbs (x, n) => box [string "class",
-                                   space,
-                                   p_named x n]
-      | SgiClass (x, n, c) => box [string "class",
-                                   space,
-                                   p_named x n,
-                                   space,
-                                   string "=",
-                                   space,
-                                   p_con env c]
+      | SgiClassAbs (x, n, k) => box [string "class",
+                                      space,
+                                      p_named x n,
+                                      space,
+                                      string "::",
+                                      space,
+                                      p_kind k]
+      | SgiClass (x, n, k, c) => box [string "class",
+                                      space,
+                                      p_named x n,
+                                      space,
+                                      string "::",
+                                      space,
+                                      p_kind k,
+                                      space,
+                                      string "=",
+                                      space,
+                                      p_con env c]
 
 and p_sgn env (sgn, _) =
     case sgn of
@@ -705,13 +713,17 @@ fun p_decl env (dAll as (d, _) : decl) =
       | DSequence (_, x, n) => box [string "sequence",
                                     space,
                                     p_named x n]
-      | DClass (x, n, c) => box [string "class",
-                                 space,
-                                 p_named x n,
-                                 space,
-                                 string "=",
-                                 space,
-                                 p_con env c]
+      | DClass (x, n, k, c) => box [string "class",
+                                    space,
+                                    p_named x n,
+                                    space,
+                                    string "::",
+                                    space,
+                                    p_kind k,
+                                    space,
+                                    string "=",
+                                    space,
+                                    p_con env c]
       | DDatabase s => box [string "database",
                             space,
                             string s]
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 6e2c76f6..6e78907d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -547,11 +547,16 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                             S.map2 (con ctx c2,
                                     fn c2' =>
                                        (SgiConstraint (c1', c2'), loc)))
-              | SgiClassAbs _ => S.return2 siAll
-              | SgiClass (x, n, c) =>
-                S.map2 (con ctx c,
-                        fn c' =>
-                           (SgiClass (x, n, c'), loc))
+              | SgiClassAbs (x, n, k) =>
+                S.map2 (kind k,
+                        fn k' =>
+                           (SgiClassAbs (x, n, k'), loc))
+              | SgiClass (x, n, k, c) =>
+                S.bind2 (kind k,
+                      fn k' => 
+                         S.map2 (con ctx c,
+                              fn c' =>
+                                 (SgiClass (x, n, k', c'), loc)))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -575,10 +580,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  | SgiSgn (x, _, sgn) =>
                                                    bind (ctx, Sgn (x, sgn))
                                                  | SgiConstraint _ => ctx
-                                                 | SgiClassAbs (x, n) =>
-                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
-                                                 | SgiClass (x, n, _) =>
-                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
+                                                 | SgiClassAbs (x, n, k) =>
+                                                   bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc)))
+                                                 | SgiClass (x, n, k, _) =>
+                                                   bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))),
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -720,8 +725,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                                                 c), loc)))
                                                  | DSequence (tn, x, n) =>
                                                    bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
-                                                 | DClass (x, n, _) =>
-                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
+                                                 | DClass (x, n, k, _) =>
+                                                   bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc)))
                                                  | DDatabase _ => ctx
                                                  | DCookie (tn, x, n, c) =>
                                                    bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
@@ -819,10 +824,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                            (DTable (tn, x, n, c'), loc))
               | DSequence _ => S.return2 dAll
 
-              | DClass (x, n, c) =>
-                S.map2 (mfc ctx c,
-                     fn c' =>
-                        (DClass (x, n, c'), loc))
+              | DClass (x, n, k, c) =>
+                S.bind2 (mfk k,
+                         fn k' =>
+                            S.map2 (mfc ctx c,
+                                 fn c' =>
+                                    (DClass (x, n, k', c'), loc)))
 
               | DDatabase _ => S.return2 dAll
 
@@ -963,7 +970,7 @@ and maxNameDecl (d, _) =
       | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | DConstraint _ => 0
-      | DClass (_, n, _) => n
+      | DClass (_, n, _, _) => n
       | DExport _ => 0
       | DTable (n1, _, n2, _) => Int.max (n1, n2)
       | DSequence (n1, _, n2) => Int.max (n1, n2)
@@ -1002,8 +1009,8 @@ and maxNameSgi (sgi, _) =
       | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | SgiConstraint _ => 0
-      | SgiClassAbs (_, n) => n
-      | SgiClass (_, n, _) => n
+      | SgiClassAbs (_, n, _) => n
+      | SgiClass (_, n, _, _) => n
               
 end
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d42175ce..05e08c81 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2059,24 +2059,26 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
         end
 
-      | L.SgiClassAbs x =>
+      | L.SgiClassAbs (x, k) =>
         let
-            val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
-            val (env, n) = E.pushCNamed env x k NONE
+            val k = elabKind 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
         in
-            ([(L'.SgiClassAbs (x, n), loc)], (env, denv, []))
+            ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
         end
 
-      | L.SgiClass (x, c) =>
+      | L.SgiClass (x, k, c) =>
         let
-            val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+            val k = elabKind 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')
+            val (env, n) = E.pushCNamed env x k' (SOME c')
             val env = E.pushClass env n
         in
-            checkKind env c' ck k;
-            ([(L'.SgiClass (x, n, c'), loc)], (env, denv, []))
+            checkKind env c' ck k';
+            ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
         end
 
 and elabSgn (env, denv) (sgn, loc) =
@@ -2140,13 +2142,13 @@ and elabSgn (env, denv) (sgn, loc) =
                                        ();
                                    (cons, vals, sgns, SS.add (strs, x)))
                                 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
-                                | L'.SgiClassAbs (x, _) =>
+                                | L'.SgiClassAbs (x, _, _) =>
                                   (if SS.member (cons, x) then
                                        sgnError env (DuplicateCon (loc, x))
                                    else
                                        ();
                                    (SS.add (cons, x), vals, sgns, strs))
-                                | L'.SgiClass (x, _, _) =>
+                                | L'.SgiClass (x, _, _, _) =>
                                   (if SS.member (cons, x) then
                                        sgnError env (DuplicateCon (loc, x))
                                    else
@@ -2222,8 +2224,8 @@ fun selfify env {str, strs, sgn} =
                               (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
                             | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
                               (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
-                            | (L'.SgiClassAbs (x, n), loc) =>
-                              (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc)
+                            | (L'.SgiClassAbs (x, n, k), loc) =>
+                              (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), 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)
@@ -2284,19 +2286,19 @@ fun dopen (env, denv) {str, strs, sgn} =
                                               (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
                                             | L'.SgiConstraint (c1, c2) =>
                                               (L'.DConstraint (c1, c2), loc)
-                                            | L'.SgiClassAbs (x, n) =>
+                                            | L'.SgiClassAbs (x, n, k) =>
                                               let
-                                                  val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                                                  val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
                                                   val c = (L'.CModProj (str, strs, x), loc)
                                               in
-                                                  (L'.DCon (x, n, k, c), loc)
+                                                  (L'.DCon (x, n, k', c), loc)
                                               end
-                                            | L'.SgiClass (x, n, _) =>
+                                            | L'.SgiClass (x, n, k, _) =>
                                               let
-                                                  val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                                                  val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
                                                   val c = (L'.CModProj (str, strs, x), loc)
                                               in
-                                                  (L'.DCon (x, n, k, c), loc)
+                                                  (L'.DCon (x, n, k', c), loc)
                                               end
                                   in
                                       (d, (E.declBinds env' d, denv'))
@@ -2320,7 +2322,7 @@ fun sgiOfDecl (d, loc) =
       | L'.DExport _ => []
       | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)]
       | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
-      | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
+      | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
       | L'.DDatabase _ => []
       | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
 
@@ -2418,14 +2420,14 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          in
                                              found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
                                          end
-                                       | L'.SgiClassAbs (x', n1) => found (x', n1,
-                                                                           (L'.KArrow ((L'.KType, loc),
-                                                                                       (L'.KType, loc)), loc),
-                                                                           NONE)
-                                       | L'.SgiClass (x', n1, c) => found (x', n1,
-                                                                           (L'.KArrow ((L'.KType, loc),
-                                                                                       (L'.KType, loc)), loc),
-                                                                           SOME c)
+                                       | L'.SgiClassAbs (x', n1, k) => found (x', n1,
+                                                                              (L'.KArrow (k,
+                                                                                          (L'.KType, loc)), loc),
+                                                                              NONE)
+                                       | L'.SgiClass (x', n1, k, c) => found (x', n1,
+                                                                              (L'.KArrow (k,
+                                                                                          (L'.KType, loc)), loc),
+                                                                              SOME c)
                                        | _ => NONE
                                  end)
 
@@ -2458,8 +2460,8 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                  in
                                      case sgi1 of
                                          L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
-                                       | L'.SgiClass (x', n1, c1) =>
-                                         found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1)
+                                       | L'.SgiClass (x', n1, k1, c1) =>
+                                         found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1)
                                        | _ => NONE
                                  end)
 
@@ -2632,13 +2634,17 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                          NONE
                                    | _ => NONE)
 
-                      | L'.SgiClassAbs (x, n2) =>
+                      | L'.SgiClassAbs (x, n2, k2) =>
                         seek (fn (env, sgi1All as (sgi1, _)) =>
                                  let
-                                     fun found (x', n1, co) =
+                                     fun found (x', n1, k1, co) =
                                          if x = x' then
                                              let
-                                                 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                                                 val () = unifyKinds k1 k2
+                                                     handle KUnify (k1, k2, err) =>
+                                                            sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+
+                                                 val k = (L'.KArrow (k1, (L'.KType, loc)), loc)
                                                  val env = E.pushCNamedAs env x n1 k co
                                              in
                                                  SOME (if n1 = n2 then
@@ -2651,18 +2657,22 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                              NONE
                                  in
                                      case sgi1 of
-                                         L'.SgiClassAbs (x', n1) => found (x', n1, NONE)
-                                       | L'.SgiClass (x', n1, c) => found (x', n1, SOME c)
+                                         L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
+                                       | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
                                        | _ => NONE
                                  end)
-                      | L'.SgiClass (x, n2, c2) =>
+                      | L'.SgiClass (x, n2, k2, c2) =>
                         seek (fn (env, sgi1All as (sgi1, _)) =>
                                  let
-                                     val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                                     val k = (L'.KArrow (k2, (L'.KType, loc)), loc)
 
-                                     fun found (x', n1, c1) =
+                                     fun found (x', n1, k1, c1) =
                                          if x = x' then
                                              let
+                                                 val () = unifyKinds k1 k2
+                                                     handle KUnify (k1, k2, err) =>
+                                                            sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+
                                                  fun good () =
                                                      let
                                                          val env = E.pushCNamedAs env x n2 k (SOME c2)
@@ -2685,7 +2695,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                              NONE
                                  in
                                      case sgi1 of
-                                         L'.SgiClass (x', n1, c1) => found (x', n1, c1)
+                                         L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
                                        | _ => NONE
                                  end)
                 end
@@ -2878,8 +2888,8 @@ fun wildifyStr env (str, sgn) =
                                                         L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
                                                                              handle NotFound =>
                                                                                     needed)
-                                                      | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV)
-                                                                            handle NotFound => needed)
+                                                      | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
+                                                                               handle NotFound => needed)
                                                       | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
                                                                              handle NotFound => needed)
                                                       | L.DOpen _ => (SM.empty, SS.empty)
@@ -3286,15 +3296,16 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
                     ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
                 end
 
-              | L.DClass (x, c) =>
+              | L.DClass (x, k, c) =>
                 let
-                    val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                    val k = elabKind 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')
+                    val (env, n) = E.pushCNamed env x k' (SOME c')
                     val env = E.pushClass env n
                 in
-                    checkKind env c' ck k;
-                    ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs))
+                    checkKind env c' ck k';
+                    ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
                 end
 
               | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
@@ -3408,29 +3419,25 @@ and elabStr (env, denv) (str, loc) =
                                   ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
                               end
                             | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
-                            | L'.SgiClassAbs (x, n) =>
+                            | L'.SgiClassAbs (x, n, k) =>
                               let
-                                  val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
-
                                   val (cons, x) =
                                       if SS.member (cons, x) then
                                           (cons, "?" ^ x)
                                       else
                                           (SS.add (cons, x), x)
                               in
-                                  ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs)
+                                  ((L'.SgiClassAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
                               end
-                            | L'.SgiClass (x, n, c) =>
+                            | L'.SgiClass (x, n, k, c) =>
                               let
-                                  val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
-
                                   val (cons, x) =
                                       if SS.member (cons, x) then
                                           (cons, "?" ^ x)
                                       else
                                           (SS.add (cons, x), x)
                               in
-                                  ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
+                                  ((L'.SgiClass (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
                               end)
 
                 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
diff --git a/src/explify.sml b/src/explify.sml
index e3c22f20..a10037ef 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -139,9 +139,9 @@ fun explifySgi (sgi, 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)
       | L.SgiConstraint _ => NONE
-      | L.SgiClassAbs (x, n) => SOME (L'.SgiConAbs (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)), loc)
-      | L.SgiClass (x, n, c) => SOME (L'.SgiCon (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc),
-                                                 explifyCon c), loc)
+      | L.SgiClassAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc)), loc)
+      | L.SgiClass (x, n, k, c) => SOME (L'.SgiCon (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc),
+                                                    explifyCon c), loc)
 
 and explifySgn (sgn, loc) =
     case sgn of
@@ -172,8 +172,8 @@ fun explifyDecl (d, loc : EM.span) =
       | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc)
       | L.DTable (nt, x, n, c) => SOME (L'.DTable (nt, x, n, explifyCon c), loc)
       | L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc)
-      | L.DClass (x, n, c) => SOME (L'.DCon (x, n,
-                                             (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), explifyCon c), loc)
+      | L.DClass (x, n, k, c) => SOME (L'.DCon (x, n,
+                                                (L'.KArrow (explifyKind k, (L'.KType, loc)), loc), explifyCon c), loc)
       | L.DDatabase s => SOME (L'.DDatabase s, loc)
       | L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc)
 
diff --git a/src/source.sml b/src/source.sml
index 7685bb2f..a5c86f66 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -81,8 +81,8 @@ datatype sgn_item' =
        | SgiSgn of string * sgn
        | SgiInclude of sgn
        | SgiConstraint of con * con
-       | SgiClassAbs of string
-       | SgiClass of string * con
+       | SgiClassAbs of string * kind
+       | SgiClass of string * kind * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -154,7 +154,7 @@ datatype decl' =
        | DExport of str
        | DTable of string * con
        | DSequence of string
-       | DClass of string * con
+       | DClass of string * kind * con
        | DDatabase of string
        | DCookie of string * con
 
diff --git a/src/source_print.sml b/src/source_print.sml
index 77f2d749..d6568efe 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -413,17 +413,25 @@ fun p_sgn_item (sgi, _) =
                                        string "~",
                                        space,
                                        p_con c2]
-      | SgiClassAbs x => box [string "class",
-                              space,
-                              string x]
-      | SgiClass (x, c) => box [string "class",
-                                space,
-                                string x,
-                                space,
-                                string "=",
-                                space,
-                                p_con c]
-
+      | SgiClassAbs (x, k) => box [string "class",
+                                   space,
+                                   string x,
+                                   space,
+                                   string "::",
+                                   space,
+                                   p_kind k]
+      | SgiClass (x, k, c) => box [string "class",
+                                   space,
+                                   string x,
+                                   space,
+                                   string "::",
+                                   space,
+                                   p_kind k,
+                                   space,
+                                   string "=",
+                                   space,
+                                   p_con c]
+                              
 and p_sgn (sgn, _) =
     case sgn of
         SgnConst sgis => box [string "sig",
@@ -562,13 +570,13 @@ fun p_decl ((d, _) : decl) =
       | DSequence x => box [string "sequence",
                             space,
                             string x]
-      | DClass (x, c) => box [string "class",
-                              space,
-                              string x,
-                              space,
-                              string "=",
-                              space,
-                              p_con c]
+      | DClass (x, k, c) => box [string "class",
+                                 space,
+                                 string x,
+                                 space,
+                                 string "=",
+                                 space,
+                                 p_con c]
 
       | DDatabase s => box [string "database",
                             space,
diff --git a/src/urweb.grm b/src/urweb.grm
index 7798b018..5f2c0575 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -410,13 +410,24 @@ decl   : CON SYMBOL cargl2 kopt EQ cexp (let
        | EXPORT spath                   ([(DExport spath, s (EXPORTleft, spathright))])
        | TABLE SYMBOL COLON cexp        ([(DTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))])
        | SEQUENCE SYMBOL                ([(DSequence SYMBOL, s (SEQUENCEleft, SYMBOLright))])
-       | CLASS SYMBOL EQ cexp           ([(DClass (SYMBOL, cexp), s (CLASSleft, cexpright))])
+       | CLASS SYMBOL EQ cexp           (let
+                                             val loc = s (CLASSleft, cexpright)
+                                         in
+                                             [(DClass (SYMBOL, (KWild, loc), cexp), loc)]
+                                         end)
+       | CLASS SYMBOL DCOLON kind EQ cexp ([(DClass (SYMBOL, kind, cexp), s (CLASSleft, cexpright))])
        | CLASS SYMBOL SYMBOL EQ cexp    (let
                                              val loc = s (CLASSleft, cexpright)
-                                             val k = (KType, loc)
+                                             val k = (KWild, loc)
                                              val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
                                          in
-                                             [(DClass (SYMBOL1, c), s (CLASSleft, cexpright))]
+                                             [(DClass (SYMBOL1, k, c), s (CLASSleft, cexpright))]
+                                         end)
+       | CLASS SYMBOL LPAREN SYMBOL DCOLON kind RPAREN EQ cexp (let
+                                             val loc = s (CLASSleft, cexpright)
+                                             val c = (CAbs (SYMBOL2, SOME kind, cexp), loc)
+                                         in
+                                             [(DClass (SYMBOL1, kind, c), s (CLASSleft, cexpright))]
                                          end)
        | COOKIE SYMBOL COLON cexp       ([(DCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))])
 
@@ -501,14 +512,38 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
                                          in
                                              (SgiVal (SYMBOL, t), loc)
                                          end)
-       | CLASS SYMBOL                   (SgiClassAbs SYMBOL, s (CLASSleft, SYMBOLright))
-       | CLASS SYMBOL EQ cexp           (SgiClass (SYMBOL, cexp), s (CLASSleft, cexpright))
+       | CLASS SYMBOL                   (let
+                                             val loc = s (CLASSleft, SYMBOLright)
+                                         in
+                                             (SgiClassAbs (SYMBOL, (KWild, loc)), loc)
+                                         end)
+       | CLASS SYMBOL DCOLON kind       (let
+                                             val loc = s (CLASSleft, kindright)
+                                         in
+                                             (SgiClassAbs (SYMBOL, kind), loc)
+                                         end)
+       | CLASS SYMBOL EQ cexp           (let
+                                             val loc = s (CLASSleft, cexpright)
+                                         in
+                                             (SgiClass (SYMBOL, (KWild, loc), cexp), loc)
+                                         end)
+       | CLASS SYMBOL DCOLON kind EQ cexp (let
+                                               val loc = s (CLASSleft, cexpright)
+                                           in
+                                               (SgiClass (SYMBOL, kind, cexp), loc)
+                                           end)
        | CLASS SYMBOL SYMBOL EQ cexp    (let
                                              val loc = s (CLASSleft, cexpright)
-                                             val k = (KType, loc)
+                                             val k = (KWild, loc)
                                              val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
                                          in
-                                             (SgiClass (SYMBOL1, c), s (CLASSleft, cexpright))
+                                             (SgiClass (SYMBOL1, k, c), s (CLASSleft, cexpright))
+                                         end)
+       | CLASS SYMBOL LPAREN SYMBOL DCOLON kind RPAREN EQ cexp    (let
+                                             val loc = s (CLASSleft, cexpright)
+                                             val c = (CAbs (SYMBOL2, SOME kind, cexp), loc)
+                                         in
+                                             (SgiClass (SYMBOL1, kind, c), s (CLASSleft, cexpright))
                                          end)
        | COOKIE SYMBOL COLON cexp       (let
                                              val loc = s (COOKIEleft, cexpright)