summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-10-27 08:36:31 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-10-27 08:36:31 -0400
commit4b4b367f011e9f49389d76c2167c193711713438 (patch)
treefbff54b6d2e52247b2f2b1003d6265e32f18c57e
parent3c6dc3613a00da2f302ed3e8a295438eedd3e649 (diff)
Harmonize have/need terminology in error messages; display canceled record summaries on errors
-rw-r--r--src/elab_err.sml24
-rw-r--r--src/elaborate.sml16
-rw-r--r--tests/cancel.ur7
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