Remove 'class' declaration; now use 'con' instead

11 files changed, 26 insertions, 97 deletions

diff --git a/doc/manual.tex b/doc/manual.tex
index c7a6491b..0b8f1c06 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -21,7 +21,7 @@
 
 \section{Introduction}
 
-\emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell.  Ur is functional, pure, statically-typed, and strict.  Ur supports a powerful kind of \emph{metaprogramming} based on \emph{type-level computation with type-level records}.
+\emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell.  Ur is functional, pure, statically typed, and strict.  Ur supports a powerful kind of \emph{metaprogramming} based on \emph{type-level computation with type-level records}.
 
 \emph{Ur/Web} is Ur plus a special standard library and associated rules for parsing and optimization.  Ur/Web supports construction of dynamic web applications backed by SQL databases.  The signature of the standard library is such that well-typed Ur/Web programs ``don't go wrong'' in a very broad sense.  Not only do they not crash during particular page generations, but they also may not:
 
@@ -155,7 +155,7 @@ Here is the complete list of directive forms.  ``FFI'' stands for ``foreign func
   \item \texttt{deltas}: maximum number of messages sendable in a single request handler with \texttt{Basis.send}
   \item \texttt{globals}: maximum number of global variables that FFI libraries may set in a single request context
   \item \texttt{headers}: maximum size (in bytes) of per-request buffer used to hold HTTP headers for generated pages
-  \item \texttt{heap}: maximum size (in bytes) of per-request heap for dynamically-allocated data
+  \item \texttt{heap}: maximum size (in bytes) of per-request heap for dynamically allocated data
   \item \texttt{inputs}: maximum number of top-level form fields per request
   \item \texttt{messages}: maximum size (in bytes) of per-request buffer used to hold a single outgoing message sent with \texttt{Basis.send}
   \item \texttt{page}: maximum size (in bytes) of per-request buffer used to hold HTML content of generated pages
@@ -522,7 +522,7 @@ $$\begin{array}{rrcll}
   &&& (e) & \textrm{explicit precedence} \\
   \\
   \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
-  &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
+  &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually recursive values} \\
 \end{array}$$
 
 As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.
@@ -533,7 +533,7 @@ $$\begin{array}{rrcll}
   &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
   &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
   &&& \mt{val} \; x : \tau = e & \textrm{value} \\
-  &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
+  &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually recursive values} \\
   &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
   &&& \mt{signature} \; X = S & \textrm{signature definition} \\
   &&& \mt{open} \; M & \textrm{module inclusion} \\
@@ -544,7 +544,6 @@ $$\begin{array}{rrcll}
   &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
   &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
   &&& \mt{style} \; x : \tau & \textrm{CSS class} \\
-  &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
   &&& \mt{task} \; e = e & \textrm{recurring task} \\
   \\
   \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
@@ -590,7 +589,7 @@ At the expression level, an analogue is available of the composite $\lambda$ for
 
 A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable.  As for function arguments, only irrefutable patterns are legal.
 
-The keyword $\mt{fun}$ is a shorthand for $\mt{val} \; \mt{rec}$ that allows arguments to be specified before the equal sign in the definition of each mutually-recursive function, as in SML.  Each curried argument must follow the grammar of the $b$ non-terminal introduced two paragraphs ago.  A $\mt{fun}$ declaration is elaborated into a version that adds additional $\lambda$s to the fronts of the righthand sides, as appropriate.
+The keyword $\mt{fun}$ is a shorthand for $\mt{val} \; \mt{rec}$ that allows arguments to be specified before the equal sign in the definition of each mutually recursive function, as in SML.  Each curried argument must follow the grammar of the $b$ non-terminal introduced two paragraphs ago.  A $\mt{fun}$ declaration is elaborated into a version that adds additional $\lambda$s to the fronts of the righthand sides, as appropriate.
 
 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$.  A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$.
 
