changeset 329:eec65c11d3e2

foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents 58f1260f293f
children f307cdd08d81
files lib/top.ur lib/top.urs src/elab_err.sig src/elab_err.sml src/elab_ops.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/sources src/urweb.grm tests/crud.ur tests/crud.urs
diffstat 12 files changed, 593 insertions(+), 328 deletions(-) [+]
line wrap: on
line diff
--- a/lib/top.ur	Thu Sep 11 19:59:31 2008 -0400
+++ b/lib/top.ur	Sat Sep 13 10:30:45 2008 -0400
@@ -1,3 +1,6 @@
+con idT = fn t :: Type => t
+con record = fn t :: {Type} => $t
+
 con mapTT (f :: Type -> Type) = fold (fn nm t acc => [nm] ~ acc =>
         [nm = f t] ++ acc) []
 
@@ -5,7 +8,7 @@
 
 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v)
 
-fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
+val foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
                 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
--- a/lib/top.urs	Thu Sep 11 19:59:31 2008 -0400
+++ b/lib/top.urs	Sat Sep 13 10:30:45 2008 -0400
@@ -1,3 +1,6 @@
+con idT = fn t :: Type => t
+con record = fn t :: {Type} => $t
+
 con mapTT = fn f :: Type -> Type => fold (fn nm t acc => [nm] ~ acc =>
         [nm = f t] ++ acc) []
 
@@ -6,3 +9,8 @@
 
 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
         -> xml ctx use []
