Initial type class support

13 files changed, 588 insertions, 163 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 9beff0c9..ec8a811d 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -124,6 +124,8 @@ datatype sgn_item' =
        | SgiSgn of string * int * sgn
        | SgiConstraint of con * con
        | SgiTable of int * string * int * con
+       | SgiClassAbs of string * int
+       | SgiClass of string * int * con
 
 and sgn' =
     SgnConst of sgn_item list
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 6f0febcc..32ba7906 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -60,6 +60,9 @@ signature ELAB_ENV = sig
 
     val lookupConstructor : env -> string -> (Elab.datatype_kind * int * string list * Elab.con option * int) option
 
+    val pushClass : env -> int -> env
+    val resolveClass : env -> Elab.con -> Elab.exp option
+
     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 acd918ec..47868e3c 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -31,6 +31,7 @@ open Elab
 
 structure U = ElabUtil
 
+structure IS = IntBinarySet
 structure IM = IntBinaryMap
 structure SM = BinaryMapFn(struct
                            type ord_key = string
@@ -61,6 +62,22 @@ val liftConInCon =
 
 val lift = liftConInCon 0
 
+val liftExpInExp =
+    U.Exp.mapB {kind = fn k => k,
+                con = fn _ => fn c => c,
+                exp = fn bound => fn e =>
+                                     case e of
+                                         ERel xn =>
+                                         if xn < bound then
+                                             e
+                                         else
+                                             ERel (xn + 1)
+                                       | _ => e,
+                bind = fn (bound, U.Exp.RelE _) => bound + 1
+                        | (bound, _) => bound}
+
+
+val liftExp = liftExpInExp 0
 
 (* Back to environments *)
 
@@ -75,6 +92,61 @@ datatype 'a var =
 
 type datatyp = string list * (string * con option) IM.map
 
+datatype class_name =
+         ClNamed of int
+       | ClProj of int * string list * string
+
+structure CK = struct
+type ord_key = class_name
+open Order
+fun compare x =
+    case x of
+        (ClNamed n1, ClNamed n2) => Int.compare (n1, n2)
+      | (ClNamed _, _) => LESS
+      | (_, ClNamed _) => GREATER
+
+      | (ClProj (m1, ms1, x1), ClProj (m2, ms2, x2)) =>
+        join (Int.compare (m1, m2),
+              fn () => join (joinL String.compare (ms1, ms2),
+                             fn () => String.compare (x1, x2)))
+end
+
+structure CM = BinaryMapFn(CK)
+
+datatype class_key =
+         CkNamed of int
+       | CkRel of int
+       | CkProj of int * string list * string
+
+structure KK = struct
+type ord_key = class_key
+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)))
+end
+
+structure KM = BinaryMapFn(KK)
+
+type class = {
+     ground : exp KM.map
+}
+
+val empty_class = {
+    ground = KM.empty
+}
+
 type env = {
      renameC : kind var' SM.map,
      relC : (string * kind) list,
@@ -83,6 +155,8 @@ type env = {
      datatypes : datatyp IM.map,
      constructors : (datatype_kind * int * string list * con option * int) SM.map,
 
+     classes : class CM.map,
+
      renameE : con var' SM.map,
      relE : (string * con) list,
      namedE : (string * con) IM.map,
@@ -112,6 +186,8 @@ val empty = {
     datatypes = IM.empty,
     constructors = SM.empty,
 
+    classes = CM.empty,
+
     renameE = SM.empty,
     relE = [],
     namedE = IM.empty,
@@ -123,6 +199,12 @@ val empty = {
     str = IM.empty
 }
 
+fun liftClassKey ck =
+    case ck of
+        CkNamed _ => ck
+      | CkRel n => CkRel (n + 1)
+      | CkProj _ => ck
+
 fun pushCRel (env : env) x k =
     let
         val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
@@ -135,6 +217,13 @@ fun pushCRel (env : env) x k =
          datatypes = #datatypes env,
          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)
+                          })
+                          (#classes env),
+
          renameE = #renameE env,
          relE = map (fn (x, c) => (x, lift c)) (#relE env),
          namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
@@ -159,6 +248,8 @@ fun pushCNamedAs (env : env) x n k co =
      datatypes = #datatypes env,
      constructors = #constructors env,
 
+     classes = #classes env,
+
      renameE = #renameE env,
      relE = #relE env,
      namedE = #namedE env,
@@ -203,6 +294,8 @@ fun pushDatatype (env : env) n xs xncs =
                                   SM.insert (cmap, x, (dk, n', xs, to, n)))
                               (#constructors env) xncs,
 
+         classes = #classes env,
+
          renameE = #renameE env,
          relE = #relE env,
          namedE = #namedE env,
@@ -229,10 +322,77 @@ 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 pushClass (env : env) n =
+    {renameC = #renameC env,
+     relC = #relC env,
+     namedC = #namedC env,
+
+     datatypes = #datatypes env,
+     constructors = #constructors env,
+
+     classes = CM.insert (#classes env, ClNamed n, {ground = KM.empty}),
+
+     renameE = #renameE env,
+     relE = #relE env,
+     namedE = #namedE env,
+
+     renameSgn = #renameSgn env,
+     sgn = #sgn env,
+
+     renameStr = #renameStr env,
+     str = #str env}    
+
+fun class_name_in (c, _) =
+    case c of
+        CNamed n => SOME (ClNamed n)
+      | CModProj x => SOME (ClProj x)
+      | _ => NONE
+
+fun class_key_in (c, _) =
+    case c of
+        CRel n => SOME (CkRel n)
+      | CNamed n => SOME (CkNamed n)
+      | CModProj x => SOME (CkProj x)
+      | _ => NONE
+
+fun class_pair_in (c, _) =
+    case c of
+        CApp (f, x) =>
+        (case (class_name_in f, class_key_in x) of
+             (SOME f, SOME x) => SOME (f, x)
+           | _ => NONE)
+      | _ => NONE
+
+fun resolveClass (env : env) c =
+    case class_pair_in c of
+        SOME (f, x) =>
+        (case CM.find (#classes env, f) of
+             NONE => NONE
+           | SOME class =>
+             case KM.find (#ground class, x) of
+                 NONE => NONE
+               | SOME e => SOME e)
+      | _ => NONE
+
 fun pushERel (env : env) x t =
     let
         val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
                                | x => x) (#renameE env)
+
+        val classes = CM.map (fn class => {
+                                 ground = KM.map liftExp (#ground class)
+                             }) (#classes env)
+        val classes = case class_pair_in t of
+                          NONE => classes
+                        | SOME (f, x) =>
+                          let
+                              val class = Option.getOpt (CM.find (classes, f), empty_class)
+                              val class = {
+                                  ground = KM.insert (#ground class, x, (ERel 0, #2 t))
+                              }
+                          in
+                              CM.insert (classes, f, class)
+                          end
     in
         {renameC = #renameC env,
          relC = #relC env,
@@ -241,6 +401,8 @@ fun pushERel (env : env) x t =
          datatypes = #datatypes env,
          constructors = #constructors env,
 
+         classes = classes,
+
          renameE = SM.insert (renameE, x, Rel' (0, t)),
          relE = (x, t) :: #relE env,
          namedE = #namedE env,
@@ -257,22 +419,39 @@ fun lookupERel (env : env) n =
     handle Subscript => raise UnboundRel n
 
 fun pushENamedAs (env : env) x n t =
-    {renameC = #renameC env,
-     relC = #relC env,
-     namedC = #namedC env,
+    let
+        val classes = #classes env
+        val classes = case class_pair_in t of
+                          NONE => classes
+                        | SOME (f, x) =>
+                          let
+                              val class = Option.getOpt (CM.find (classes, f), empty_class)
+                              val class = {
+                                  ground = KM.insert (#ground class, x, (ENamed n, #2 t))
+                              }
+                          in
+                              CM.insert (classes, f, class)
+                          end
+    in
+        {renameC = #renameC env,
+         relC = #relC env,
+         namedC = #namedC env,
 
-     datatypes = #datatypes env,
-     constructors = #constructors env,
+         datatypes = #datatypes env,
+         constructors = #constructors env,
 
-     renameE = SM.insert (#renameE env, x, Named' (n, t)),
-     relE = #relE env,
-     namedE = IM.insert (#namedE env, n, (x, t)),
+         classes = classes,
 
-     renameSgn = #renameSgn env,
-     sgn = #sgn env,
-     
-     renameStr = #renameStr env,
-     str = #str env}
+         renameE = SM.insert (#renameE env, x, Named' (n, t)),
+         relE = #relE env,
+         namedE = IM.insert (#namedE env, n, (x, t)),
+
+         renameSgn = #renameSgn env,
+         sgn = #sgn env,
+         
+         renameStr = #renameStr env,
+         str = #str env}
+    end
 
 fun pushENamed env x t =
     let
@@ -301,6 +480,8 @@ fun pushSgnNamedAs (env : env) x n sgis =
      datatypes = #datatypes env,
      constructors = #constructors env,
 
+     classes = #classes env,
+
      renameE = #renameE env,
      relE = #relE env,
      namedE = #namedE env,
@@ -326,32 +507,6 @@ fun lookupSgnNamed (env : env) n =
 
 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
 
-fun pushStrNamedAs (env : env) x n sgis =
-    {renameC = #renameC env,
-     relC = #relC env,
-     namedC = #namedC env,
-
-     datatypes = #datatypes env,
-     constructors = #constructors env,
-
-     renameE = #renameE env,
-     relE = #relE env,
-     namedE = #namedE env,
-
-     renameSgn = #renameSgn env,
-     sgn = #sgn env,
-
-     renameStr = SM.insert (#renameStr env, x, (n, sgis)),
-     str = IM.insert (#str env, n, (x, sgis))}
-
-fun pushStrNamed env x sgis =
-    let
-        val n = !namedCounter
-    in
-        namedCounter := n + 1;
-        (pushStrNamedAs env x n sgis, n)
-    end
-
 fun lookupStrNamed (env : env) n =
     case IM.find (#str env, n) of
         NONE => raise UnboundNamed n
@@ -359,57 +514,6 @@ fun lookupStrNamed (env : env) n =
 
 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
 
-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, xs, xncs) =>
-        let
-            val env = pushCNamedAs env x n (KType, loc) NONE
-        in
-            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', xs, xncs) =>
-        let
-            val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
-        in
-            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
-      | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
-      | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
-      | SgiConstraint _ => env
-
-      | SgiTable (tn, x, n, c) =>
-        let
-            val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
-        in
-            pushENamedAs env x n t
-        end
 
 fun sgnSeek f sgis =
     let
@@ -439,6 +543,8 @@ fun sgnSeek f sgis =
                       | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
                       | SgiConstraint _ => seek (sgis, sgns, strs, cons)
                       | SgiTable _ => seek (sgis, sgns, strs, cons)
+                      | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+                      | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
     in
         seek (sgis, IM.empty, IM.empty, IM.empty)
     end
@@ -500,17 +606,24 @@ fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
              end)
       | _ => sgn
 
-fun sgnSubCon x =
-    ElabUtil.Con.map {kind = id,
-                      con = sgnS_con x}
-
 fun sgnSubSgn x =
     ElabUtil.Sgn.map {kind = id,
                       con = sgnS_con x,
                       sgn_item = id,
                       sgn = sgnS_sgn x}
 
-fun hnormSgn env (all as (sgn, loc)) =
+
+
+and projectSgn env {sgn, str, field} =
+    case #1 (hnormSgn env sgn) of
+        SgnConst sgis =>
+        (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
+             NONE => NONE
+           | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
+      | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
+      | _ => NONE
+
+and hnormSgn env (all as (sgn, loc)) =
     case sgn of
         SgnError => all
       | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
@@ -547,14 +660,117 @@ fun hnormSgn env (all as (sgn, loc)) =
             end
           | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
 
-and projectSgn env {sgn, str, field} =
+fun enrichClasses env classes (m1, ms) sgn =
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
-        (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
-             NONE => NONE
-           | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
-      | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
-      | _ => NONE
+        let
+            val (classes, _) =
+                foldl (fn (sgi, (classes, newClasses)) =>
+                          let
+                              fun found (x, n) =
+                                  (CM.insert (classes,
+                                              ClProj (m1, ms, x),
+                                              empty_class),
+                                   IS.add (newClasses, n))
+                          in
+                              case #1 sgi of
+                                  SgiClassAbs xn => found xn
+                                | SgiClass (x, n, _) => found (x, n)
+                                | _ => (classes, newClasses)
+                          end)
+                (classes, IS.empty) sgis
+        in
+            classes
+        end
+      | _ => classes
+
+fun pushStrNamedAs (env : env) x n sgn =
+    {renameC = #renameC env,
+     relC = #relC env,
+     namedC = #namedC env,
+
+     datatypes = #datatypes env,
+     constructors = #constructors env,
+
+     classes = enrichClasses env (#classes env) (n, []) sgn,
+
+     renameE = #renameE env,
+     relE = #relE env,
+     namedE = #namedE env,
+
+     renameSgn = #renameSgn env,
+     sgn = #sgn env,
+
+     renameStr = SM.insert (#renameStr env, x, (n, sgn)),
+     str = IM.insert (#str env, n, (x, sgn))}
+
+fun pushStrNamed env x sgn =
+    let
+        val n = !namedCounter
+    in
+        namedCounter := n + 1;
+        (pushStrNamedAs env x n sgn, n)
+    end
+
+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, xs, xncs) =>
+        let
+            val env = pushCNamedAs env x n (KType, loc) NONE
+        in
+            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', xs, xncs) =>
+        let
+            val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
+        in
+            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
+      | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
+      | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
+      | SgiConstraint _ => env
+
+      | SgiTable (tn, x, n, c) =>
+        let
+            val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
+        in
+            pushENamedAs env x n t
+        end
+
+      | 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)
+        
+
+fun sgnSubCon x =
+    ElabUtil.Con.map {kind = id,
+                      con = sgnS_con x}
 
 fun projectStr env {sgn, str, field} =
     case #1 (hnormSgn env sgn) of
@@ -675,6 +891,8 @@ fun sgnSeekConstraints (str, sgis) =
                   | 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)
                   | SgiTable _ => seek (sgis, sgns, strs, 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)
     in
         seek (sgis, IM.empty, IM.empty, IM.empty, [])
     end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index b67ff7eb..73b91b67 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -464,6 +464,16 @@ fun p_sgn_item env (sgi, _) =
                                       string ":",
                                       space,
                                       p_con env c]
+      | 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]
 
 and p_sgn env (sgn, _) =
     case sgn of
diff --git a/src/elab_util.sig b/src/elab_util.sig
index e33e956b..57883073 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -75,6 +75,11 @@ structure Exp : sig
                    con : (Elab.con', 'state, 'abort) Search.mapfolder,
                    exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
                   -> (Elab.exp, 'state, 'abort) Search.mapfolder
+    val mapB : {kind : Elab.kind' -> Elab.kind',
+                con : 'context -> Elab.con' -> Elab.con',
+                exp : 'context -> Elab.exp' -> Elab.exp',
+                bind : 'context * binder -> 'context}
+               -> 'context -> (Elab.exp -> Elab.exp)
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool,
                   exp : Elab.exp' -> bool} -> Elab.exp -> bool
diff --git a/src/elab_util.sml b/src/elab_util.sml
index b0bca7bf..c3ed2d19 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -376,6 +376,14 @@ fun exists {kind, con, exp} k =
         S.Return _ => true
       | S.Continue _ => false
 
+fun mapB {kind, con, exp, bind} ctx e =
+    case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+                   con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
+                   exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+                   bind = bind} ctx e () of
+        S.Continue (e, ()) => e
+      | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
+
 end
 
 structure Sgn = struct
@@ -455,6 +463,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                 S.map2 (con ctx c,
                         fn c' =>
                            (SgiTable (tn, x, n, c'), loc))
+              | SgiClassAbs _ => S.return2 siAll
+              | SgiClass (x, n, c) =>
+                S.map2 (con ctx c,
+                        fn c' =>
+                           (SgiClass (x, n, c'), loc))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -478,7 +491,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
                                                  | SgiSgn (x, _, sgn) =>
                                                    bind (ctx, Sgn (x, sgn))
                                                  | SgiConstraint _ => ctx
-                                                 | SgiTable _ => ctx,
+                                                 | SgiTable _ => ctx
+                                                 | SgiClassAbs (x, _) =>
+                                                   bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc)))
+                                                 | SgiClass (x, _, _) =>
+                                                   bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))),
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a03904d0..e4369dd4 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -985,7 +985,8 @@ datatype exp_error =
      | PatHasNoArg of ErrorMsg.span
      | Inexhaustive of ErrorMsg.span
      | DuplicatePatField of ErrorMsg.span * string
-     | SqlInfer of ErrorMsg.span * L'.con
+     | Unresolvable of ErrorMsg.span * L'.con
+     | OutOfContext of ErrorMsg.span
 
 fun expError env err =
     case err of
@@ -1028,9 +1029,11 @@ fun expError env err =
         ErrorMsg.errorAt loc "Inexhaustive 'case'"
       | DuplicatePatField (loc, s) =>
         ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
-      | SqlInfer (loc, c) =>
-        (ErrorMsg.errorAt loc "Can't infer SQL-ness of type";
-         eprefaces' [("Type", p_con env c)])
+      | OutOfContext loc =>
+        ErrorMsg.errorAt loc "Type class wildcard occurs out of context"
+      | Unresolvable (loc, c) =>
+        (ErrorMsg.errorAt loc "Can't resolve type class instance";
+         eprefaces' [("Class constraint", p_con env c)])
          
 fun checkCon (env, denv) e c1 c2 =
     unifyCons (env, denv) c1 c2
@@ -1419,50 +1422,23 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                      ((L'.EModProj (n, ms, s), loc), t, [])
                  end)
 
-          | L.EApp (e1, (L.ESqlInfer, _)) =>
+          | L.EApp (e1, (L.EWild, _)) =>
             let
                 val (e1', t1, gs1) = elabExp (env, denv) e1
                 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
                 val (t1, gs3) = hnormCon (env, denv) t1
             in
                 case t1 of
-                    (L'.TFun ((L'.CApp ((L'.CModProj (basis, [], "sql_type"), _),
-                                        t), _), ran), _) =>
-                    if basis <> !basis_r then
-                        raise Fail "Bad use of ESqlInfer [1]"
-                    else
-                        let
-                            val (t, gs4) = hnormCon (env, denv) t
-
-                            fun error () = expError env (SqlInfer (loc, t))
-                        in
-                            case t of
-                                (L'.CModProj (basis, [], x), _) =>
-                                (if basis <> !basis_r then
-                                     error ()
-                                 else
-                                     case x of
-                                         "bool" => ()
-                                       | "int" => ()
-                                       | "float" => ()
-                                       | "string" => ()
-                                       | _ => error ();
-                                 ((L'.EApp (e1', (L'.EModProj (basis, [], "sql_" ^ x), loc)), loc),
-                                  ran, gs1 @ gs2 @ gs3 @ gs4))
-                              | (L'.CUnif (_, (L'.KType, _), _, r), _) =>
-                                let
-                                    val t = (L'.CModProj (basis, [], "int"), loc)
-                                in
-                                    r := SOME t;
-                                    ((L'.EApp (e1', (L'.EModProj (basis, [], "sql_int"), loc)), loc),
-                                     ran, gs1 @ gs2 @ gs3 @ gs4)
-                                end
-                              | _ => (error ();
-                                      (eerror, cerror, []))
-                        end
-                  | _ => raise Fail "Bad use of ESqlInfer [2]"
+                    (L'.TFun (dom, ran), _) =>
+                    (case E.resolveClass env dom of
+                         NONE => (expError env (Unresolvable (loc, dom));
+                                  (eerror, cerror, []))
+                       | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3))
+                  | _ => (expError env (OutOfContext loc);
+                          (eerror, cerror, []))
             end
-          | L.ESqlInfer => raise Fail "Bad use of ESqlInfer [3]"
+          | L.EWild => (expError env (OutOfContext loc);
+                        (eerror, cerror, []))
 
           | L.EApp (e1, e2) =>
             let
@@ -1961,6 +1937,26 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
         end
 
+      | L.SgiClassAbs x =>
+        let
+            val k = (L'.KArrow ((L'.KType, loc), (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, []))
+        end
+
+      | L.SgiClass (x, c) =>
+        let
+            val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+            val (c', ck, gs) = elabCon (env, denv) 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, []))
+        end
+
 and elabSgn (env, denv) (sgn, loc) =
     case sgn of
         L.SgnConst sgis =>
@@ -2027,7 +2023,19 @@ and elabSgn (env, denv) (sgn, loc) =
                                        sgnError env (DuplicateVal (loc, x))
                                    else
                                        ();
-                                   (cons, SS.add (vals, x), sgns, strs)))
+                                   (cons, SS.add (vals, x), sgns, strs))
+                                | 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, _, _) =>
+                                  (if SS.member (cons, x) then
+                                       sgnError env (DuplicateCon (loc, x))
+                                   else
+                                       ();
+                                   (SS.add (cons, x), vals, sgns, strs)))
                     (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
         in
             ((L'.SgnConst sgis', loc), gs)
@@ -2160,6 +2168,20 @@ fun dopen (env, denv) {str, strs, sgn} =
                                             | L'.SgiTable (_, x, n, c) =>
                                               (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
                                                         (L'.EModProj (str, strs, x), loc)), loc)
+                                            | L'.SgiClassAbs (x, n) =>
+                                              let
+                                                  val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                                                  val c = (L'.CModProj (str, strs, x), loc)
+                                              in
+                                                  (L'.DCon (x, n, k, c), loc)
+                                              end
+                                            | L'.SgiClass (x, n, _) =>
+                                              let
+                                                  val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                                                  val c = (L'.CModProj (str, strs, x), loc)
+                                              in
+                                                  (L'.DCon (x, n, k, c), loc)
+                                              end
                                   in
                                       (d, (E.declBinds env' d, denv'))
                                   end)
@@ -2283,27 +2305,41 @@ 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)
                                        | _ => NONE
                                  end)
 
                       | L'.SgiCon (x, n2, k2, c2) =>
                         seek (fn sgi1All as (sgi1, _) =>
-                                 case sgi1 of
-                                     L'.SgiCon (x', n1, k1, c1) =>
-                                     if x = x' then
-                                         let
-                                             fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
-                                         in
-                                             (case unifyCons (env, denv) c1 c2 of
-                                                  [] => good ()
-                                                | _ => NONE)
-                                             handle CUnify (c1, c2, err) =>
-                                                    (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
-                                                     good ())
-                                         end
-                                     else
-                                         NONE
-                                   | _ => NONE)
+                                 let
+                                     fun found (x', n1, k1, c1) =
+                                         if x = x' then
+                                             let
+                                                 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
+                                             in
+                                                 (case unifyCons (env, denv) c1 c2 of
+                                                      [] => good ()
+                                                    | _ => NONE)
+                                                 handle CUnify (c1, c2, err) =>
+                                                        (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                         good ())
+                                             end
+                                         else
+                                             NONE
+                                 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)
+                                       | _ => NONE
+                                 end)
 
                       | L'.SgiDatatype (x, n2, xs2, xncs2) =>
                         seek (fn sgi1All as (sgi1, _) =>
@@ -2491,6 +2527,54 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                      else
                                          NONE
                                    | _ => NONE)
+
+                      | L'.SgiClassAbs (x, n2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 let
+                                     fun found (x', n1, co) =
+                                         if x = x' then
+                                             let
+                                                 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+                                                 val env = E.pushCNamedAs env x n1 k co
+                                             in
+                                                 SOME (if n1 = n2 then
+                                                           env
+                                                       else
+                                                           E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)),
+                                                       denv)
+                                             end
+                                         else
+                                             NONE
+                                 in
+                                     case sgi1 of
+                                         L'.SgiClassAbs (x', n1) => found (x', n1, NONE)
+                                       | L'.SgiClass (x', n1, c) => found (x', n1, SOME c)
+                                       | _ => NONE
+                                 end)
+                      | L'.SgiClass (x, n2, c2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 let
+                                     val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+
+                                     fun found (x', n1, c1) =
+                                         if x = x' then
+                                             let
+                                                 fun good () = SOME (E.pushCNamedAs env x n2 k (SOME c2), denv)
+                                             in
+                                                 (case unifyCons (env, denv) c1 c2 of
+                                                      [] => good ()
+                                                    | _ => NONE)
+                                                 handle CUnify (c1, c2, err) =>
+                                                        (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                         good ())
+                                             end
+                                         else
+                                             NONE
+                                 in
+                                     case sgi1 of
+                                         L'.SgiClass (x', n1, c1) => found (x', n1, c1)
+                                       | _ => NONE
+                                 end)
                 end
         in
             ignore (foldl folder (env, denv) sgis2)
@@ -2849,6 +2933,17 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
             ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, gs' @ gs))
         end
 
+      | L.DClass (x, c) =>
+        let
+            val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
+            val (c', ck, gs) = elabCon (env, denv) c
+            val (env, n) = E.pushCNamed env x k (SOME c')
+            val env = E.pushClass env n
+        in
+            checkKind env c' ck k;
+            ([(L'.DCon (x, n, k, c'), loc)], (env, denv, []))
+        end
+
 and elabStr (env, denv) (str, loc) =
     case str of
         L.StrConst ds =>
@@ -2949,6 +3044,30 @@ and elabStr (env, denv) (str, loc) =
                                           (SS.add (vals, x), x)
                               in
                                   ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
+                              end
+                            | L'.SgiClassAbs (x, n) =>
+                              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)
+                              end
+                            | L'.SgiClass (x, n, 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)
                               end)
 
                 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
diff --git a/src/explify.sml b/src/explify.sml
index da338147..50a1851b 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -128,6 +128,9 @@ fun explifySgi (sgi, loc) =
       | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
       | L.SgiConstraint _ => NONE
       | L.SgiTable _ => raise Fail "Explify SgiTable"
+      | 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)
 
 and explifySgn (sgn, loc) =
     case sgn of
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 464f5f82..fd24ba31 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -89,7 +89,7 @@ fun sql_inject (v, t, loc) =
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
  | DIVIDE | GT | DOTDOTDOT
- | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT
+ | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT | CLASS
  | DATATYPE | OF
  | TYPE | NAME
  | ARROW | LARROW | DARROW | STAR
@@ -241,6 +241,14 @@ 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))
        | TABLE SYMBOL COLON cexp        (DTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))
+       | CLASS SYMBOL EQ cexp           (DClass (SYMBOL, cexp), s (CLASSleft, cexpright))
+       | CLASS SYMBOL SYMBOL EQ cexp    (let
+                                             val loc = s (CLASSleft, cexpright)
+                                             val k = (KType, loc)
+                                             val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
+                                         in
+                                             (DClass (SYMBOL1, c), s (CLASSleft, cexpright))
+                                         end)
 
 dargs  :                                ([])
        | SYMBOL dargs                   (SYMBOL :: dargs)
@@ -299,6 +307,15 @@ sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, k
        | INCLUDE sgn                    (SgiInclude sgn, s (INCLUDEleft, sgnright))
        | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
        | TABLE SYMBOL COLON cexp        (SgiTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))
+       | CLASS SYMBOL                   (SgiClassAbs SYMBOL, s (CLASSleft, SYMBOLright))
+       | CLASS SYMBOL EQ cexp           (SgiClass (SYMBOL, cexp), s (CLASSleft, cexpright))
+       | CLASS SYMBOL SYMBOL EQ cexp    (let
+                                             val loc = s (CLASSleft, cexpright)
+                                             val k = (KType, loc)
+                                             val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
+                                         in
+                                             (SgiClass (SYMBOL1, c), s (CLASSleft, cexpright))
+                                         end)
 
 sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)
@@ -459,6 +476,7 @@ eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
                                                (EPrim (Prim.String ""), s (XML_BEGINleft, XML_ENDright))),
                                          s (XML_BEGINleft, XML_ENDright))
        | LPAREN query RPAREN            (query)
+       | UNDER                          (EWild, s (UNDERleft, UNDERright))
 
 idents : ident                          ([ident])
        | ident DOT idents               (ident :: idents)
@@ -633,7 +651,7 @@ sqlexp : TRUE                           (sql_inject (EVar (["Basis"], "True"),
                                                      s (FALSEleft, FALSEright)))
 
        | LBRACE eexp RBRACE             (sql_inject (#1 eexp,
-                                                     ESqlInfer,
+                                                     EWild,
                                                      s (LBRACEleft, RBRACEright)))
 
 wopt   :                                (sql_inject (EVar (["Basis"], "True"),
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 9e994b27..3d745bf2 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -280,6 +280,7 @@ notags = [^<{\n]+;
 <INITIAL> "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext));
 <INITIAL> "export"    => (Tokens.EXPORT (pos yypos, pos yypos + size yytext));
 <INITIAL> "table"     => (Tokens.TABLE (pos yypos, pos yypos + size yytext));
+<INITIAL> "class"     => (Tokens.CLASS (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "Type"      => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
 <INITIAL> "Name"      => (Tokens.NAME (pos yypos, pos yypos + size yytext));
diff --git a/src/source.sml b/src/source.sml
index 70851c73..f8a12a93 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -83,6 +83,8 @@ datatype sgn_item' =
        | SgiInclude of sgn
        | SgiConstraint of con * con
        | SgiTable of string * con
+       | SgiClassAbs of string
+       | SgiClass of string * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -119,7 +121,7 @@ datatype exp' =
        | ECut of exp * con
        | EFold
 
-       | ESqlInfer
+       | EWild
 
        | ECase of exp * (pat * exp) list
 
@@ -139,6 +141,7 @@ datatype decl' =
        | DOpenConstraints of string * string list
        | DExport of str
        | DTable of string * con
+       | DClass of string * con
 
      and str' =
          StrConst of decl list
diff --git a/src/source_print.sml b/src/source_print.sml
index ceb331f0..6aaeb402 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -379,6 +379,16 @@ fun p_sgn_item (sgi, _) =
                                 string ":",
                                 space,
                                 p_con c]
+      | SgiClassAbs x => box [string "class",
+                              space,
+                              string x]
+      | SgiClass (x, c) => box [string "class",
+                                space,
+                                string x,
+                                space,
+                                string "=",
+                                space,
+                                p_con c]
 
 and p_sgn (sgn, _) =
     case sgn of
@@ -531,6 +541,13 @@ fun p_decl ((d, _) : decl) =
                               string ":",
                               space,
                               p_con c]
+      | DClass (x, c) => box [string "class",
+                              space,
+                              string x,
+                              space,
+                              string "=",
+                              space,
+                              p_con c]
 
 and p_str (str, _) =
     case str of
diff --git a/tests/type_class.lac b/tests/type_class.lac
new file mode 100644
index 00000000..72baa3b3
--- /dev/null
+++ b/tests/type_class.lac
@@ -0,0 +1,9 @@
+class default t = t
+
+val string_default : default string = ""
+val int_default : default int = 0
+
+val default : t :: Type -> default t -> t =
+        fn t :: Type => fn d : default t => d
+val empty = default [string] _
+val zero = default [int] _