@@ -949,8 +948,6 @@ $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{
 
 We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$.
 
-This is the first judgment where we deal with constructor classes, for the $\mt{class}$ declaration form.  We will omit their special handling in this formal specification.  Section \ref{typeclasses} gives an informal description of how constructor classes influence type inference.
-
 We presuppose the existence of a function $\mathcal O$, where $\mathcal O(M, \overline{s})$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$.  Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained.  A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $\overline s$.
 We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$.  We write $\mt{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables.
 
@@ -1026,10 +1023,6 @@ $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{
   & \Gamma \vdash e_2 :: \tau \to \mt{Basis}.\mt{transaction} \; \{\}
 }$$
 
-$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
-  \Gamma \vdash c :: \kappa
-}$$
-
 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
   \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
@@ -1042,6 +1035,8 @@ $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
 
 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
 
+This is the first judgment where we deal with constructor classes, for the $\mt{class}$ forms.  We will omit their special handling in this formal specification.  Section \ref{typeclasses} gives an informal description of how constructor classes influence type inference.
+
 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
   \Gamma \vdash s \leadsto \Gamma'
@@ -1090,7 +1085,7 @@ $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kapp
 
 \subsection{Signature Compatibility}
 
-To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including multiple bindings for the same identifier.  This is in addition to the usual alpha-variation of locally-bound variables.
+To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including multiple bindings for the same identifier.  This is in addition to the usual alpha-variation of locally bound variables.
 
 We rely on a judgment $\Gamma \vdash \overline{s} \leq s'$, which expresses the occurrence in signature items $\overline{s}$ of an item compatible with $s'$.  We also use a judgment $\Gamma \vdash \overline{dc} \leq \overline{dc}$, which expresses compatibility of datatype definitions.
 
@@ -1201,6 +1196,12 @@ $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}
   \Gamma \vdash c_1 \equiv c_2
 }$$
 
+$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
+\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
+\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
+  \Gamma \vdash c_1 \equiv c_2
+}$$
+
 \subsection{Module Typing}
 
 We use a helper function $\mt{sigOf}$, which converts declarations and sequences of declarations into their principal signature items and sequences of signature items, respectively.
