From 31e82db1a6d6d448fa783a9829afacf7af6a03ba Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 21 Oct 2008 19:56:20 -0400
Subject: Sum prose

---
 src/elab_err.sig  | 2 +-
 src/elab_err.sml  | 6 +++---
 src/elaborate.sml | 8 ++++----
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/elab_err.sig b/src/elab_err.sig
index 1fd234b7..d757572f 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -49,7 +49,7 @@ signature ELAB_ERR = sig
            | COccursCheckFailed of Elab.con * Elab.con
            | CIncompatible of Elab.con * Elab.con
            | CExplicitness of Elab.con * Elab.con
-           | CKindof of Elab.kind * Elab.con
+           | CKindof of Elab.kind * Elab.con * string
            | CRecordFailure of Elab.con * Elab.con
 
     val cunifyError : ElabEnv.env -> cunify_error -> unit
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 8131633c..e8d7ff68 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -109,7 +109,7 @@ datatype cunify_error =
        | COccursCheckFailed of con * con
        | CIncompatible of con * con
        | CExplicitness of con * con
-       | CKindof of kind * con
+       | CKindof of kind * con * string
        | CRecordFailure of con * con
 
 fun cunifyError env err =
@@ -131,8 +131,8 @@ fun cunifyError env err =
         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"
+      | CKindof (k, c, expected) =>
+        eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
                   [("Kind", p_kind k),
                    ("Con", p_con env c)]
       | CRecordFailure (c1, c2) =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index aa48952c..6e23c760 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -481,7 +481,7 @@
          (case hnormKind (kindof env c) of
               (L'.KArrow (_, k), _) => k
             | (L'.KError, _) => kerror
-            | k => raise CUnify' (CKindof (k, c)))
+            | k => raise CUnify' (CKindof (k, c, "arrow")))
        | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
        | L'.CDisjoint (_, _, _, c) => kindof env c
 
@@ -497,7 +497,7 @@
        | L'.CProj (c, n) =>
          (case hnormKind (kindof env c) of
               (L'.KTuple ks, _) => List.nth (ks, n - 1)
-            | k => raise CUnify' (CKindof (k, c)))
+            | k => raise CUnify' (CKindof (k, c, "tuple")))
 
        | L'.CError => kerror
        | L'.CUnif (_, k, _, _) => k
@@ -546,7 +546,7 @@
              case hnormKind (kindof env c) of
                  (L'.KRecord k, _) => k
                | (L'.KError, _) => kerror
-               | k => raise CUnify' (CKindof (k, c))
+               | k => raise CUnify' (CKindof (k, c, "record"))
 
          val k1 = rkindof c1
          val k2 = rkindof c2
@@ -2318,7 +2318,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                                      val env = if n1 = n2 then
                                                                    env
                                                                else
-                                                                   E.pushCNamedAs env x n1 (L'.KType, loc)
+                                                                   E.pushCNamedAs env x n1 k'
                                                                                   (SOME (L'.CNamed n2, loc))
                                                  in
                                                      SOME (env, denv)
-- 
cgit v1.2.3