Better subSgn error locations

3 files changed, 46 insertions, 39 deletions

diff --git a/src/elab_err.sig b/src/elab_err.sig
index 10cda7d3..18596d04 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -88,11 +88,12 @@ signature ELAB_ERR = sig
 
     datatype sgn_error =
              UnboundSgn of ErrorMsg.span * string
-           | UnmatchedSgi of Elab.sgn_item
-           | SgiWrongKind of Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
-           | SgiWrongCon of Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
-           | SgiMismatchedDatatypes of Elab.sgn_item * Elab.sgn_item * (Elab.con * Elab.con * cunify_error) option
-           | SgnWrongForm of Elab.sgn * Elab.sgn
+           | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
+           | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
+           | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
+           | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
+                                       * (Elab.con * Elab.con * cunify_error) option
+           | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
            | UnWhereable of Elab.sgn * string
            | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
            | NotIncludable of Elab.sgn
diff --git a/src/elab_err.sml b/src/elab_err.sml
index dc34560b..6d9bd2e6 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -259,11 +259,12 @@ fun declError env err =
 
 datatype sgn_error =
          UnboundSgn of ErrorMsg.span * string
-       | UnmatchedSgi of sgn_item
-       | SgiWrongKind of sgn_item * kind * sgn_item * kind * kunify_error
-       | SgiWrongCon of sgn_item * con * sgn_item * con * cunify_error
-       | SgiMismatchedDatatypes of sgn_item * sgn_item * (con * con * cunify_error) option
-       | SgnWrongForm of sgn * sgn
+       | UnmatchedSgi of ErrorMsg.span * sgn_item
+       | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * kunify_error
+       | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * cunify_error
+       | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
+                                   * (con * con * cunify_error) option
+       | SgnWrongForm of ErrorMsg.span * sgn * sgn
        | UnWhereable of sgn * string
        | WhereWrongKind of kind * kind * kunify_error
        | NotIncludable of sgn
@@ -280,25 +281,25 @@ fun sgnError env err =
     case err of
         UnboundSgn (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
-      | UnmatchedSgi (sgi as (_, loc)) =>
+      | UnmatchedSgi (loc, sgi) =>
         (ErrorMsg.errorAt loc "Unmatched signature item";
          eprefaces' [("Item", p_sgn_item env sgi)])
-      | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
-        (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
+      | SgiWrongKind (loc, sgi1, k1, sgi2, k2, kerr) =>
+        (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
          eprefaces' [("Have", p_sgn_item env sgi1),
                      ("Need", p_sgn_item env sgi2),
                      ("Kind 1", p_kind env k1),
                      ("Kind 2", p_kind env k2)];
          kunifyError env kerr)
-      | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
-        (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
+      | SgiWrongCon (loc, sgi1, c1, sgi2, c2, cerr) =>
+        (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
          eprefaces' [("Have", p_sgn_item env sgi1),
                      ("Need", p_sgn_item env sgi2),
                      ("Con 1", p_con env c1),
                      ("Con 2", p_con env c2)];
          cunifyError env cerr)
-      | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
-        (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
+      | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
+        (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
          eprefaces' [("Have", p_sgn_item env sgi1),
                      ("Need", p_sgn_item env sgi2)];
          Option.app (fn (c1, c2, ue) =>
@@ -306,8 +307,8 @@ fun sgnError env err =
                                    [("Con 1", p_con env c1),
                                     ("Con 2", p_con env c2)];
                          cunifyError env ue)) cerro)
-      | SgnWrongForm (sgn1, sgn2) =>
-        (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
+      | SgnWrongForm (loc, sgn1, sgn2) =>
+        (ErrorMsg.errorAt loc "Incompatible signatures:";
          eprefaces' [("Sig 1", p_sgn env sgn1),
                      ("Sig 2", p_sgn env sgn2)])
       | UnWhereable (sgn, x) =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9aeac8f3..b46c262e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2516,7 +2516,7 @@ and sgiOfDecl (d, loc) =
       | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
       | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
 
-and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
+and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
     ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
                         ("sgn2", p_sgn env sgn2)];*)
     case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
@@ -2575,7 +2575,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                             seek env sgis1
                         end
 
-                    val seek = seek' (fn env => (sgnError env (UnmatchedSgi sgi2All);
+                    val seek = seek' (fn env => (sgnError env (UnmatchedSgi (strLoc, sgi2All));
                                                  env))
                 in
                     case sgi of
@@ -2587,7 +2587,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                              let
                                                  val () = unifyKinds env k1 k2
                                                      handle KUnify (k1, k2, err) =>
