diff options
| -rw-r--r-- | src/elab_err.sml | 24 | ||||
| -rw-r--r-- | src/elaborate.sml | 16 | ||||
| -rw-r--r-- | tests/cancel.ur | 7 |
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 |