Made type class system very general; demo compiles

7 files changed, 263 insertions, 373 deletions

diff --git a/src/elab_env.sig b/src/elab_env.sig
index 10d11e3b..4b927a16 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -72,6 +72,7 @@ signature ELAB_ENV = sig
     val pushClass : env -> int -> env
     val isClass : env -> Elab.con -> bool
     val resolveClass : env -> Elab.con -> Elab.exp option
+    val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list
 
     val pushERel : env -> string -> Elab.con -> env
     val lookupERel : env -> int -> string * Elab.con
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 8da78375..1c3eb62e 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -162,6 +162,11 @@ datatype class_name =
          ClNamed of int
        | ClProj of int * string list * string
 
+fun class_name_out cn =
+    case cn of
+        ClNamed n => (CNamed n, ErrorMsg.dummySpan)
+      | ClProj x => (CModProj x, ErrorMsg.dummySpan)
+
 fun cn2s cn =
     case cn of
         ClNamed n => "Named(" ^ Int.toString n ^ ")"
@@ -185,71 +190,10 @@ end
 structure CS = BinarySetFn(CK)
 structure CM = BinaryMapFn(CK)
 
-datatype class_key =
-         CkNamed of int
-       | CkRel of int
-       | CkProj of int * string list * string
-       | CkApp of class_key * class_key
-       | CkOther of con
-
-fun ck2s ck =
-    case ck of
-        CkNamed n => "Named(" ^ Int.toString n ^ ")"
-      | CkRel n => "Rel(" ^ Int.toString n ^ ")"
-      | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
-      | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")"
-      | CkOther _ => "Other"
-
-type class_key_n = class_key * int
-
-fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]"
-
-fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")"
-
-structure KK = struct
-type ord_key = class_key_n
-open Order
-fun compare' x =
-    case x of
-        (CkNamed n1, CkNamed n2) => Int.compare (n1, n2)
-      | (CkNamed _, _) => LESS
-      | (_, CkNamed _) => GREATER
-
-      | (CkRel n1, CkRel n2) => Int.compare (n1, n2)
-      | (CkRel _, _) => LESS
-      | (_, CkRel _) => GREATER
-
-      | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) =>
-        join (Int.compare (m1, m2),
-              fn () => join (joinL String.compare (ms1, ms2),
-                             fn () => String.compare (x1, x2)))
-      | (CkProj _, _) => LESS
-      | (_, CkProj _) => GREATER
-
-      | (CkApp (f1, x1), CkApp (f2, x2)) =>
-        join (compare' (f1, f2),
-              fn () => compare' (x1, x2))
-      | (CkApp _, _) => LESS
-      | (_, CkApp _) => GREATER
-
-      | (CkOther _, CkOther _) => EQUAL
-fun compare ((k1, n1), (k2, n2)) =
-    join (Int.compare (n1, n2),
-       fn () => compare' (k1, k2))
-end
-
-structure KM = BinaryMapFn(KK)
-
-type class = {ground : ((class_name * class_key) list * exp) KM.map,
-              inclusions : exp CM.map}
-val empty_class = {ground = KM.empty,
-                   inclusions = CM.empty}
-
-fun printClasses cs = (print "Classes:\n";
-                       CM.appi (fn (cn, {ground = km, ...} : class) =>
-                                   (print (cn2s cn ^ ":");
-                                    KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km;
-                                    print "\n")) cs)
+type class = {ground : (con * exp) list,
+              rules : (int * con list * con * exp) list}
+val empty_class = {ground = [],
+                   rules = []}
 
 type env = {
      renameK : int SM.map,
@@ -309,16 +253,6 @@ val empty = {
     str = IM.empty
 }
 
-fun liftClassKey' ck =
-    case ck of
-        CkNamed _ => ck
-      | CkRel n => CkRel (n + 1)
-      | CkProj _ => ck
-      | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2)
-      | CkOther c => CkOther (lift c)
-
-fun liftClassKey (ck, n) = (liftClassKey' ck, n)
-
 fun pushKRel (env : env) x =
     let
         val renameK = SM.map (fn n => n+1) (#renameK env)
@@ -334,7 +268,12 @@ fun pushKRel (env : env) x =
          datatypes = #datatypes env,
          constructors = #constructors env,
 
-         classes = #classes env,
+         classes = CM.map (fn cl => {ground = map (fn (c, e) =>
+                                                      (liftKindInCon 0 c,
+                                                       e))
+                                                  (#ground cl),
+                                     rules = #rules cl})
+                          (#classes env),
 
          renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
                             | Named' (n, c) => Named' (n, c)) (#renameE env),
@@ -371,10 +310,11 @@ fun pushCRel (env : env) x k =
          constructors = #constructors env,
 
          classes = CM.map (fn class =>
-                              {ground = KM.foldli (fn (ck, e, km) =>
-                                                      KM.insert (km, liftClassKey ck, e))
-                                                  KM.empty (#ground class),
-                               inclusions = #inclusions class})
+                              {ground = map (fn (c, e) =>
+                                                (liftConInCon 0 c,
+                                                 e))
+                                            (#ground class),
+                               rules = #rules class})
                           (#classes env),
 
          renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
@@ -482,6 +422,23 @@ fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
 fun datatypeArgs (xs, _) = xs
 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
 
+fun listClasses (env : env) =
+    map (fn (cn, {ground, rules}) =>
+            (class_name_out cn,
+             ground
+             @ map (fn (nvs, cs, c, e) =>
+                       let
+                           val loc = #2 c
+                           val c = foldr (fn (c', c) => (TFun (c', c), loc)) c cs
+                           val c = ListUtil.foldli (fn (n, (), c) => (TCFun (Explicit,
+                                                                             "x" ^ Int.toString n,
+                                                                             (KError, loc),
+                                                                             c), loc))
+                                                   c (List.tabulate (nvs, fn _ => ()))
+                       in
+                           (c, e)
+                       end) rules)) (CM.listItemsi (#classes env))
+
 fun pushClass (env : env) n =
     {renameK = #renameK env,
      relK = #relK env,
@@ -520,133 +477,169 @@ fun isClass (env : env) c =
         find (class_name_in c)
     end
 
-fun class_key_in (all as (c, _)) =
-    case c of
-        CRel n => CkRel n
-      | CNamed n => CkNamed n
-      | CModProj x => CkProj x
-      | CUnif (_, _, _, ref (SOME c)) => class_key_in c
-      | CApp (c1, c2) => CkApp (class_key_in c1, class_key_in c2)
-      | _ => CkOther all
-
-fun class_key_out loc =
+fun class_head_in c =
+    case #1 c of
+        CApp (f, _) => class_head_in f
+      | CUnif (_, _, _, ref (SOME c)) => class_head_in c
+      | _ => class_name_in c
+
+exception Unify
+
+fun unifyKinds (k1, k2) =
+    case (#1 k1, #1 k2) of
+        (KType, KType) => ()
+      | (KArrow (d1, r1), KArrow (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
+      | (KName, KName) => ()
+      | (KRecord k1, KRecord k2) => unifyKinds (k1, k2)
+      | (KUnit, KUnit) => ()
+      | (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2)
+                                     handle ListPair.UnequalLengths => raise Unify)
+      | (KUnif (_, _, ref (SOME k1)), _) => unifyKinds (k1, k2)
+      | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2)
+      | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify
+      | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
+      | _ => raise Unify
+
+fun unifyCons rs =
     let
-        fun cko k =
-            case k of
-                CkRel n => (CRel n, loc)
-              | CkNamed n => (CNamed n, loc)
-              | CkProj x => (CModProj x, loc)
-              | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc)
-              | CkOther c => c
+        fun unify d (c1, c2) =
+            case (#1 c1, #1 c2) of
+                (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2)
+              | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2)
+
+              | (c1', CRel n2) =>
+                if n2 < d then
+                    case c1' of
+                        CRel n1 => if n1 = n2 then () else raise Unify
+                      | _ => raise Unify
+                else if n2 - d >= length rs then
+                    case c1' of
+                        CRel n1 => if n1 = n2 - length rs then () else raise Unify
+                      | _ => raise Unify
+                else
+                    let
+                        val r = List.nth (rs, n2 - d)
+                    in
+                        case !r of
+                            NONE => r := SOME c1
+                          | SOME c2 => unify d (c1, c2)
+                    end
+
+              | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2))
+              | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (d + 1) (r1, r2))
+              | (TRecord c1, TRecord c2) => unify d (c1, c2)
+              | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
+                (unify d (a1, a2); unify d (b1, b2); unify d (c1, c2))
+
+              | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
+              | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
+                if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
+              | (CApp (f1, x1), CApp (f2, x2)) => (unify d (f1, f2); unify d (x1, x2))
+              | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (d + 1) (b1, b2))
+
+              | (CKAbs (_, b1), CKAbs (_, b2)) => unify d (b1, b2)
+              | (CKApp (c1, k1), CKApp (c2, k2)) => (unify d (c1, c2); unifyKinds (k1, k2))
+              | (TKFun (_, c1), TKFun (_, c2)) => unify d (c1, c2)
+
+              | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
+
+              | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
+                (unifyKinds (k1, k2);
+                 ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify d (x1, x2); unify d (c1, c2))) (xcs1, xcs2)
+                 handle ListPair.UnequalLengths => raise Unify)
+              | (CConcat (f1, x1), CConcat (f2, x2)) => (unify d (f1, f2); unify d (x1, x2))
+              | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
+
+              | (CUnit, CUnit) => ()
+
+              | (CTuple cs1, CTuple cs2) => (ListPair.appEq (unify d) (cs1, cs2)
+                                             handle ListPair.UnequalLengths => raise Unify)
+              | (CProj (c1, n1), CProj (c2, n2)) => (unify d (c1, c2);
+                                                     if n1 = n2 then () else raise Unify)
+
+              | _ => raise Unify
     in
-        cko
+        unify
     end
 
-fun class_pair_in (c, _) =
-    case c of
-        CApp (f, x) =>
-        (case class_name_in f of
-             SOME f => SOME (f, class_key_in x)
-           | _ => NONE)
-      | CUnif (_, _, _, ref (SOME c)) => class_pair_in c
-      | _ => NONE
-
-fun sub_class_key (n, c) =
+fun tryUnify nRs (c1, c2) =
     let
-        fun csk k =
-            case k of
-                CkRel n' => SOME (if n' = n then
-                                      c
-                                  else
-                                      k)
-              | CkNamed _ => SOME k
-              | CkProj _ => SOME k
-              | CkApp (k1, k2) =>
-                (case (csk k1, csk k2) of
-                     (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
-                   | _ => NONE)
-              | CkOther _ => NONE
+        val rs = List.tabulate (nRs, fn _ => ref NONE)
     in
-        csk
+        (unifyCons rs 0 (c1, c2);
+         SOME (map (fn r => case !r of
+                                NONE => raise Unify
+                              | SOME c => c) rs))
+        handle Unify => NONE
     end
 
-fun resolveClass (env : env) c =
+fun unifySubst (rs : con list) =
+    U.Con.mapB {kind = fn _ => fn k => k,
+                con = fn d => fn c =>
+                                 case c of
+                                     CRel n =>
+                                     if n < d then
+                                         c
+                                     else
+                                         #1 (List.nth (rs, n - d))
+                                   | _ => c,
+                bind = fn (d, U.Con.RelC _) => d + 1
+                        | (d, _) => d}
+               0
+
+fun resolveClass (env : env) =
     let
-        fun doPair (f, x) =
-            case CM.find (#classes env, f) of
-                NONE => NONE
-              | SOME class =>
-                let
-                    val loc = #2 c
-
-                    fun tryIncs () =
+        fun resolve c =
+            let
+                fun doHead f =
+                    case CM.find (#classes env, f) of
+                        NONE => NONE
+                      | SOME class =>
                         let
-                            fun tryIncs fs =
-                                case fs of
+                            val loc = #2 c
+
+                            fun tryRules rules =
+                                case rules of
                                     [] => NONE
-                                  | (f', e') :: fs =>
-                                    case doPair (f', x) of
-                                        NONE => tryIncs fs
-                                      | SOME e =>
+                                  | (nRs, cs, c', e) :: rules' =>
+                                    case tryUnify nRs (c, c') of
+                                        NONE => tryRules rules'
+                                      | SOME rs =>
                                         let
-                                            val e' = (ECApp (e', class_key_out loc x), loc)
-                                            val e' = (EApp (e', e), loc)
+                                            val eos = map (resolve o unifySubst rs) cs
                                         in
-                                            SOME e'
+                                            if List.exists (not o Option.isSome) eos then
+                                                tryRules rules'
+                                            else
+                                                let
+                                                    val es = List.mapPartial (fn x => x) eos
+
+                                                    val e = foldr (fn (c, e) => (ECApp (e, c), loc)) e rs
+                                                    val e = foldl (fn (e', e) => (EApp (e, e'), loc)) e es
+                                                in
+                                                    SOME e
+                                                end
                                         end
-                        in
-                            tryIncs (CM.listItemsi (#inclusions class))
-                        end
 
-                    fun tryRules (k, args) =
-                        let
-                            val len = length args
-
-                            fun tryNext () =
-                                case k of
-                                    CkApp (k1, k2) => tryRules (k1, k2 :: args)
-                                  | _ => tryIncs ()
+                            fun rules () = tryRules (#rules class)
+  
+                            fun tryGrounds ces =
+                                case ces of
+                                    [] => rules ()
+                                  | (c', e) :: ces' =>
+                                    case tryUnify 0 (c, c') of
+                                        NONE => tryGrounds ces'
+                                      | SOME _ => SOME e
                         in
-                            case KM.find (#ground class, (k, length args)) of
-                                SOME (cs, e) =>
-                                let
-                                    val es = map (fn (cn, ck) =>
-                                                     let
-                                                         val ck = ListUtil.foldli (fn (i, arg, ck) =>
-                                                                                      case ck of
-                                                                                          NONE => NONE
-                                                                                        | SOME ck =>
-                                                                                          sub_class_key (len - i - 1,
-                                                                                                         arg)
-                                                                                                        ck)
-                                                                                  (SOME ck) args
-                                                     in
-                                                         case ck of
-                                                             NONE => NONE
-                                                           | SOME ck => doPair (cn, ck)
-                                                     end) cs
-                                in
-                                    if List.exists (not o Option.isSome) es then
-                                        tryNext ()
-                                    else
-                                        let
-                                            val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc))
-                                                          e args
-                                            val e = foldr (fn (pf, e) => (EApp (e, pf), loc))
-                                                          e (List.mapPartial (fn x => x) es)
-                                        in
-                                            SOME e
-                                        end
-                                end
-                              | NONE => tryNext ()
+                            tryGrounds (#ground class)
                         end
-                in
-                    tryRules (x, [])
-                end
+            in
+                case class_head_in c of
+                    SOME f => doHead f
+                  | _ => NONE
+            end
     in
-        case class_pair_in c of
-            SOME p => doPair p
-          | _ => NONE
+        resolve
     end
 
 fun pushERel (env : env) x t =
@@ -655,17 +648,17 @@ fun pushERel (env : env) x t =
                                | x => x) (#renameE env)
 
         val classes = CM.map (fn class =>
-                                 {ground = KM.map (fn (ps, e) => (ps, liftExp e)) (#ground class),
-                                  inclusions = #inclusions class}) (#classes env)
-        val classes = case class_pair_in t of
+                                 {ground = map (fn (c, e) => (c, liftExp e)) (#ground class),
+                                  rules = #rules class}) (#classes env)
+        val classes = case class_head_in t of
                           NONE => classes
-                        | SOME (f, x) =>
+                        | SOME f =>
                           case CM.find (classes, f) of
                               NONE => classes
                             | SOME class =>
                               let
-                                  val class = {ground = KM.insert (#ground class, (x, 0), ([], (ERel 0, #2 t))),
-                                               inclusions = #inclusions class}
+                                  val class = {ground = (t, (ERel 0, #2 t)) :: #ground class,
+                                               rules = #rules class}
                               in
                                   CM.insert (classes, f, class)
                               end
@@ -697,16 +690,6 @@ fun lookupERel (env : env) n =
     (List.nth (#relE env, n))
     handle Subscript => raise UnboundRel n
 
-datatype rule =
-         Normal of int * (class_name * class_key) list * class_key
-       | Inclusion of class_name
-
-fun containsOther k =
-    case k of
-        CkOther _ => true
-      | CkApp (k1, k2) => containsOther k1 orelse containsOther k2
-      | _ => false
-
 fun rule_in c =
     let
         fun quantifiers (c, nvars) =
@@ -717,68 +700,18 @@ fun rule_in c =
                     fun clauses (c, hyps) =
                         case #1 c of
                             TFun (hyp, c) =>
-                            (case class_pair_in hyp of
-                                 SOME (p as (_, CkRel _)) => clauses (c, p :: hyps)
-                               | _ => NONE)
+                            (case class_head_in hyp of
+                                 SOME _ => clauses (c, hyp :: hyps)
+                               | NONE => NONE)
                           | _ =>
-                            case class_pair_in c of
+                            case class_head_in c of
                                 NONE => NONE
-                              | SOME (cn, ck) =>
-                                let
-                                    fun dearg (ck, i) =
-                                        if i >= nvars then
-                                            if containsOther ck
-                                               orelse List.exists (fn (_, k) => containsOther k) hyps then
-                                                NONE
-                                            else
-                                                SOME (cn, Normal (nvars, hyps, ck))
-                                        else case ck of
-                                                 CkApp (ck, CkRel i') =>
-                                                 if i' = i then
-                                                     dearg (ck, i + 1)
-                                                 else
-                                                     NONE
-                                               | _ => NONE
-                                in
-                                    dearg (ck, 0)
-                                end
+                              | SOME f => SOME (f, nvars, rev hyps, c)
                 in
                     clauses (c, [])
                 end
     in
-        case #1 c of
-            TCFun (_, _, _, (TFun ((CApp (f1, (CRel 0, _)), _),
-                                   (CApp (f2, (CRel 0, _)), _)), _)) =>
-            (case (class_name_in f1, class_name_in f2) of
-                 (SOME f1, SOME f2) => SOME (f2, Inclusion f1)
-               | _ => NONE)
-          | _ => quantifiers (c, 0)
-    end
-
-fun inclusion (classes : class CM.map, init, inclusions, f, e : exp) =
-    let
-        fun search (f, fs) =
-            if f = init then
-                NONE
-            else if CS.member (fs, f) then
-                SOME fs
-            else
-                let
-                    val fs = CS.add (fs, f)
-                in
-                    case CM.find (classes, f) of
-                        NONE => SOME fs
-                      | SOME {inclusions = fs', ...} =>
-                        CM.foldli (fn (f', _, fs) =>
-                                      case fs of
-                                          NONE => NONE
-                                        | SOME fs => search (f', fs)) (SOME fs) fs'
-                end
-    in
-        case search (f, CS.empty) of
-            SOME _ => CM.insert (inclusions, f, e)
-          | NONE => (ErrorMsg.errorAt (#2 e) "Type class inclusion would create a cycle";
-                     inclusions)
+        quantifiers (c, 0)
     end
 
 fun pushENamedAs (env : env) x n t =
@@ -786,7 +719,7 @@ fun pushENamedAs (env : env) x n t =
         val classes = #classes env
         val classes = case rule_in t of
                           NONE => classes
-                        | SOME (f, rule) =>
+                        | SOME (f, nvs, cs, c) =>
                           case CM.find (classes, f) of
                               NONE => classes
                             | SOME class =>
@@ -794,13 +727,8 @@ fun pushENamedAs (env : env) x n t =
                                   val e = (ENamed n, #2 t)
 
                                   val class =
-                                      case rule of
-                                          Normal (nvars, hyps, x) =>
-                                          {ground = KM.insert (#ground class, (x, nvars), (hyps, e)),
-                                           inclusions = #inclusions class}
-                                        | Inclusion f' =>
-                                          {ground = #ground class,
-                                           inclusions = inclusion (classes, f, #inclusions class, f', e)}
+                                      {ground = #ground class,
+                                       rules = (nvs, cs, c, e) :: #rules class}
                               in
                                   CM.insert (classes, f, class)
                               end
@@ -985,31 +913,6 @@ fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c =
                                (sgnS_con' arg (#1 c2), #2 c2))
       | _ => c
 
-fun sgnS_class_name (arg as (m1, ms', (sgns, strs, cons))) nm =
-    case nm of
-        ClProj (m1, ms, x) =>
-        (case IM.find (strs, m1) of
-             NONE => nm
-           | SOME m1x => ClProj (m1, ms' @ m1x :: ms, x))
-      | ClNamed n =>
-        (case IM.find (cons, n) of
-             NONE => nm
-           | SOME nx => ClProj (m1, ms', nx))
-
-fun sgnS_class_key (arg as (m1, ms', (sgns, strs, cons))) k =
-    case k of
-        CkProj (m1, ms, x) =>
-        (case IM.find (strs, m1) of
-             NONE => k
-           | SOME m1x => CkProj (m1, ms' @ m1x :: ms, x))
-      | CkNamed n =>
-        (case IM.find (cons, n) of
-             NONE => k
-           | SOME nx => CkProj (m1, ms', nx))
-      | CkApp (k1, k2) => CkApp (sgnS_class_key arg k1,
-                                 sgnS_class_key arg k2)
-      | _ => k
-
 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
     case sgn of
         SgnProj (m1, ms, x) =>
@@ -1120,22 +1023,10 @@ fun enrichClasses env classes (m1, ms) sgn =
                                 | SgiVal (x, n, c) =>
                                   (case rule_in c of
                                        NONE => default ()
-                                     | SOME (cn, rule) =>
+                                     | SOME (cn, nvs, cs, c) =>
                                        let
-                                           val globalizeN = sgnS_class_name (m1, ms, fmap)
-                                           val globalize = sgnS_class_key (m1, ms, fmap)
-
-                                           fun unravel c =
-                                               case c of
-                                                   ClNamed n =>
-                                                   ((case lookupCNamed env n of
-                                                         (_, _, SOME c') =>
-                                                         (case class_name_in c' of
-                                                              NONE => c
-                                                            | SOME k => unravel k)
-                                                       | _ => c)
-                                                    handle UnboundNamed _ => c)
-                                                 | _ => c
+                                           val loc = #2 c
+                                           fun globalize (c, loc) = (sgnS_con' (m1, ms, fmap) c, loc)
 
                                            val nc =
                                                case cn of
@@ -1150,23 +1041,14 @@ fun enrichClasses env classes (m1, ms) sgn =
                                                            NONE => classes
                                                          | SOME class =>
                                                            let
-                                                               val e = (EModProj (m1, ms, x),
-                                                                                     #2 sgn)
+                                                               val e = (EModProj (m1, ms, x), #2 sgn)
 
                                                                val class =
-                                                                   case rule of
-                                                                       Normal (nvars, hyps, a) =>
-                                                                       {ground = 
-                                                                        KM.insert (#ground class, (globalize a, nvars),
-                                                                                   (map (fn (n, k) =>
-                                                                                            (globalizeN n,
-                                                                                             globalize k)) hyps, e)),
-                                                                        inclusions = #inclusions class}
-                                                                     | Inclusion f' =>
-                                                                       {ground = #ground class,
-                                                                        inclusions = inclusion (classes, cn,
-                                                                                                #inclusions class,
-                                                                                                globalizeN f', e)}
+                                                                   {ground = #ground class,
+                                                                    rules = (nvs,
+                                                                             map globalize cs,
+                                                                             globalize c,
+                                                                             e) :: #rules class}
                                                            in
                                                                CM.insert (classes, cn, class)
                                                            end
@@ -1188,19 +1070,11 @@ fun enrichClasses env classes (m1, ms) sgn =
                                                                val e = (EModProj (m1, ms, x), #2 sgn)
 
                                                                val class = 
-                                                                   case rule of
-                                                                       Normal (nvars, hyps, a) =>
-                                                                       {ground =
-                                                                        KM.insert (#ground class, (globalize a, nvars),
-                                                                                   (map (fn (n, k) =>
-                                                                                            (globalizeN n,
-                                                                                             globalize k)) hyps, e)),
-                                                                        inclusions = #inclusions class}
-                                                                     | Inclusion f' =>
-                                                                       {ground = #ground class,
-                                                                        inclusions = inclusion (classes, cn,
-                                                                                                #inclusions class,
-                                                                                                globalizeN f', e)}
+                                                                   {ground = #ground class,
+                                                                    rules = (nvs,
+                                                                             map globalize cs,
+                                                                             globalize c,
+                                                                             e) :: #rules class}
                                                            in
                                                                CM.insert (classes, cn, class)
                                                            end
@@ -1301,8 +1175,8 @@ fun sgiBinds env (sgi, loc) =
       | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
       | SgiConstraint _ => env
 
-      | 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)
+      | SgiClassAbs (x, n, k) => pushCNamedAs env x n k NONE
+      | SgiClass (x, n, k, c) => pushCNamedAs env x n k (SOME c)
 
 fun sgnSubCon x =
     ElabUtil.Con.map {kind = id,
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 4f24e225..172f7d37 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -217,7 +217,17 @@ fun expError env err =
                                               ("Type", p_con env c)]) co)
       | Unresolvable (loc, c) =>
         (ErrorMsg.errorAt loc "Can't resolve type class instance";
-         eprefaces' [("Class constraint", p_con env c)])
+         eprefaces' [("Class constraint", p_con env c),
+                     ("Class database", p_list (fn (c, rules) =>
+                                                   box [P.p_con env c,
+                                                        PD.string ":",
+                                                        space,
+                                                        p_list (fn (c, e) =>
+                                                                   box [p_exp env e,
+                                                                        PD.string ":",
+                                                                        space,
+                                                                        P.p_con env c]) rules])
+                                        (E.listClasses env))])
       | IllegalRec (x, e) =>
         (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
          eprefaces' [("Variable", PD.string x),
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 817f885f..5b4bc46a 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -62,6 +62,10 @@ structure Con : sig
     val map : {kind : Elab.kind' -> Elab.kind',
                con : Elab.con' -> Elab.con'}
               -> Elab.con -> Elab.con
+    val existsB : {kind : 'context * Elab.kind' -> bool,
+                  con : 'context * Elab.con' -> bool,
+                   bind : 'context * binder -> 'context}
+                  -> 'context -> Elab.con -> bool
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool} -> Elab.con -> bool
 
diff --git a/src/elab_util.sml b/src/elab_util.sml
index ff4abbfb..17e67787 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -244,7 +244,22 @@ fun map {kind, con} s =
         S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
       | S.Continue (s, ()) => s
 
-fun exists {kind, con} k =
+fun existsB {kind, con, bind} ctx c =
+    case mapfoldB {kind = fn ctx => fn k => fn () =>
+                                               if kind (ctx, k) then
+                                                   S.Return ()
+                                               else
+                                                   S.Continue (k, ()),
+                   con = fn ctx => fn c => fn () =>
+                                              if con (ctx, c) then
+                                                  S.Return ()
+                                              else
+                                                  S.Continue (c, ()),
+                   bind = bind} ctx c () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+fun exists {kind, con} c =
     case mapfold {kind = fn k => fn () =>
                                     if kind k then
                                         S.Return ()
@@ -254,7 +269,7 @@ fun exists {kind, con} k =
                                     if con c then
                                         S.Return ()
                                     else
-                                        S.Continue (c, ())} k () of
+                                        S.Continue (c, ())} c () of
         S.Return _ => true
       | S.Continue _ => false
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 874f6c82..1323086c 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2021,8 +2021,8 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
         let
             val (c', ck, gs') = elabCon (env, denv) c
 
-            val (env', n) = E.pushENamed env x c'
             val c' = normClassConstraint env c'
+            val (env', n) = E.pushENamed env x c'
         in
             (unifyKinds env ck ktype
              handle KUnify ue => strError env (NotType (loc, ck, ue)));
@@ -2115,8 +2115,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
       | L.SgiClassAbs (x, k) =>
         let
             val k = elabKind env k
-            val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
-            val (env, n) = E.pushCNamed env x k' NONE
+            val (env, n) = E.pushCNamed env x k NONE
             val env = E.pushClass env n
         in
             ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
@@ -2125,12 +2124,11 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
       | L.SgiClass (x, k, c) =>
         let
             val k = elabKind env k
-            val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
             val (c', ck, gs) = elabCon (env, denv) c
-            val (env, n) = E.pushCNamed env x k' (SOME c')
+            val (env, n) = E.pushCNamed env x k (SOME c')
             val env = E.pushClass env n
         in
-            checkKind env c' ck k';
+            checkKind env c' ck k;
             ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
         end
 
@@ -2341,17 +2339,15 @@ and dopen env {str, strs, sgn} =
                                               (L'.DConstraint (c1, c2), loc)
                                             | L'.SgiClassAbs (x, n, k) =>
                                               let
-                                                  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, k, _) =>
                                               let
-                                                  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)
@@ -2466,14 +2462,8 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                                          in
                                              found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
                                          end
-                                       | 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)
+                                       | L'.SgiClassAbs (x', n1, k) => found (x', n1, k, NONE)
+                                       | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c)
                                        | _ => NONE
                                  end)
 
@@ -2505,8 +2495,7 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                                  in
                                      case sgi1 of
                                          L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
-                                       | L'.SgiClass (x', n1, k1, c1) =>
-                                         found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1)
+                                       | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
                                        | _ => NONE
                                  end)
 
@@ -2677,13 +2666,12 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                                                      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
+                                                 val env = E.pushCNamedAs env x n1 k1 co
                                              in
                                                  SOME (if n1 = n2 then
                                                            env
                                                        else
-                                                           E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)))
+                                                           E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2)))
                                              end
                                          else
                                              NONE
@@ -2696,8 +2684,6 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
                       | L'.SgiClass (x, n2, k2, c2) =>
                         seek (fn (env, sgi1All as (sgi1, _)) =>
                                  let
-                                     val k = (L'.KArrow (k2, (L'.KType, loc)), loc)
-
                                      fun found (x', n1, k1, c1) =
                                          if x = x' then
                                              let
@@ -2707,11 +2693,11 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
 
                                                  fun good () =
                                                      let
-                                                         val env = E.pushCNamedAs env x n2 k (SOME c2)
+                                                         val env = E.pushCNamedAs env x n2 k2 (SOME c2)
                                                          val env = if n1 = n2 then
                                                                        env
                                                                    else
-                                                                       E.pushCNamedAs env x n1 k (SOME c1)
+                                                                       E.pushCNamedAs env x n1 k2 (SOME c1)
                                                      in
                                                          SOME env
                                                      end
@@ -3361,12 +3347,11 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
               | L.DClass (x, k, c) =>
                 let
                     val k = elabKind env k
-                    val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
                     val (c', ck, gs') = elabCon (env, denv) c
-                    val (env, n) = E.pushCNamed env x k' (SOME c')
+                    val (env, n) = E.pushCNamed env x k (SOME c')
                     val env = E.pushClass env n
                 in
-                    checkKind env c' ck k';
+                    checkKind env c' ck k;
                     ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
                 end
 
diff --git a/src/urweb.grm b/src/urweb.grm
index fb31bd18..16a77150 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -660,8 +660,9 @@ sgi    : CON SYMBOL DCOLON kind         ((SgiConAbs (SYMBOL, kind), s (CONleft,
                                          end)
        | CLASS SYMBOL                   (let
                                              val loc = s (CLASSleft, SYMBOLright)
+                                             val k = (KArrow ((KType, loc), (KType, loc)), loc)
                                          in
-                                             (SgiClassAbs (SYMBOL, (KWild, loc)), loc)
+                                             (SgiClassAbs (SYMBOL, k), loc)
                                          end)
        | CLASS SYMBOL DCOLON kind       (let
                                              val loc = s (CLASSleft, kindright)