# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1335100125 14400
# Node ID 5ecf67553da8a74b32120ddaa9693085910022e9
# Parent  f7d9dc5d57eb515f5d7565ccb08e678d53d17783
-unifyMore

diff -r f7d9dc5d57eb -r 5ecf67553da8 doc/manual.tex
--- a/doc/manual.tex	Sat Apr 21 15:47:02 2012 -0400
+++ b/doc/manual.tex	Sun Apr 22 09:08:45 2012 -0400
@@ -202,6 +202,8 @@
 
 A related option is \cd{-dumpTypes}, which, as long as parsing succeeds, outputs to stdout a summary of the kinds of all identifiers declared with \cd{con} and the types of all identifiers declared with \cd{val} or \cd{val rec}.  This information is dumped even if there are errors during type inference.  Compiler error messages go to stderr, not stdout, so it is easy to distinguish the two kinds of output programmatically.
 
+It may be useful to combine another option \cd{-unifyMore} with \cd{-dumpTypes}.  Ur/Web type inference proceeds in a series of stages, where the first is standard Hindley-Milner type inference as in ML, and the later phases add more complex aspects.  By default, an error detected in one phase cuts off the execution of later phases.  However, the later phases might still determine more values of unification variables.  These value choices might be ``misguided,'' since earlier phases have not come up with reasonable types at a coarser detail level; but the unification decisions may still be useful for debugging and program understanding.  So, if a run with \cd{-dumpTypes} leaves unification variables undetermined in positions where you would like to see best-effort guesses instead, consider \cd{-unifyMore}.  Note that \cd{-unifyMore} has no effect when type inference succeeds fully, but it may lead to many more error messages when inference fails.
+
 To output information relevant to CSS stylesheets (and not finish regular compilation), run
 \begin{verbatim}
 urweb -css P
diff -r f7d9dc5d57eb -r 5ecf67553da8 src/elaborate.sig
--- a/src/elaborate.sig	Sat Apr 21 15:47:02 2012 -0400
+++ b/src/elaborate.sig	Sun Apr 22 09:08:45 2012 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008, 2012, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -36,4 +36,8 @@
     (* After elaboration (successful or failed), should I output a mapping from
      * all identifiers to their kinds/types? *)
 
+    val unifyMore : bool ref
+    (* Run all phases of type inference, even if an error is detected by an
+     * early phase. *)
+
 end
diff -r f7d9dc5d57eb -r 5ecf67553da8 src/elaborate.sml
--- a/src/elaborate.sml	Sat Apr 21 15:47:02 2012 -0400
+++ b/src/elaborate.sml	Sun Apr 22 09:08:45 2012 -0400
@@ -39,6 +39,7 @@
  open ElabErr
 
  val dumpTypes = ref false
+ val unifyMore = ref false
 
  structure IS = IntBinarySet
  structure IM = IntBinaryMap
@@ -4519,10 +4520,11 @@
                 end
 
         val checkConstraintErrors = ref (fn () => ())
+        fun stopHere () = not (!unifyMore) andalso ErrorMsg.anyErrors ()
     in
         oneSummaryRound ();
 
-        if ErrorMsg.anyErrors () then
+        if stopHere () then
             ()
         else
             let
@@ -4625,7 +4627,7 @@
 
         mayDelay := false;
 
-        if ErrorMsg.anyErrors () then
+        if stopHere () then
             ()
         else
             (app (fn (loc, env, k, s1, s2) =>
@@ -4641,7 +4643,7 @@
                  (!delayedUnifs);
              delayedUnifs := []);
 
-        if ErrorMsg.anyErrors () then
+        if stopHere () then
             ()
         else
             if List.exists kunifsInDecl file then
@@ -4651,7 +4653,7 @@
             else
                 ();
         
-        if ErrorMsg.anyErrors () then
+        if stopHere () then
             ()
         else
             if List.exists cunifsInDecl file then
@@ -4661,7 +4663,7 @@
             else
                 ();
 
-        if ErrorMsg.anyErrors () then
+        if stopHere () then
             ()
         else
             app (fn all as (env, _, _, loc) =>
@@ -4670,7 +4672,7 @@
                       | SOME p => expError env (Inexhaustive (loc, p)))
                 (!delayedExhaustives);
 
-        if ErrorMsg.anyErrors () then
+        if stopHere () then
             ()
         else
             !checkConstraintErrors ();
diff -r f7d9dc5d57eb -r 5ecf67553da8 src/main.mlton.sml
--- a/src/main.mlton.sml	Sat Apr 21 15:47:02 2012 -0400
+++ b/src/main.mlton.sml	Sun Apr 22 09:08:45 2012 -0400
@@ -85,6 +85,9 @@
       | "-dumpTypes" :: rest =>
         (Elaborate.dumpTypes := true;
          doArgs rest)
+      | "-unifyMore" :: rest =>
+        (Elaborate.unifyMore := true;
+         doArgs rest)
       | "-dumpSource" :: rest =>
         (Compiler.dumpSource := true;
          doArgs rest)
diff -r f7d9dc5d57eb -r 5ecf67553da8 tests/league.ur
--- a/tests/league.ur	Sat Apr 21 15:47:02 2012 -0400
+++ b/tests/league.ur	Sun Apr 22 09:08:45 2012 -0400
@@ -4,4 +4,5 @@
 table team : { Id : team,
                League : league }
 
-val foo:int = queryL(SELECT * FROM team)
+val foo = queryL(SELECT * FROM team)
+val bar : int = "hi"