Shorter, more focused error messages about undetermined unification variables

4 files changed, 98 insertions, 19 deletions

diff --git a/src/elab_err.sml b/src/elab_err.sml
index 00f1e4fc..84c8c61f 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -262,7 +262,55 @@ datatype decl_error =
 fun lspan [] = ErrorMsg.dummySpan
   | lspan ((_, loc) :: _) = loc
 
-val p_decl = P.p_decl
+val baseLen = 2000
+
+fun p_decl env d =
+    let
+        val fname = OS.FileSys.tmpName ()
+        val out' = TextIO.openOut fname
+        val out = Print.openOut {dst = out', wid = 80}
+
+        fun readFromFile () =
+            let
+                val inf = TextIO.openIn fname
+
+                fun loop acc =
+                    case TextIO.inputLine inf of
+                        NONE => String.concat (rev acc)
+                      | SOME line => loop (line :: acc)
+            in
+                loop []
+                before TextIO.closeIn inf
+            end
+    in
+        Print.fprint out (P.p_decl env d);
+        TextIO.closeOut out';
+        let
+            val content = readFromFile ()
+        in
+            OS.FileSys.remove fname;
+            Print.PD.string (if size content <= baseLen then
+                                 content
+                             else
+                                 let
+                                     val (befor, after) = Substring.position "<UNIF:" (Substring.full content)
+                                 in
+                                     if Substring.isEmpty after then
+                                         raise Fail "No unification variables in rendering"
+                                     else
+                                         Substring.concat [Substring.full "\n.....\n",
+                                                           if Substring.size befor <= baseLen then
+                                                               befor
+                                                           else
+                                                               Substring.slice (befor, Substring.size befor - baseLen, SOME baseLen),
+                                                           if Substring.size after <= baseLen then
+                                                               after
+                                                           else
+                                                               Substring.slice (after, 0, SOME baseLen),
+                                                           Substring.full "\n.....\n"]
+                                 end)
+        end
+    end
 
 fun declError env err =
     case err of
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 88bdc892..2998e7db 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -226,6 +226,8 @@ end
 
 structure File : sig
     val maxName : Elab.file -> int
+
+    val findDecl : (Elab.decl -> bool) -> Elab.file -> Elab.decl option
 end
 
 end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index fd8163c2..bf0185b1 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -1235,6 +1235,32 @@ and maxNameSgi (sgi, _) =
       | SgiConstraint _ => 0
       | SgiClassAbs (_, n, _) => n
       | SgiClass (_, n, _, _) => n
+
+fun findDecl pred file =
+    let
+        fun decl d =
+            let
+                val r = case #1 d of
+                            DStr (_, _, _, s) => str s
+                          | _ => NONE
+            in
+                case r of
+                    NONE => if pred d then SOME d else NONE
+                  | _ => r
+            end
+
+        and str s =
+            case #1 s of
+                StrConst ds => ListUtil.search decl ds
+              | StrFun (_, _, _, _, s) => str s
+              | StrApp (s1, s2) =>
+                (case str s1 of
+                     NONE => str s2
+                   | r => r)
+              | _ => NONE
+    in
+        ListUtil.search decl file
+    end
               
 end
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5b54db9a..9051299a 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -500,9 +500,9 @@
      case c of
          L'.CUnif (_, loc, k, _, r as ref NONE) =>
          (case #1 (hnormKind k) of
-              L'.KUnit => (r := SOME (L'.CUnit, loc); NONE)
-            | _ => SOME loc)
-       | _ => NONE
+              L'.KUnit => (r := SOME (L'.CUnit, loc); false)
+            | _ => true)
+       | _ => false
 
  val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
                                    con = fn _ => false,
@@ -512,13 +512,13 @@
                                    str = fn _ => false,
                                    decl = fn _ => false}
 
- val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
+ val cunifsInDecl = U.Decl.exists {kind = fn _ => false,
                                    con = cunifsRemain,
-                                   exp = fn _ => NONE,
-                                   sgn_item = fn _ => NONE,
-                                   sgn = fn _ => NONE,
-                                   str = fn _ => NONE,
-                                   decl = fn _ => NONE}
+                                   exp = fn _ => false,
+                                   sgn_item = fn _ => false,
+                                   sgn = fn _ => false,
+                                   str = fn _ => false,
+                                   decl = fn _ => false}
 
  fun occursCon r =
      U.Con.exists {kind = fn _ => false,
@@ -4473,19 +4473,22 @@ fun elabFile basis topStr topSgn env file =
         if ErrorMsg.anyErrors () then
             ()
         else
-            ignore (List.exists (fn d => if kunifsInDecl d then
-                                             (declError env'' (KunifsRemain [d]);
-                                              true)
-                                         else
-                                             false) file);
+            if List.exists kunifsInDecl file then
+                case U.File.findDecl kunifsInDecl file of
+                    NONE => ()
+                  | SOME d => declError env'' (KunifsRemain [d])
+            else
+                ();
         
         if ErrorMsg.anyErrors () then
             ()
         else
-            ignore (List.exists (fn d => case cunifsInDecl d of
-                                             NONE => false
-                                           | SOME _ => (declError env'' (CunifsRemain [d]);
-                                                        true)) file);
+            if List.exists cunifsInDecl file then
+                case U.File.findDecl cunifsInDecl file of
+                    NONE => ()
+                  | SOME d => declError env'' (CunifsRemain [d])
+            else
+                ();
 
         if ErrorMsg.anyErrors () then
             ()