@@ -1249,8 +1250,7 @@ $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
   \mt{sigOf}(\mt{view} \; x = e) &=& \mt{view} \; x : c \textrm{ (where $\Gamma \vdash e : \mt{Basis}.\mt{sql\_query} \; [] \; [] \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; c') \; c$)} \\
   \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
   \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
-  \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\
-  \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
+  \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x
 \end{eqnarray*}
 \begin{eqnarray*}
   \mt{selfify}(M, \cdot) &=& \cdot \\
@@ -1329,11 +1329,11 @@ The type inference engine tries to take advantage of the algebraic rules governi
 
 Ur includes a constructor class facility inspired by Haskell's.  The current version is experimental, with very general Prolog-like facilities that can lead to compile-time non-termination.
 
-Constructor classes are integrated with the module system.  A constructor class of kind $\kappa$ is just a constructor of kind $\kappa$.  By marking such a constructor $c$ as a constructor class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; c_1 \; \ldots \; c_n$ as \emph{instances}.  Any function argument whose type is of such a form is treated as implicit, to be determined by examining the current instance database.
+Constructor classes are integrated with the module system.  A constructor class of kind $\kappa$ is just a constructor of kind $\kappa$.  By marking such a constructor $c$ as a constructor class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; c_1 \; \ldots \; c_n$ as \emph{instances}.  Any function argument whose type is of such a form is treated as implicit, to be determined by examining the current instance database.  Any suitably kinded constructor within a module may be exposed as a constructor class from outside the module, simply by using a $\mt{class}$ signature item instead of a $\mt{con}$ signature item in the module's signature.
 
-The ``dictionary encoding'' often used in Haskell implementations is made explicit in Ur.  Constructor class instances are just properly-typed values, and they can also be considered as ``proofs'' of membership in the class.  In some cases, it is useful to pass these proofs around explicitly.  An underscore written where a proof is expected will also be inferred, if possible, from the current instance database.
+The ``dictionary encoding'' often used in Haskell implementations is made explicit in Ur.  Constructor class instances are just properly typed values, and they can also be considered as ``proofs'' of membership in the class.  In some cases, it is useful to pass these proofs around explicitly.  An underscore written where a proof is expected will also be inferred, if possible, from the current instance database.
 
-Just as for constructors, constructors classes may be exported from modules, and they may be exported as concrete or abstract.  Concrete constructor classes have their ``real'' definitions exposed, so that client code may add new instances freely.  Abstract constructor classes are useful as ``predicates'' that can be used to enforce invariants, as we will see in some definitions of SQL syntax in the Ur/Web standard library.
+Just as for constructors, constructors classes may be exported from modules, and they may be exported as concrete or abstract.  Concrete constructor classes have their ``real'' definitions exposed, so that client code may add new instances freely.  Automatic inference of concrete class instances will not generally work, so abstract classes are almost always the right choice.  They are useful as ``predicates'' that can be used to enforce invariants, as we will see in some definitions of SQL syntax in the Ur/Web standard library.  Free extension of a concrete class is easily supported by exporting a constructor function from a module, since the class implementation will be concrete within the module.
 
 \subsection{Reverse-Engineering Record Types}
 
@@ -1434,7 +1434,7 @@ $$\begin{array}{l}
 
 \subsection{HTTP}
 
-There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies.  Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure.  For now, cookie operations are server-side only.
+There are transactions for reading an HTTP header by name and for getting and setting strongly typed cookies.  Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure.  For now, cookie operations are server-side only.
 $$\begin{array}{l}
   \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
   \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
@@ -1777,7 +1777,7 @@ $$\begin{array}{l}
   \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
 \end{array}$$
 
-Finally, we have aggregate functions.  The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument.  The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly-typed arguments.  The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.
+Finally, we have aggregate functions.  The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument.  The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly typed arguments.  The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.
 $$\begin{array}{l}
   \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int}
 \end{array}$$
@@ -1939,7 +1939,7 @@ $$\begin{array}{l}
   \mt{val} \; \mt{tryDml} : \mt{dml} \to \mt{transaction} \; (\mt{option} \; \mt{string})
 \end{array}$$
 
-Properly-typed records may be used to form $\mt{INSERT}$ commands.
+Properly typed records may be used to form $\mt{INSERT}$ commands.
 $$\begin{array}{l}
   \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
   \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
@@ -2306,7 +2306,7 @@ Similar support is provided for \cd{style} attributes.  Normal CSS syntax may be
 
 \section{\label{structure}The Structure of Web Applications}
 
-A web application is built from a series of modules, with one module, the last one appearing in the \texttt{.urp} file, designated as the main module.  The signature of the main module determines the URL entry points to the application.  Such an entry point should have type $\mt{t1} \to \ldots \to \mt{tn} \to \mt{transaction} \; \mt{page}$, for any integer $n \geq 0$, where $\mt{page}$ is a type synonym for top-level HTML pages, defined in $\mt{Basis}$.  If such a function is at the top level of main module $M$, with $n = 0$, it will be accessible at URI \texttt{/M/f}, and so on for more deeply-nested functions, as described in Section \ref{tag} below.  See Section \ref{cl} for information on the \texttt{prefix} and \texttt{rewrite url} directives, which can be used to rewrite the default URIs of different entry point functions.  The final URL of a function is its default module-based URI, with \texttt{rewrite url} rules applied, and with the \texttt{prefix} prepended.  Arguments to an entry-point function are deserialized from the part of the URI following \texttt{f}.
+A web application is built from a series of modules, with one module, the last one appearing in the \texttt{.urp} file, designated as the main module.  The signature of the main module determines the URL entry points to the application.  Such an entry point should have type $\mt{t1} \to \ldots \to \mt{tn} \to \mt{transaction} \; \mt{page}$, for any integer $n \geq 0$, where $\mt{page}$ is a type synonym for top-level HTML pages, defined in $\mt{Basis}$.  If such a function is at the top level of main module $M$, with $n = 0$, it will be accessible at URI \texttt{/M/f}, and so on for more deeply nested functions, as described in Section \ref{tag} below.  See Section \ref{cl} for information on the \texttt{prefix} and \texttt{rewrite url} directives, which can be used to rewrite the default URIs of different entry point functions.  The final URL of a function is its default module-based URI, with \texttt{rewrite url} rules applied, and with the \texttt{prefix} prepended.  Arguments to an entry-point function are deserialized from the part of the URI following \texttt{f}.
 
 Elements of modules beside the main module, including page handlers, will only be included in the final application if they are transitive dependencies of the handlers in the main module.
 
@@ -2506,7 +2506,7 @@ Functions are specialized to particular argument patterns.  This is an important
 
 \subsection{Untangle}
 
-Remove unnecessary mutual recursion, splitting recursive groups into strongly-connected components.
+Remove unnecessary mutual recursion, splitting recursive groups into strongly connected components.
 
 \subsection{Shake}
 
diff --git a/src/elab.sml b/src/elab.sml
index 15365951..9147f7d3 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -175,7 +175,6 @@ datatype decl' =
        | DTable of int * string * int * con * exp * con * exp * con
        | DSequence of int * string * int
        | DView of int * string * int * exp * con
-       | DClass of string * int * kind * con
        | DDatabase of string
        | DCookie of int * string * int * con
        | DStyle of int * string * int
diff --git a/src/elab_env.sml b/src/elab_env.sml
index f31804f2..5d684817 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1647,13 +1647,6 @@ fun declBinds env (d, loc) =
         in
             pushENamedAs env x n ct
         end
-      | DClass (x, n, k, c) =>
-        let
-            val k = (KArrow (k, (KType, loc)), loc)
-            val env = pushCNamedAs env x n k (SOME c)
-        in
-            pushClass env n
-        end
       | DDatabase _ => env
       | DCookie (tn, x, n, c) =>
         let
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 37669312..c32368a9 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -828,17 +828,6 @@ fun p_decl env (dAll as (d, _) : decl) =
                                       string "as",
                                       space,
                                       p_exp env e]
