diff src/elaborate.sml @ 1582:dfb38a333816

Harmonize have/need terminology in error messages; display canceled record summaries on errors
author Adam Chlipala <adam@chlipala.net>
date Thu, 27 Oct 2011 08:36:31 -0400
parents ec466c1e082a
children 7fcdf836b761
line wrap: on
line diff
--- 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 := []);