Change error message display order: only show disjointness/type class failures if all record unifications succeeded

1 files changed, 37 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