-      | DClass (x, n, k, c) => box [string "class",
-                                    space,
-                                    p_named x n,
-                                    space,
-                                    string "::",
-                                    space,
-                                    p_kind env k,
-                                    space,
-                                    string "=",
-                                    space,
-                                    p_con env c]
       | DDatabase s => box [string "database",
                             space,
                             string s]
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 97e3b572..51bcba5a 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -919,8 +919,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                    in
                                                        bind (ctx, NamedE (x, ct))
                                                    end
-                                                 | DClass (x, n, k, c) =>
-                                                   bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c))
                                                  | DDatabase _ => ctx
                                                  | DCookie (tn, x, n, c) =>
                                                    bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
@@ -1040,13 +1038,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                    fn c' =>
                                       (DView (tn, x, n, e', c'), loc)))
 
-              | DClass (x, n, k, c) =>
-                S.bind2 (mfk ctx k,
-                         fn k' =>
-                            S.map2 (mfc ctx c,
-                                 fn c' =>
-                                    (DClass (x, n, k', c'), loc)))
-
               | DDatabase _ => S.return2 dAll
 
               | DCookie (tn, x, n, c) =>
@@ -1233,7 +1224,6 @@ and maxNameDecl (d, _) =
       | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | DConstraint _ => 0
-      | DClass (_, n, _, _) => n
       | DExport _ => 0
       | DTable (n1, _, n2, _, _, _, _, _) => Int.max (n1, n2)
       | DSequence (n1, _, n2) => Int.max (n1, n2)
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 8436c975..426934bd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2982,7 +2982,6 @@ and sgiOfDecl (d, loc) =
       | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
       | L'.DView (tn, x, n, _, c) =>
         [(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), loc)]
-      | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
       | L'.DDatabase _ => []
       | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
       | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
@@ -3362,6 +3361,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                      case sgi1 of
                                          L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
                                        | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
+                                       | L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
+                                       | L'.SgiCon (x', n1, k1, c) => found (x', n1, k1, SOME c)
                                        | _ => NONE
                                  end)
                       | L'.SgiClass (x, n2, k2, c2) =>
@@ -3401,6 +3402,7 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                  in
                                      case sgi1 of
                                          L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
+                                       | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
                                        | _ => NONE
                                  end)
                 end
@@ -3508,7 +3510,6 @@ and wildifyStr env (str, sgn) =
                  fun dname (d, _) =
                      case d of
                          L.DCon (x, _, _) => SOME x
-                       | L.DClass (x, _, _) => SOME x
                        | _ => NONE
                                                      
                  fun decompileKind (k, loc) =
