diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2011-10-27 08:36:31 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2011-10-27 08:36:31 -0400 |
| commit | 4b4b367f011e9f49389d76c2167c193711713438 (patch) | |
| tree | fbff54b6d2e52247b2f2b1003d6265e32f18c57e /src/elaborate.sml | |
| parent | 3c6dc3613a00da2f302ed3e8a295438eedd3e649 (diff) | |
Harmonize have/need terminology in error messages; display canceled record summaries on errors
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 16 |
1 files changed, 15 insertions, 1 deletions
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 := []); |