Harmonize have/need terminology in error messages; display canceled record summaries on errors

3 files changed, 34 insertions, 13 deletions

diff --git a/src/elab_err.sml b/src/elab_err.sml
index 1194f817..00f1e4fc 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -127,29 +127,29 @@ fun cunifyError env err =
     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 @@ fun expError env err =
                      ("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 --git a/src/elaborate.sml b/src/elaborate.sml
index f331d813..89accb26 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -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 @@ fun elabFile basis topStr topSgn env file =
             (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 --git a/tests/cancel.ur b/tests/cancel.ur
new file mode 100644
index 00000000..9edb15af
--- /dev/null
+++ b/tests/cancel.ur
@@ -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