+
+val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
+        -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
+                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+        -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/elab_err.sig	Sat Sep 13 10:30:45 2008 -0400
@@ -0,0 +1,113 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature ELAB_ERR = sig
+
+    datatype kunify_error =
+             KOccursCheckFailed of Elab.kind * Elab.kind
+           | KIncompatible of Elab.kind * Elab.kind
+
+    val kunifyError : kunify_error -> unit
+
+    datatype con_error =
+             UnboundCon of ErrorMsg.span * string
+           | UnboundDatatype of ErrorMsg.span * string
+           | UnboundStrInCon of ErrorMsg.span * string
+           | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error
+           | DuplicateField of ErrorMsg.span * string
+           | ProjBounds of Elab.con * int
+           | ProjMismatch of Elab.con * Elab.kind
+
+    val conError : ElabEnv.env -> con_error -> unit
+
+    datatype cunify_error =
+             CKind of Elab.kind * Elab.kind * kunify_error
+           | COccursCheckFailed of Elab.con * Elab.con
+           | CIncompatible of Elab.con * Elab.con
+           | CExplicitness of Elab.con * Elab.con
+           | CKindof of Elab.kind * Elab.con
+           | CRecordFailure of Elab.con * Elab.con
+
+    val cunifyError : ElabEnv.env -> cunify_error -> unit
+
+    datatype exp_error =
+             UnboundExp of ErrorMsg.span * string
+           | UnboundStrInExp of ErrorMsg.span * string
+           | Unify of Elab.exp * Elab.con * Elab.con * cunify_error
+           | Unif of string * Elab.con
+           | WrongForm of string * Elab.exp * Elab.con
+           | IncompatibleCons of Elab.con * Elab.con
+           | DuplicatePatternVariable of ErrorMsg.span * string
+           | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error
+           | UnboundConstructor of ErrorMsg.span * string list * string
+           | PatHasArg of ErrorMsg.span
+           | PatHasNoArg of ErrorMsg.span
+           | Inexhaustive of ErrorMsg.span
+           | DuplicatePatField of ErrorMsg.span * string
+           | Unresolvable of ErrorMsg.span * Elab.con
+           | OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option
+           | IllegalRec of string * Elab.exp
+
+    val expError : ElabEnv.env -> exp_error -> unit
+
+    datatype decl_error =
+             KunifsRemain of Elab.decl list
+           | CunifsRemain of Elab.decl list
+           | Nonpositive of Elab.decl
+
+    val declError : ElabEnv.env -> decl_error -> unit
+
+    datatype sgn_error =
+             UnboundSgn of ErrorMsg.span * string
+           | UnmatchedSgi of Elab.sgn_item
+           | SgiWrongKind of Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
+           | SgiWrongCon of Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
+           | SgiMismatchedDatatypes of Elab.sgn_item * Elab.sgn_item * (Elab.con * Elab.con * cunify_error) option
+           | SgnWrongForm of Elab.sgn * Elab.sgn
+           | UnWhereable of Elab.sgn * string
+           | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
+           | NotIncludable of Elab.sgn
+           | DuplicateCon of ErrorMsg.span * string
+           | DuplicateVal of ErrorMsg.span * string
+           | DuplicateSgn of ErrorMsg.span * string
+           | DuplicateStr of ErrorMsg.span * string
+           | NotConstraintsable of Elab.sgn
+
+    val sgnError : ElabEnv.env -> sgn_error -> unit
+
+    datatype str_error =
+             UnboundStr of ErrorMsg.span * string
+           | NotFunctor of Elab.sgn
+           | FunctorRebind of ErrorMsg.span
+           | UnOpenable of Elab.sgn
+           | NotType of Elab.kind * (Elab.kind * Elab.kind * kunify_error)
+           | DuplicateConstructor of string * ErrorMsg.span
+           | NotDatatype of ErrorMsg.span
+
+    val strError : ElabEnv.env -> str_error -> unit
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/elab_err.sml	Sat Sep 13 10:30:45 2008 -0400
@@ -0,0 +1,349 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure ElabErr :> ELAB_ERR = struct
+
+structure L = Source
+open Elab
+
+structure E = ElabEnv
+structure U = ElabUtil
+
+open Print
+structure P = ElabPrint
+
+val simplCon = U.Con.mapB {kind = fn k => k,
+                           con = fn env => fn c =>
+                                              let
+                                                  val c = (c, ErrorMsg.dummySpan)
+                                                  val (c', _) = Disjoint.hnormCon (env, Disjoint.empty) c
+                                              in
+                                                  (*prefaces "simpl" [("c", P.p_con env c),
+                                                                    ("c'", P.p_con env c')];*)
+                                                  #1 c'
+                                              end,
+                           bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k
+                                   | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE}
+
+val p_kind = P.p_kind
+
+datatype kunify_error =
+         KOccursCheckFailed of kind * kind
+       | KIncompatible of kind * kind
+
+fun kunifyError err =
+    case err of
+        KOccursCheckFailed (k1, k2) =>
+        eprefaces "Kind occurs check failed"
+        [("Kind 1", p_kind k1),
+         ("Kind 2", p_kind k2)]
+      | KIncompatible (k1, k2) =>
+        eprefaces "Incompatible kinds"
+        [("Kind 1", p_kind k1),
+         ("Kind 2", p_kind k2)]
+
+
+fun p_con env c = P.p_con env (simplCon env c)
+
+datatype con_error =
+         UnboundCon of ErrorMsg.span * string
+       | UnboundDatatype of ErrorMsg.span * string
+       | UnboundStrInCon of ErrorMsg.span * string
+       | WrongKind of con * kind * kind * kunify_error
+       | DuplicateField of ErrorMsg.span * string
+       | ProjBounds of con * int
+       | ProjMismatch of con * kind
+
+fun conError env err =
+    case err of
+        UnboundCon (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
+      | UnboundDatatype (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
+      | UnboundStrInCon (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound structure " ^ s)
+      | WrongKind (c, k1, k2, kerr) =>
+        (ErrorMsg.errorAt (#2 c) "Wrong kind";
+         eprefaces' [("Constructor", p_con env c),
+                     ("Have kind", p_kind k1),
+                     ("Need kind", p_kind k2)];
+         kunifyError kerr)
+      | DuplicateField (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
+      | ProjBounds (c, n) =>
+        (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
+         eprefaces' [("Constructor", p_con env c),
+                     ("Index", Print.PD.string (Int.toString n))])
+      | ProjMismatch (c, k) =>
+        (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
+         eprefaces' [("Constructor", p_con env c),
+                     ("Kind", p_kind k)])
+
+
+datatype cunify_error =
+         CKind of kind * kind * kunify_error
+       | COccursCheckFailed of con * con
+       | CIncompatible of con * con
+       | CExplicitness of con * con
+       | CKindof of kind * con
+       | CRecordFailure of con * con
+
+fun cunifyError env err =
+    case err of
+        CKind (k1, k2, kerr) =>
+        (eprefaces "Kind unification failure"
+                   [("Kind 1", p_kind k1),
+                    ("Kind 2", p_kind k2)];
+         kunifyError kerr)
+      | COccursCheckFailed (c1, c2) =>
+        eprefaces "Constructor occurs check failed"
+                  [("Con 1", p_con env c1),
+                   ("Con 2", p_con env c2)]
+      | CIncompatible (c1, c2) =>
+        eprefaces "Incompatible constructors"
+                  [("Con 1", p_con env c1),
+                   ("Con 2", p_con env c2)]
+      | CExplicitness (c1, c2) =>
+        eprefaces "Differing constructor function explicitness"
+                  [("Con 1", p_con env c1),
+                   ("Con 2", p_con env c2)]
+      | CKindof (k, c) =>
+        eprefaces "Unexpected kind for kindof calculation"
+                  [("Kind", p_kind k),
+                   ("Con", p_con env c)]
+      | CRecordFailure (c1, c2) =>
+        eprefaces "Can't unify record constructors"
+                  [("Summary 1", p_con env c1),
+                   ("Summary 2", p_con env c2)]
+
+datatype exp_error =
+       UnboundExp of ErrorMsg.span * string
+     | UnboundStrInExp of ErrorMsg.span * string
+     | Unify of exp * con * con * cunify_error
+     | Unif of string * con
+     | WrongForm of string * exp * con
+     | IncompatibleCons of con * con
+     | DuplicatePatternVariable of ErrorMsg.span * string
+     | PatUnify of pat * con * con * cunify_error
+     | UnboundConstructor of ErrorMsg.span * string list * string
+     | PatHasArg of ErrorMsg.span
+     | PatHasNoArg of ErrorMsg.span
+     | Inexhaustive of ErrorMsg.span
+     | DuplicatePatField of ErrorMsg.span * string
+     | Unresolvable of ErrorMsg.span * con
+     | OutOfContext of ErrorMsg.span * (exp * con) option
+     | IllegalRec of string * exp
+
+val p_exp = P.p_exp
+val p_pat = P.p_pat
+
+fun expError env err =
+    case err of
+        UnboundExp (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
+      | UnboundStrInExp (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound structure " ^ s)
+      | Unify (e, c1, c2, uerr) =>
+        (ErrorMsg.errorAt (#2 e) "Unification failure";
+         eprefaces' [("Expression", p_exp env e),
+                     ("Have con", p_con env c1),
+                     ("Need con", p_con env c2)];
+         cunifyError env uerr)
+      | Unif (action, c) =>
+        (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
+         eprefaces' [("Con", p_con env c)])
+      | WrongForm (variety, e, t) =>
+        (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
+         eprefaces' [("Expression", p_exp env e),
+                     ("Type", p_con env t)])
+      | IncompatibleCons (c1, c2) =>
+        (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
+         eprefaces' [("Con 1", p_con env c1),
+                     ("Con 2", p_con env c2)])
+      | DuplicatePatternVariable (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
+      | PatUnify (p, c1, c2, uerr) =>
+        (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
+         eprefaces' [("Pattern", p_pat env p),
+                     ("Have con", p_con env c1),
+                     ("Need con", p_con env c2)];
+         cunifyError env uerr)
+      | UnboundConstructor (loc, ms, s) =>
+        ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
+      | PatHasArg loc =>
+        ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
+      | PatHasNoArg loc =>
+        ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
+      | Inexhaustive loc =>
+        ErrorMsg.errorAt loc "Inexhaustive 'case'"
+      | DuplicatePatField (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
+      | OutOfContext (loc, co) =>
+        (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
+         Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
+                                              ("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)])
+      | IllegalRec (x, e) =>
+        (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
+         eprefaces' [("Variable", PD.string x),
+                     ("Expression", p_exp env e)])
+
+
+datatype decl_error =
+         KunifsRemain of decl list
+       | CunifsRemain of decl list
+       | Nonpositive of decl
+
+fun lspan [] = ErrorMsg.dummySpan
+  | lspan ((_, loc) :: _) = loc
+
+val p_decl = P.p_decl
+
+fun declError env err =
+    case err of
+        KunifsRemain ds =>
+        (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
+         eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
+      | CunifsRemain ds =>
+        (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
+         eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
+      | Nonpositive d =>
+        (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
+         eprefaces' [("Decl", p_decl env d)])
+
+datatype sgn_error =
+         UnboundSgn of ErrorMsg.span * string
+       | UnmatchedSgi of sgn_item
+       | SgiWrongKind of sgn_item * kind * sgn_item * kind * kunify_error
+       | SgiWrongCon of sgn_item * con * sgn_item * con * cunify_error
+       | SgiMismatchedDatatypes of sgn_item * sgn_item * (con * con * cunify_error) option
+       | SgnWrongForm of sgn * sgn
+       | UnWhereable of sgn * string
+       | WhereWrongKind of kind * kind * kunify_error
+       | NotIncludable of sgn
+       | DuplicateCon of ErrorMsg.span * string
+       | DuplicateVal of ErrorMsg.span * string
+       | DuplicateSgn of ErrorMsg.span * string
+       | DuplicateStr of ErrorMsg.span * string
+       | NotConstraintsable of sgn
+
+val p_sgn_item = P.p_sgn_item
+val p_sgn = P.p_sgn
+
+fun sgnError env err =
+    case err of
+        UnboundSgn (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
+      | UnmatchedSgi (sgi as (_, loc)) =>
+        (ErrorMsg.errorAt loc "Unmatched signature item";
+         eprefaces' [("Item", p_sgn_item env sgi)])
+      | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
+        (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
+         eprefaces' [("Have", p_sgn_item env sgi1),
+                     ("Need", p_sgn_item env sgi2),
+                     ("Kind 1", p_kind k1),
+                     ("Kind 2", p_kind k2)];
+         kunifyError kerr)
+      | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
+        (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
+         eprefaces' [("Have", p_sgn_item env sgi1),
+                     ("Need", p_sgn_item env sgi2),
+                     ("Con 1", p_con env c1),
+                     ("Con 2", p_con env c2)];
+         cunifyError env cerr)
+      | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
+        (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
+         eprefaces' [("Have", p_sgn_item env sgi1),
+                     ("Need", p_sgn_item env sgi2)];
+         Option.app (fn (c1, c2, ue) =>
+                        (eprefaces "Unification error"
+                                   [("Con 1", p_con env c1),
+                                    ("Con 2", p_con env c2)];
+                         cunifyError env ue)) cerro)
+      | SgnWrongForm (sgn1, sgn2) =>
+        (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
+         eprefaces' [("Sig 1", p_sgn env sgn1),
+                     ("Sig 2", p_sgn env sgn2)])
+      | UnWhereable (sgn, x) =>
+        (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
+         eprefaces' [("Signature", p_sgn env sgn),
+                     ("Field", PD.string x)])
+      | WhereWrongKind (k1, k2, kerr) =>
+        (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
+         eprefaces' [("Have", p_kind k1),
+                     ("Need", p_kind k2)];
+         kunifyError kerr)
+      | NotIncludable sgn =>
+        (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
+         eprefaces' [("Signature", p_sgn env sgn)])
+      | DuplicateCon (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
+      | DuplicateVal (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
+      | DuplicateSgn (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
+      | DuplicateStr (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
+      | NotConstraintsable sgn =>
+        (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
+         eprefaces' [("Signature", p_sgn env sgn)])
+
+datatype str_error =
+         UnboundStr of ErrorMsg.span * string
+       | NotFunctor of sgn
+       | FunctorRebind of ErrorMsg.span
+       | UnOpenable of sgn
+       | NotType of kind * (kind * kind * kunify_error)
+       | DuplicateConstructor of string * ErrorMsg.span
+       | NotDatatype of ErrorMsg.span
+
+fun strError env err =
+    case err of
+        UnboundStr (loc, s) =>
+        ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
+      | NotFunctor sgn =>
+        (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
+         eprefaces' [("Signature", p_sgn env sgn)])
+      | FunctorRebind loc =>
+        ErrorMsg.errorAt loc "Attempt to rebind functor"
+      | UnOpenable sgn =>
+        (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
+         eprefaces' [("Signature", p_sgn env sgn)])
+      | NotType (k, (k1, k2, ue)) =>
+        (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
+         eprefaces' [("Kind", p_kind k),
+                     ("Subkind 1", p_kind k1),
+                     ("Subkind 2", p_kind k2)];
+         kunifyError ue)
+      | DuplicateConstructor (x, loc) =>
+        ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
+      | NotDatatype loc =>
+        ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
+
+end
--- a/src/elab_ops.sml	Thu Sep 11 19:59:31 2008 -0400
+++ b/src/elab_ops.sml	Sat Sep 13 10:30:45 2008 -0400
@@ -127,7 +127,47 @@
                                                    (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
                                                           rest''), loc)), loc)
                                end
-                             | _ => default ())
+                             | _ =>
+                               let
+                                   fun cunif () =
+                                       let
+                                           val r = ref NONE
+                                       in
+                                           (r, (CUnif (loc, (KType, loc), "_", r), loc))
+                                       end
+
+                                   val (nmR, nm) = cunif ()
+                                   val (vR, v) = cunif ()
+                                   val (rR, r) = cunif ()
+
+                                   val c = f
+                                   val c = (CApp (c, nm), loc)
+                                   val c = (CApp (c, v), loc)
+                                   val c = (CApp (c, r), loc)
+                                   fun unconstraint c =
+                                       case hnormCon env c of
+                                           (CDisjoint (_, _, c), _) => unconstraint c
+                                         | c => c
+                                   val c = unconstraint c
+                               in
+                                   (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
+                                   case (hnormCon env i, unconstraint c) of
+                                       ((CRecord (_, []), _),
+                                        (CConcat (c1, c2'), _)) =>
+                                       (case (hnormCon env c1, hnormCon env c2') of
+                                            ((CRecord (_, [(nm', v')]), _),
+                                             (CUnif (_, _, _, rR'), _)) =>
+                                            (case (hnormCon env nm', hnormCon env v') of
+                                                 ((CUnif (_, _, _, nmR'), _),
+                                                  (CUnif (_, _, _, vR'), _)) =>
+                                                 if nmR' = nmR andalso vR' = vR andalso rR' = rR then
+                                                     hnormCon env c2
+                                                 else
+                                                     default ()
+                                               | _ => default ())
+                                          | _ => default ())
+                                     | _ => default ()
+                               end)
                         | _ => default ())
                    | _ => default ()
              end
@@ -141,7 +181,7 @@
            | ((CConcat (c11, c12), loc), c2') =>
              hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
            | (c1', (CRecord (_, []), _)) => c1'
-           | _ => cAll)
+           | (c1', c2') => (CConcat (c1', c2'), loc))
 
       | CProj (c, n) =>
         (case hnormCon env c of
--- a/src/elab_util.sig	Thu Sep 11 19:59:31 2008 -0400
+++ b/src/elab_util.sig	Sat Sep 13 10:30:45 2008 -0400
@@ -38,7 +38,7 @@
 structure Con : sig
     datatype binder =
              Rel of string * Elab.kind
-           | Named of string * Elab.kind
+           | Named of string * int * Elab.kind
 
     val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
@@ -62,7 +62,7 @@
 structure Exp : sig
     datatype binder =
              RelC of string * Elab.kind
-           | NamedC of string * Elab.kind
+           | NamedC of string * int * Elab.kind
            | RelE of string * Elab.con
            | NamedE of string * Elab.con
 
@@ -88,7 +88,7 @@
 structure Sgn : sig
     datatype binder =
              RelC of string * Elab.kind
-           | NamedC of string * Elab.kind
+           | NamedC of string * int * Elab.kind
            | Str of string * Elab.sgn
            | Sgn of string * Elab.sgn
 
@@ -117,7 +117,7 @@
 structure Decl : sig
     datatype binder =
              RelC of string * Elab.kind
-           | NamedC of string * Elab.kind
+           | NamedC of string * int * Elab.kind
            | RelE of string * Elab.con
            | NamedE of string * Elab.con
            | Str of string * Elab.sgn
--- a/src/elab_util.sml	Thu Sep 11 19:59:31 2008 -0400
+++ b/src/elab_util.sml	Sat Sep 13 10:30:45 2008 -0400
@@ -96,7 +96,7 @@
 
 datatype binder =
          Rel of string * Elab.kind
-       | Named of string * Elab.kind
+       | Named of string * int * Elab.kind
 
 fun mapfoldB {kind = fk, con = fc, bind} =
     let
@@ -240,7 +240,7 @@
 
 datatype binder =
          RelC of string * Elab.kind
-       | NamedC of string * Elab.kind
+       | NamedC of string * int * Elab.kind
        | RelE of string * Elab.con
        | NamedE of string * Elab.con
 
@@ -392,7 +392,7 @@
 
 datatype binder =
          RelC of string * Elab.kind
-       | NamedC of string * Elab.kind
+       | NamedC of string * int * Elab.kind
        | Str of string * Elab.sgn
        | Sgn of string * Elab.sgn
 
@@ -479,14 +479,14 @@
                 SgnConst sgis =>
                 S.map2 (ListUtil.mapfoldB (fn (ctx, si)  =>
                                               (case #1 si of
-                                                   SgiConAbs (x, _, k) =>
-                                                   bind (ctx, NamedC (x, k))
-                                                 | SgiCon (x, _, k, _) =>
-                                                   bind (ctx, NamedC (x, k))
+                                                   SgiConAbs (x, n, k) =>
+                                                   bind (ctx, NamedC (x, n, k))
+                                                 | SgiCon (x, n, k, _) =>
+                                                   bind (ctx, NamedC (x, n, k))
                                                  | SgiDatatype (x, n, _, xncs) =>
-                                                   bind (ctx, NamedC (x, (KType, loc)))
-                                                 | SgiDatatypeImp (x, _, _, _, _, _, _) =>
-                                                   bind (ctx, NamedC (x, (KType, loc)))
+                                                   bind (ctx, NamedC (x, n, (KType, loc)))
+                                                 | SgiDatatypeImp (x, n, _, _, _, _, _) =>
+                                                   bind (ctx, NamedC (x, n, (KType, loc)))
                                                  | SgiVal _ => ctx
                                                  | SgiStr (x, _, sgn) =>
                                                    bind (ctx, Str (x, sgn))
@@ -494,10 +494,10 @@
                                                    bind (ctx, Sgn (x, sgn))
                                                  | SgiConstraint _ => 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))),
+                                                 | SgiClassAbs (x, n) =>
+                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
+                                                 | SgiClass (x, n, _) =>
+                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -542,7 +542,7 @@
 
 datatype binder =
          RelC of string * Elab.kind
-       | NamedC of string * Elab.kind
+       | NamedC of string * int * Elab.kind
        | RelE of string * Elab.con
        | NamedE of string * Elab.con
        | Str of string * Elab.sgn
@@ -594,11 +594,11 @@
                 StrConst ds => 
                 S.map2 (ListUtil.mapfoldB (fn (ctx, d)  =>
                                               (case #1 d of
-                                                   DCon (x, _, k, _) =>
-                                                   bind (ctx, NamedC (x, k))
+                                                   DCon (x, n, k, _) =>
+                                                   bind (ctx, NamedC (x, n, k))
                                                  | DDatatype (x, n, xs, xncs) =>
                                                    let
-                                                       val ctx = bind (ctx, NamedC (x, (KType, loc)))
+                                                       val ctx = bind (ctx, NamedC (x, n, (KType, loc)))
                                                    in
                                                        foldl (fn ((x, _, co), ctx) =>
                                                                  let
@@ -621,7 +621,7 @@
                                                        ctx xncs
                                                    end
                                                  | DDatatypeImp (x, n, m, ms, x', _, _) =>
-                                                   bind (ctx, NamedC (x, (KType, loc)))
+                                                   bind (ctx, NamedC (x, n, (KType, loc)))
                                                  | DVal (x, _, c, _) =>
                                                    bind (ctx, NamedE (x, c))
                                                  | DValRec vis =>
@@ -637,8 +637,8 @@
                                                  | DTable (tn, x, n, c) =>
                                                    bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc),
                                                                                 c), loc)))
-                                                 | DClass (x, _, _) =>
-                                                   bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc)))
+                                                 | DClass (x, n, _) =>
+                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
                                                  | DDatabase _ => ctx,
                                                mfd ctx d)) ctx ds,
                      fn ds' => (StrConst ds', loc))
--- a/src/elaborate.sml	Thu Sep 11 19:59:31 2008 -0400
+++ b/src/elaborate.sml	Sat Sep 13 10:30:45 2008 -0400
@@ -36,6 +36,7 @@
 
 open Print
 open ElabPrint
+open ElabErr
 
 structure IM = IntBinaryMap
 
@@ -58,23 +59,8 @@
     U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
                     | _ => false)
 
-datatype kunify_error =
-         KOccursCheckFailed of L'.kind * L'.kind
-       | KIncompatible of L'.kind * L'.kind
-
 exception KUnify' of kunify_error
 
-fun kunifyError err =
-    case err of
-        KOccursCheckFailed (k1, k2) =>
-        eprefaces "Kind occurs check failed"
-        [("Kind 1", p_kind k1),
-         ("Kind 2", p_kind k2)]
-      | KIncompatible (k1, k2) =>
-        eprefaces "Incompatible kinds"
-        [("Kind 1", p_kind k1),
-         ("Kind 2", p_kind k2)]
-
 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
     let
         fun err f = raise KUnify' (f (k1All, k2All))
@@ -124,40 +110,6 @@
     unifyKinds' k1 k2
     handle KUnify' err => raise KUnify (k1, k2, err)
 
-datatype con_error =
-         UnboundCon of ErrorMsg.span * string
-       | UnboundDatatype of ErrorMsg.span * string
-       | UnboundStrInCon of ErrorMsg.span * string
-       | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
-       | DuplicateField of ErrorMsg.span * string
-       | ProjBounds of L'.con * int
-       | ProjMismatch of L'.con * L'.kind
-
-fun conError env err =
-    case err of
-        UnboundCon (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
-      | UnboundDatatype (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
-      | UnboundStrInCon (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound structure " ^ s)
-      | WrongKind (c, k1, k2, kerr) =>
-        (ErrorMsg.errorAt (#2 c) "Wrong kind";
-         eprefaces' [("Constructor", p_con env c),
-                     ("Have kind", p_kind k1),
-                     ("Need kind", p_kind k2)];
-         kunifyError kerr)
-      | DuplicateField (loc, s) =>
-        ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
-      | ProjBounds (c, n) =>
-        (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
-         eprefaces' [("Constructor", p_con env c),
-                     ("Index", Print.PD.string (Int.toString n))])
-      | ProjMismatch (c, k) =>
-        (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
-         eprefaces' [("Constructor", p_con env c),
-                     ("Kind", p_kind k)])
-
 fun checkKind env c k1 k2 =
     unifyKinds k1 k2
     handle KUnify (k1, k2, err) =>
@@ -495,44 +447,8 @@
                   con = fn L'.CUnif (_, _, _, r') => r = r'
                          | _ => false}
 
-datatype cunify_error =
-         CKind of L'.kind * L'.kind * kunify_error
-       | COccursCheckFailed of L'.con * L'.con
-       | CIncompatible of L'.con * L'.con
-       | CExplicitness of L'.con * L'.con
-       | CKindof of L'.kind * L'.con
-       | CRecordFailure of PD.pp_desc * PD.pp_desc
-
 exception CUnify' of cunify_error
 
-fun cunifyError env err =
-    case err of
-        CKind (k1, k2, kerr) =>
-        (eprefaces "Kind unification failure"
-                   [("Kind 1", p_kind k1),
-                    ("Kind 2", p_kind k2)];
-         kunifyError kerr)
-      | COccursCheckFailed (c1, c2) =>
-        eprefaces "Constructor occurs check failed"
-                  [("Con 1", p_con env c1),
-                   ("Con 2", p_con env c2)]
-      | CIncompatible (c1, c2) =>
-        eprefaces "Incompatible constructors"
-                  [("Con 1", p_con env c1),
-                   ("Con 2", p_con env c2)]
-      | CExplicitness (c1, c2) =>
-        eprefaces "Differing constructor function explicitness"
-                  [("Con 1", p_con env c1),
-                   ("Con 2", p_con env c2)]
-      | CKindof (k, c) =>
-        eprefaces "Unexpected kind for kindof calculation"
-                  [("Kind", p_kind k),
-                   ("Con", p_con env c)]
-      | CRecordFailure (s1, s2) =>
-        eprefaces "Can't unify record constructors"
-        [("Summary 1", s1),
-         ("Summary 2", s2)]
-
 exception SynUnif = E.SynUnif
 
 open ElabOps
@@ -801,18 +717,29 @@
                        | _ => false
         val empty = (L'.CRecord (k, []), dummy)
 
+        fun unsummarize {fields, unifs, others} =
+            let
+                val c = (L'.CRecord (k, fields), loc)
+
+                val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
+                              c unifs
+            in
+                foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
+                      c others
+            end
+
         fun pairOffUnifs (unifs1, unifs2) =
             case (unifs1, unifs2) of
                 ([], _) =>
                 if clear then
                     List.app (fn (_, r) => r := SOME empty) unifs2
                 else
-                    raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
+                    raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
               | (_, []) =>
                 if clear then
                     List.app (fn (_, r) => r := SOME empty) unifs1
                 else
-                    raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
+                    raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
               | ((c1, _) :: rest1, (_, r2) :: rest2) =>
                 (r2 := SOME c1;
                  pairOffUnifs (rest1, rest2))
@@ -1027,77 +954,6 @@
     unifyCons' (env, denv) c1 c2
     handle CUnify' err => raise CUnify (c1, c2, err)
          | KUnify args => raise CUnify (c1, c2, CKind args)
-
-datatype exp_error =
-       UnboundExp of ErrorMsg.span * string
-     | UnboundStrInExp of ErrorMsg.span * string
-     | Unify of L'.exp * L'.con * L'.con * cunify_error
-     | Unif of string * L'.con
-     | WrongForm of string * L'.exp * L'.con
-     | IncompatibleCons of L'.con * L'.con
-     | DuplicatePatternVariable of ErrorMsg.span * string
-     | PatUnify of L'.pat * L'.con * L'.con * cunify_error
-     | UnboundConstructor of ErrorMsg.span * string list * string
-     | PatHasArg of ErrorMsg.span
-     | PatHasNoArg of ErrorMsg.span
-     | Inexhaustive of ErrorMsg.span
-     | DuplicatePatField of ErrorMsg.span * string
-     | Unresolvable of ErrorMsg.span * L'.con
-     | OutOfContext of ErrorMsg.span * (L'.exp * L'.con) option
-     | IllegalRec of string * L'.exp
-
-fun expError env err =
-    case err of
-        UnboundExp (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
-      | UnboundStrInExp (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound structure " ^ s)
-      | Unify (e, c1, c2, uerr) =>
-        (ErrorMsg.errorAt (#2 e) "Unification failure";
-         eprefaces' [("Expression", p_exp env e),
-                     ("Have con", p_con env c1),
-                     ("Need con", p_con env c2)];
-         cunifyError env uerr)
-      | Unif (action, c) =>
-        (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
-         eprefaces' [("Con", p_con env c)])
-      | WrongForm (variety, e, t) =>
-        (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
-         eprefaces' [("Expression", p_exp env e),
-                     ("Type", p_con env t)])
-      | IncompatibleCons (c1, c2) =>
-        (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
-         eprefaces' [("Con 1", p_con env c1),
-                     ("Con 2", p_con env c2)])
-      | DuplicatePatternVariable (loc, s) =>
-        ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
-      | PatUnify (p, c1, c2, uerr) =>
-        (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
-         eprefaces' [("Pattern", p_pat env p),
-                     ("Have con", p_con env c1),
-                     ("Need con", p_con env c2)];
-         cunifyError env uerr)
-      | UnboundConstructor (loc, ms, s) =>
-        ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
-      | PatHasArg loc =>
-        ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
-      | PatHasNoArg loc =>
-        ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
-      | Inexhaustive loc =>
-        ErrorMsg.errorAt loc "Inexhaustive 'case'"
-      | DuplicatePatField (loc, s) =>
-        ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
-      | OutOfContext (loc, co) =>
-        (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
-         Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
-                                              ("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)])
-      | IllegalRec (x, e) =>
-        (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
-         eprefaces' [("Variable", PD.string x),
-                     ("Expression", p_exp env e)])
          
 fun checkCon (env, denv) e c1 c2 =
     unifyCons (env, denv) c1 c2
@@ -1787,133 +1643,6 @@
                             ("|tcs|", PD.string (Int.toString (length tcs)))];*)
         r
     end
-            
-
-datatype decl_error =
-         KunifsRemain of L'.decl list
-       | CunifsRemain of L'.decl list
-       | Nonpositive of L'.decl
-
-fun lspan [] = ErrorMsg.dummySpan
-  | lspan ((_, loc) :: _) = loc
-
-fun declError env err =
-    case err of
-        KunifsRemain ds =>
-        (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
-         eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
-      | CunifsRemain ds =>
-        (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
-         eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
-      | Nonpositive d =>
-        (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
-         eprefaces' [("Decl", p_decl env d)])
-
-datatype sgn_error =
-         UnboundSgn of ErrorMsg.span * string
-       | UnmatchedSgi of L'.sgn_item
-       | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
-       | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
-       | SgiMismatchedDatatypes of L'.sgn_item * L'.sgn_item * (L'.con * L'.con * cunify_error) option
-       | SgnWrongForm of L'.sgn * L'.sgn
-       | UnWhereable of L'.sgn * string
-       | WhereWrongKind of L'.kind * L'.kind * kunify_error
-       | NotIncludable of L'.sgn
-       | DuplicateCon of ErrorMsg.span * string
-       | DuplicateVal of ErrorMsg.span * string
-       | DuplicateSgn of ErrorMsg.span * string
-       | DuplicateStr of ErrorMsg.span * string
-       | NotConstraintsable of L'.sgn
-
-fun sgnError env err =
-    case err of
-        UnboundSgn (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
-      | UnmatchedSgi (sgi as (_, loc)) =>
-        (ErrorMsg.errorAt loc "Unmatched signature item";
-         eprefaces' [("Item", p_sgn_item env sgi)])
-      | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
-        (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
-         eprefaces' [("Have", p_sgn_item env sgi1),
-                     ("Need", p_sgn_item env sgi2),
-                     ("Kind 1", p_kind k1),
-                     ("Kind 2", p_kind k2)];
-         kunifyError kerr)
-      | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
-        (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
-         eprefaces' [("Have", p_sgn_item env sgi1),
-                     ("Need", p_sgn_item env sgi2),
-                     ("Con 1", p_con env c1),
-                     ("Con 2", p_con env c2)];
-         cunifyError env cerr)
-      | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
-        (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
-         eprefaces' [("Have", p_sgn_item env sgi1),
-                     ("Need", p_sgn_item env sgi2)];
-         Option.app (fn (c1, c2, ue) =>
-                        (eprefaces "Unification error"
-                                   [("Con 1", p_con env c1),
-                                    ("Con 2", p_con env c2)];
-                         cunifyError env ue)) cerro)
-      | SgnWrongForm (sgn1, sgn2) =>
-        (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
-         eprefaces' [("Sig 1", p_sgn env sgn1),
-                     ("Sig 2", p_sgn env sgn2)])
-      | UnWhereable (sgn, x) =>
-        (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
-         eprefaces' [("Signature", p_sgn env sgn),
-                     ("Field", PD.string x)])
-      | WhereWrongKind (k1, k2, kerr) =>
-        (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
-         eprefaces' [("Have", p_kind k1),
-                     ("Need", p_kind k2)];
-         kunifyError kerr)
-      | NotIncludable sgn =>
-        (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
-         eprefaces' [("Signature", p_sgn env sgn)])
-      | DuplicateCon (loc, s) =>
-        ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
-      | DuplicateVal (loc, s) =>
-        ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
-      | DuplicateSgn (loc, s) =>
-        ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
-      | DuplicateStr (loc, s) =>
-        ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
-      | NotConstraintsable sgn =>
-        (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
-         eprefaces' [("Signature", p_sgn env sgn)])
-
-datatype str_error =
-         UnboundStr of ErrorMsg.span * string
-       | NotFunctor of L'.sgn
-       | FunctorRebind of ErrorMsg.span
-       | UnOpenable of L'.sgn
-       | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
-       | DuplicateConstructor of string * ErrorMsg.span
-       | NotDatatype of ErrorMsg.span
-
-fun strError env err =
-    case err of
-        UnboundStr (loc, s) =>
-        ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
-      | NotFunctor sgn =>
-        (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
-         eprefaces' [("Signature", p_sgn env sgn)])
-      | FunctorRebind loc =>
-        ErrorMsg.errorAt loc "Attempt to rebind functor"
-      | UnOpenable sgn =>
-        (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
-         eprefaces' [("Signature", p_sgn env sgn)])
-      | NotType (k, (k1, k2, ue)) =>
-        (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
-         eprefaces' [("Kind", p_kind k),
-                     ("Subkind 1", p_kind k1),
-                     ("Subkind 2", p_kind k2)];
-         kunifyError ue)
-      | DuplicateConstructor (x, loc) =>
-        ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
-      | NotDatatype loc =>
-        ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
 
 val hnormSgn = E.hnormSgn
 
@@ -3527,12 +3256,16 @@
         val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
         val () = case gs of
                      [] => ()
-                   | _ => (app (fn Disjoint (_, env, _, c1, c2) =>
-                                   prefaces "Unresolved"
-                                            [("c1", p_con env c1),
-                                             ("c2", p_con env c2)]
-                                 | TypeClass _ => TextIO.print "Type class\n") gs;
-                           raise Fail "Unresolved constraints in top.ur")
+                   | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
+                                  (case D.prove env denv (c1, c2, loc) of
+                                       [] => ()
+                                     | _ =>
+                                       (prefaces "Unresolved constraint in top.ur"
+                                                 [("loc", PD.string (ErrorMsg.spanToString loc)),
+                                                  ("c1", p_con env c1),
+                                                  ("c2", p_con env c2)];
+                                        raise Fail "Unresolve constraint in top.ur"))
+                                | TypeClass _ => raise Fail "Unresolved type class constraint in top.ur") gs
         val () = subSgn (env', D.empty) topSgn' topSgn
 
         val (env', top_n) = E.pushStrNamed env' "Top" topSgn
--- a/src/sources	Thu Sep 11 19:59:31 2008 -0400
+++ b/src/sources	Sat Sep 13 10:30:45 2008 -0400
@@ -41,6 +41,9 @@
 disjoint.sig
 disjoint.sml
 
+elab_err.sig
+elab_err.sml
+
 elaborate.sig
 elaborate.sml
 
--- a/src/urweb.grm	Thu Sep 11 19:59:31 2008 -0400
+++ b/src/urweb.grm	Sat Sep 13 10:30:45 2008 -0400
@@ -543,6 +543,13 @@
                                                 ((CAbs (SYMBOL, SOME kind, c), loc),
                                                  (KArrow (kind, k), loc))
                                             end)
+       | UNDER DCOLON kind              (fn (c, k) =>
+                                            let
+                                                val loc = s (UNDERleft, kindright)
+                                            in
+                                                ((CAbs ("_", SOME kind, c), loc),
+                                                 (KArrow (kind, k), loc))
+                                            end)
        | cargp                          (cargp)
 
 cargp  : SYMBOL                         (fn (c, k) =>
@@ -552,6 +559,13 @@
                                                 ((CAbs (SYMBOL, NONE, c), loc),
                                                  (KArrow ((KWild, loc), k), loc))
                                             end)
+       | UNDER                          (fn (c, k) =>
+                                            let
+                                                val loc = s (UNDERleft, UNDERright)
+                                            in
+                                                ((CAbs ("_", NONE, c), loc),
+                                                 (KArrow ((KWild, loc), k), loc))
+                                            end)
        | LPAREN SYMBOL DCOLON kind RPAREN (fn (c, k) =>
                                               let
                                                   val loc = s (LPARENleft, RPARENright)
--- a/tests/crud.ur	Thu Sep 11 19:59:31 2008 -0400
+++ b/tests/crud.ur	Sat Sep 13 10:30:45 2008 -0400
@@ -1,4 +1,5 @@
-con colMeta = fn cols :: {Type} => $(Top.mapTT (fn t => {Show : t -> xbody}) cols)
+con colMeta' = fn t :: Type => {Show : t -> xbody}
+con colMeta = fn cols :: {Type} => $(Top.mapTT colMeta' cols)
 
 functor Make(M : sig
         con cols :: {Type}
@@ -15,19 +16,19 @@
 
 fun list () =
         rows <- query (SELECT * FROM tab AS T)
-                (fn fs acc => return <body>
+                (fn (fs : {T : $([Id = int] ++ M.cols)}) acc => return <body>
                         {acc}
                         <tr>
                                 <td>{txt _ fs.T.Id}</td>
-                                {fold [fn cols :: {Type} => $cols -> colMeta cols -> xtr]
-                                        (fn (nm :: Name) (t :: Type) (rest :: {Type}) acc =>
+                                {foldTR2 [idT] [colMeta'] [fn _ => xtr]
+                                        (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
                                                 [[nm] ~ rest] =>
-                                                fn r cols =>
+                                                fn v funcs acc =>
                                                 <tr>
-                                                        <td>{cols.nm.Show r.nm}</td>
-                                                        {acc (r -- nm) (cols -- nm)}
+                                                        <td>{funcs.Show v}</td>
+                                                        {acc}
                                                 </tr>)
-                                        (fn _ _ => <tr></tr>)
+                                        <tr></tr>
                                         [M.cols] (fs.T -- #Id) M.cols}
                         </tr>
                 </body>) <body></body>;
--- a/tests/crud.urs	Thu Sep 11 19:59:31 2008 -0400
+++ b/tests/crud.urs	Sat Sep 13 10:30:45 2008 -0400
@@ -1,4 +1,5 @@
-con colMeta = fn cols :: {Type} => $(mapTT (fn t => {Show : t -> xbody}) cols)
+con colMeta' = fn t :: Type => {Show : t -> xbody}
+con colMeta = fn cols :: {Type} => $(Top.mapTT colMeta' cols)
 
 functor Make(M : sig
         con cols :: {Type}