-                                                            sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+                                                            sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
+                                                                                        sgi2All, k2, err))
                                                  val env = E.pushCNamedAs env x n1 k1 co1
                                              in
                                                  SOME (if n1 = n2 then
@@ -2655,7 +2656,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                                  (unifyCons env loc c1 c2;
                                                   good ())
                                                  handle CUnify (c1, c2, err) =>
-                                                        (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                        (sgnError env (SgiWrongCon (strLoc, sgi1All, c1,
+                                                                                    sgi2All, c2, err));
                                                          good ())
                                              end
                                          else
@@ -2675,7 +2677,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                 else
                                     let
                                         fun mismatched ue =
-                                            (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
+                                            (sgnError env (SgiMismatchedDatatypes (strLoc, sgi1All, sgi2All, ue));
                                              SOME env)
 
                                         val k = (L'.KType, loc)
@@ -2780,7 +2782,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                              (unifyCons env loc t1 t2;
                                               good ())
                                              handle CUnify (c1, c2, err) =>
-                                                    (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                    (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err));
                                                      good ())
                                          end
                                      else
@@ -2801,7 +2803,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                           unifyCons env loc c1 (sub2 c2);
                                           SOME env)
                                          handle CUnify (c1, c2, err) =>
-                                                (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err));
                                                  SOME env)
                                      else
                                          NONE
@@ -2813,7 +2815,7 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                      L'.SgiStr (x', n1, sgn1) =>
                                      if x = x' then
                                          let
-                                             val () = subSgn' counterparts env sgn1 sgn2
+                                             val () = subSgn' counterparts env strLoc sgn1 sgn2
                                              val env = E.pushStrNamedAs env x n1 sgn1
                                              val env = if n1 = n2 then
                                                            env
@@ -2834,8 +2836,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                      L'.SgiSgn (x', n1, sgn1) =>
                                      if x = x' then
                                          let
-                                             val () = subSgn' counterparts env sgn1 sgn2
-                                             val () = subSgn' counterparts env sgn2 sgn1
+                                             val () = subSgn' counterparts env strLoc sgn1 sgn2
+                                             val () = subSgn' counterparts env strLoc sgn2 sgn1
 
                                              val env = E.pushSgnNamedAs env x n2 sgn2
                                              val env = if n1 = n2 then
@@ -2869,7 +2871,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                              let
                                                  val () = unifyKinds env k1 k2
                                                      handle KUnify (k1, k2, err) =>
-                                                            sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+                                                            sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
+                                                                                        sgi2All, k2, err))
 
                                                  val env = E.pushCNamedAs env x n1 k1 co
                                              in
@@ -2895,7 +2898,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                              let
                                                  val () = unifyKinds env k1 k2
                                                      handle KUnify (k1, k2, err) =>
-                                                            sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
+                                                            sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
+                                                                                        sgi2All, k2, err))
 
                                                  val c2 = sub2 c2
 
@@ -2914,7 +2918,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                                  (unifyCons env loc c1 c2;
                                                   good ())
                                                  handle CUnify (c1, c2, err) =>
-                                                        (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                        (sgnError env (SgiWrongCon (strLoc, sgi1All, c1,
+                                                                                    sgi2All, c2, err));
                                                          good ())
                                              end
                                          else
@@ -2937,11 +2942,11 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                 else
                     subStrInSgn (n2, n1) ran2
         in
-            subSgn' counterparts env dom2 dom1;
-            subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2
+            subSgn' counterparts env strLoc dom2 dom1;
+            subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) strLoc ran1 ran2
         end
 
-      | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
+      | _ => sgnError env (SgnWrongForm (strLoc, sgn1, sgn2)))
 
 and subSgn env = subSgn' (ref IM.empty) env
 
@@ -3405,7 +3410,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                                 val str = wildifyStr env (str, formal)
                                 val (str', actual, gs2) = elabStr (env, denv) str
                             in
-                                subSgn env (selfifyAt env {str = str', sgn = actual}) formal;
+                                subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal;
                                 (str', formal, enD gs1 @ gs2)
                             end
 
@@ -3786,7 +3791,7 @@ and elabStr (env, denv) (str, loc) =
                     let
                         val (ran', gs) = elabSgn (env', denv') ran
                     in
-                        subSgn env' actual ran';
+                        subSgn env' loc actual ran';
                         (ran', gs)
                     end
         in
@@ -3807,7 +3812,7 @@ and elabStr (env, denv) (str, loc) =
             case #1 (hnormSgn env sgn1) of
                 L'.SgnError => (strerror, sgnerror, [])
               | L'.SgnFun (m, n, dom, ran) =>
-                (subSgn env sgn2 dom;
+                (subSgn env loc sgn2 dom;
                  case #1 (hnormSgn env ran) of
                      L'.SgnError => (strerror, sgnerror, [])
                    | L'.SgnConst sgis =>
@@ -3878,7 +3883,7 @@ fun elabFile basis topStr topSgn env file =
                                         | NONE => expError env (Unresolvable (loc, c))
                                   end) gs
 
-        val () = subSgn env' topSgn' topSgn
+        val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn
 
         val (env', top_n) = E.pushStrNamed env' "Top" topSgn
         val () = top_r := top_n