@@ -3641,7 +3642,6 @@ and wildifyStr env (str, sgn) =
                      foldl (fn ((d, _), nd) =>
                                case d of
                                    L.DCon (x, _, _) => ndelCon (nd, x)
-                                 | L.DClass (x, _, _) => ndelCon (nd, x)
                                  | L.DVal (x, _, _) => ndelVal (nd, x)
                                  | L.DOpen _ => nempty
                                  | L.DStr (x, _, _, (L.StrConst ds', _)) =>
@@ -3666,7 +3666,6 @@ and wildifyStr env (str, sgn) =
                                             | L.DDatatypeImp _ => true
                                             | L.DStr _ => true
                                             | L.DConstraint _ => true
-                                            | L.DClass _ => true
                                             | _ => false
                          in
                              if isCony then
@@ -4184,17 +4183,6 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                      (env', denv, gs' @ gs))
                 end
 
-              | L.DClass (x, k, c) =>
-                let
-                    val k = elabKind env k
-                    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'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
-                end
-
               | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
 
               | L.DCookie (x, c) =>
diff --git a/src/explify.sml b/src/explify.sml
index 3c922a44..65e78443 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -192,8 +192,6 @@ fun explifyDecl (d, loc : EM.span) =
       | L.DView (nt, x, n, e, c) =>
         SOME (L'.DView (nt, x, n, explifyExp e, explifyCon c), loc)
       | L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc)
-      | L.DClass (x, n, k, c) => SOME (L'.DCon (x, n,
-                                                (L'.KArrow (explifyKind k, (L'.KType, loc)), loc), explifyCon c), loc)
       | L.DDatabase s => SOME (L'.DDatabase s, loc)
       | L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc)
       | L.DStyle (nt, x, n) => SOME (L'.DStyle (nt, x, n), loc)
diff --git a/src/source.sml b/src/source.sml
index 8b126628..18f83d2b 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -163,7 +163,6 @@ datatype decl' =
        | DTable of string * con * exp * exp
        | DSequence of string
        | DView of string * exp
-       | DClass of string * kind * con
        | DDatabase of string
        | DCookie of string * con
        | DStyle of string
diff --git a/src/source_print.sml b/src/source_print.sml
index aad673f3..cd3314e1 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -640,13 +640,6 @@ fun p_decl ((d, _) : decl) =
                              string "=",
                              space,
                              p_exp e]
-      | DClass (x, k, c) => box [string "class",
-                                 space,
-                                 string x,
-                                 space,
-                                 string "=",
-                                 space,
-                                 p_con c]
 
       | DDatabase s => box [string "database",
                             space,
diff --git a/src/unnest.sml b/src/unnest.sml
index 2d6956cb..52d729d7 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -428,7 +428,6 @@ fun unnest file =
                   | DTable _ => default ()
                   | DSequence _ => default ()
                   | DView _ => default ()
-                  | DClass _ => default ()
                   | DDatabase _ => default ()
                   | DCookie _ => default ()
                   | DStyle _ => default ()
diff --git a/src/urweb.grm b/src/urweb.grm
index 708e5fcd..084cec1e 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -602,25 +602,6 @@ decl   : CON SYMBOL cargl2 kopt EQ cexp (let
                                            s (VIEWleft, queryright))])
        | VIEW SYMBOL EQ LBRACE eexp RBRACE ([(DView (SYMBOL, eexp),
                                            s (VIEWleft, RBRACEright))])
-       | CLASS SYMBOL EQ cexp           (let
-                                             val loc = s (CLASSleft, cexpright)
-                                         in
-                                             [(DClass (SYMBOL, (KWild, loc), cexp), loc)]
-                                         end)
-       | CLASS SYMBOL DCOLON kind EQ cexp ([(DClass (SYMBOL, kind, cexp), s (CLASSleft, cexpright))])
-       | CLASS SYMBOL SYMBOL EQ cexp    (let
-                                             val loc = s (CLASSleft, cexpright)
-                                             val k = (KWild, loc)
-                                             val c = (CAbs (SYMBOL2, SOME k, cexp), loc)
-                                         in
-                                             [(DClass (SYMBOL1, k, c), s (CLASSleft, cexpright))]
-                                         end)
-       | CLASS SYMBOL LPAREN SYMBOL DCOLON kind RPAREN EQ cexp (let
-                                             val loc = s (CLASSleft, cexpright)
-                                             val c = (CAbs (SYMBOL2, SOME kind, cexp), loc)
-                                         in
-                                             [(DClass (SYMBOL1, kind, c), s (CLASSleft, cexpright))]
-                                         end)
        | COOKIE SYMBOL COLON cexp       ([(DCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))])
        | STYLE SYMBOL                   ([(DStyle SYMBOL, s (STYLEleft, SYMBOLright))])
        | TASK eapps EQ eexp             ([(DTask (eapps, eexp), s (TASKleft, eexpright))])