Mercurial > urweb

changeset 1668:64c1e65c2365

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prevent horrifying loops in unification variable graph
author Adam Chlipala <adam@chlipala.net>
date Mon, 09 Jan 2012 16:20:10 -0500
parents 833402503855
children 61421ab6be36
files src/elaborate.sml
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/elaborate.sml	Mon Jan 09 09:51:39 2012 -0500
+++ b/src/elaborate.sml	Mon Jan 09 16:20:10 2012 -0500
@@ -1188,16 +1188,19 @@
                | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
                | _ => isRecord' ()
      in
-         (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
-                                  ("c2All", p_con env c2All)];*)
-
-         case (c1, c2) of
+         (*eprefaces "unifyCons''" [("c1", p_con env c1All),
+                                  ("c2", p_con env c2All)];*)
+
+         (case (c1, c2) of
              (L'.CError, _) => ()
            | (_, L'.CError) => ()
 
            | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) =>
-             if r1 = r2 andalso nl1 = nl2 then
-                 ()
+             if r1 = r2 then
+                 if nl1 = nl2 then
+                     ()
+                 else
+                     err (fn _ => TooLifty (loc1, loc2))
              else if nl1 = 0 then
                  (unifyKinds env k1 k2;
                   if f1 c2All then
@@ -1335,7 +1338,9 @@
            | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
              unifyCons' (E.pushKRel env x) loc c1 c2
 
-           | _ => err CIncompatible
+           | _ => err CIncompatible)(*;
+        eprefaces "/unifyCons''" [("c1", p_con env c1All),
+                                  ("c2", p_con env c2All)]*)
      end
 
  and unifyCons env loc c1 c2 =
@@ -3010,7 +3015,7 @@
 
             fun folder (sgi2All as (sgi, loc), env) =
                 let
-                    (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*)
+                    (*val () = prefaces "folder" [("sgi2", p_sgn_item env sgi2All)]*)
 
                     fun seek' f p =
                         let
@@ -4496,7 +4501,6 @@
                 val () = resetCunif ()
                 val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs))
             in
-                                    (**)
                 (ds, (env', gs))
             end