From 7711c829190f80e32de4d3b45ce39245dba07435 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 18 Dec 2011 11:29:13 -0500
Subject: Add a new scoping check for unification variables, to fix a type
 inference bug

---
 src/elab_err.sml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'src/elab_err.sml')

diff --git a/src/elab_err.sml b/src/elab_err.sml
index 84c8c61f..2bf059e6 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -63,6 +63,7 @@ fun kindError env err =
 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 @@ fun kunifyError env err =
         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 @@ datatype cunify_error =
        | 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 @@ fun cunifyError env err =
          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
-- 
cgit v1.2.3