Mercurial > urweb

diff src/elab_err.sml @ 1639:6c00d8af6239

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents c37d8341940a
children d6c45026240d
line wrap: on
line diff
--- a/src/elab_err.sml	Sat Dec 17 20:42:39 2011 -0500
+++ b/src/elab_err.sml	Sun Dec 18 11:29:13 2011 -0500
@@ -63,6 +63,7 @@
 datatype kunify_error =
          KOccursCheckFailed of kind * kind
        | KIncompatible of kind * kind
+       | KScope of kind * kind
 
 fun kunifyError env err =
     case err of
@@ -74,7 +75,10 @@
         eprefaces "Incompatible kinds"
         [("Kind 1", p_kind env k1),
          ("Kind 2", p_kind env k2)]
-
+      | KScope (k1, k2) =>
+        eprefaces "Scoping prevents kind unification"
+        [("Kind 1", p_kind env k1),
+         ("Kind 2", p_kind env k2)]
 
 fun p_con env c = P.p_con env (simplCon env c)
 
@@ -122,6 +126,7 @@
        | TooLifty of ErrorMsg.span * ErrorMsg.span
        | TooUnify of con * con
        | TooDeep
+       | CScope of con * con
 
 fun cunifyError env err =
     case err of
@@ -167,6 +172,10 @@
          eprefaces' [("Replacement", p_con env c1),
                      ("Body", p_con env c2)])
       | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
+      | CScope (c1, c2) =>
+        eprefaces "Scoping prevents constructor unification"
+                  [("Have", p_con env c1),
+                   ("Need", p_con env c2)]
 
 datatype exp_error =
        UnboundExp of ErrorMsg.span * string