# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1319718991 14400
# Node ID dfb38a333816c0c9ced29ff53f4ca40fa8fc838a
# Parent  1ced338f691a7e1af162ea8437fb8272f22f0188
Harmonize have/need terminology in error messages; display canceled record summaries on errors

diff -r 1ced338f691a -r dfb38a333816 src/elab_err.sml
--- a/src/elab_err.sml	Wed Oct 26 09:10:40 2011 -0400
+++ b/src/elab_err.sml	Thu Oct 27 08:36:31 2011 -0400
@@ -127,29 +127,29 @@
     case err of
         CKind (k1, k2, kerr) =>
         (eprefaces "Kind unification failure"
-                   [("Kind 1", p_kind env k1),
-                    ("Kind 2", p_kind env k2)];
+                   [("Have", p_kind env k1),
+                    ("Need", p_kind env k2)];
          kunifyError env kerr)
       | COccursCheckFailed (c1, c2) =>
         eprefaces "Constructor occurs check failed"
-                  [("Con 1", p_con env c1),
-                   ("Con 2", p_con env c2)]
+                  [("Have", p_con env c1),
+                   ("Need", p_con env c2)]
       | CIncompatible (c1, c2) =>
         eprefaces "Incompatible constructors"
-                  [("Con 1", p_con env c1),
-                   ("Con 2", p_con env c2)]
+                  [("Have", p_con env c1),
+                   ("Need", p_con env c2)]
       | CExplicitness (c1, c2) =>
         eprefaces "Differing constructor function explicitness"
-                  [("Con 1", p_con env c1),
-                   ("Con 2", p_con env c2)]
+                  [("Have", p_con env c1),
+                   ("Need", p_con env c2)]
       | CKindof (k, c, expected) =>
         eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
                   [("Kind", p_kind env k),
                    ("Con", p_con env c)]
       | CRecordFailure (c1, c2, fo) =>
         (eprefaces "Can't unify record constructors"
-                   (("Summary 1", p_con env c1)
-                    :: ("Summary 2", p_con env c2)
+                   (("Have", p_con env c1)
+                    :: ("Need", p_con env c2)
                     :: (case fo of
                             NONE => []
                           | SOME (nm, t1, t2, _) =>
@@ -210,8 +210,8 @@
                      ("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)])
+         eprefaces' [("Have", p_con env c1),
+                     ("Need", p_con env c2)])
       | DuplicatePatternVariable (loc, s) =>
         ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
       | PatUnify (p, c1, c2, uerr) =>
diff -r 1ced338f691a -r dfb38a333816 src/elaborate.sml
--- a/src/elaborate.sml	Wed Oct 26 09:10:40 2011 -0400
+++ b/src/elaborate.sml	Thu Oct 27 08:36:31 2011 -0400
@@ -698,6 +698,8 @@
                  bind = fn (bound, U.Con.RelC _) => bound + 1
                          | (bound, _) => bound} 0
 
+ val reducedSummaries = ref (NONE : (Print.PD.pp_desc * Print.PD.pp_desc) option)
+
  fun unifyRecordCons env (loc, c1, c2) =
      let
          fun rkindof c =
@@ -891,6 +893,12 @@
                       (fs1, fs2, others1, others2, unifs1, unifs2)
                | _ => (fs1, fs2, others1, others2, unifs1, unifs2)
 
+         val () = if !mayDelay then
+                      ()
+                  else
+                      reducedSummaries := SOME (p_summary env {fields = fs1, unifs = unifs1, others = others1},
+                                                p_summary env {fields = fs2, unifs = unifs2, others = others2})
+
          (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
                                           ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
 
@@ -4450,7 +4458,13 @@
             (app (fn (loc, env, k, s1, s2) =>
                      unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
                      handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification";
-                                            cunifyError env err))
+                                            cunifyError env err;
+                                            case !reducedSummaries of
+                                                NONE => ()
+                                              | SOME (s1, s2) =>
+                                                (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:";
+                                                 eprefaces' [("Have", s1),
+                                                             ("Need", s2)])))
                  (!delayedUnifs);
              delayedUnifs := []);
 
diff -r 1ced338f691a -r dfb38a333816 tests/cancel.ur
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/cancel.ur	Thu Oct 27 08:36:31 2011 -0400
@@ -0,0 +1,7 @@
+type t = {A : int, B : float, C : string}
+type u = {A : int, C : string, D : bool}
+
+fun f (x : t) = x
+fun g (x : u) = f x
+
+fun h [ts] [ts ~ [A]] (r : $([A = int] ++ ts)) : $([A = int, B = float] ++ ts) = r