summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-10-15 10:31:30 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-10-15 10:31:30 -0400
commit27b7ae9ca08e4675341166928806f66623132ae2 (patch)
tree4b2d4d39aece6815b4c87f6e46503d6f5721c6f1
parent8a2f6e7bf923bc145cb85a5ed5cc34daa0f7d664 (diff)
Change error message display order: only show disjointness/type class failures if all record unifications succeeded
-rw-r--r--src/elaborate.sml73
-rw-r--r--tests/nopoly.ur2
2 files changed, 39 insertions, 36 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 4d6d4658..1473613c 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4335,6 +4335,8 @@ fun elabFile basis topStr topSgn env file =
unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
delayed
end
+
+ val checkConstraintErrors = ref (fn () => ())
in
oneSummaryRound ();
@@ -4404,42 +4406,36 @@ fun elabFile basis topStr topSgn env file =
([], _) => ()
| (_, true) => (oneSummaryRound (); solver gs)
| _ =>
- app (fn Disjoint (loc, env, denv, c1, c2) =>
- let
- val c1' = ElabOps.hnormCon env c1
- val c2' = ElabOps.hnormCon env c2
-
- fun isUnif (c, _) =
- case c of
- L'.CUnif _ => true
- | _ => false
-
- fun maybeAttr (c, _) =
- case c of
- L'.CRecord ((L'.KType, _), xts) => true
- | _ => false
- in
- ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
- eprefaces' [("Con 1", p_con env c1),
- ("Con 2", p_con env c2),
- ("Hnormed 1", p_con env c1'),
- ("Hnormed 2", p_con env c2')];
-
- (*app (fn (loc, env, k, s1, s2) =>
- eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
- ("s2", p_summary env (normalizeRecordSummary env s2))])
- (!delayedUnifs);*)
-
- if (isUnif c1' andalso maybeAttr c2')
- orelse (isUnif c2' andalso maybeAttr c1') then
- TextIO.output (TextIO.stdErr,
- "You may be using a disallowed attribute with an HTML tag.\n")
- else
- ()
- end
- | TypeClass (env, c, r, loc) =>
- expError env (Unresolvable (loc, c)))
- gs
+ checkConstraintErrors :=
+ (fn () => app (fn Disjoint (loc, env, denv, c1, c2) =>
+ let
+ val c1' = ElabOps.hnormCon env c1
+ val c2' = ElabOps.hnormCon env c2
+
+ fun isUnif (c, _) =
+ case c of
+ L'.CUnif _ => true
+ | _ => false
+
+ fun maybeAttr (c, _) =
+ case c of
+ L'.CRecord ((L'.KType, _), xts) => true
+ | _ => false
+ in
+ ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
+ eprefaces' [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2),
+ ("Hnormed 1", p_con env c1'),
+ ("Hnormed 2", p_con env c2')]
+
+ (*app (fn (loc, env, k, s1, s2) =>
+ eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
+ ("s2", p_summary env (normalizeRecordSummary env s2))])
+ (!delayedUnifs);*)
+ end
+ | TypeClass (env, c, r, loc) =>
+ expError env (Unresolvable (loc, c)))
+ gs)
end
in
solver gs
@@ -4483,6 +4479,11 @@ fun elabFile basis topStr topSgn env file =
| SOME p => expError env (Inexhaustive (loc, p)))
(!delayedExhaustives);
+ if ErrorMsg.anyErrors () then
+ ()
+ else
+ !checkConstraintErrors ();
+
(*preface ("file", p_file env' file);*)
if !dumpTypes then
diff --git a/tests/nopoly.ur b/tests/nopoly.ur
new file mode 100644
index 00000000..687403aa
--- /dev/null
+++ b/tests/nopoly.ur
@@ -0,0 +1,2 @@
+fun x y = y.Hellodsad
+val bar = x {Hello = 1, RightO = 2}