# HG changeset patch
# User paulson
# Date 1287159667 -3600
# Node ID b654fa27fbc499fa406df1a50afe634b8e23084c
# Parent  eebfa0b9389692b579db0d197a8e2f2a4cef1759
prevention of self-referential type environments

diff -r eebfa0b93896 -r b654fa27fbc4 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Oct 14 12:40:14 2010 +0200
+++ b/src/Pure/type.ML	Fri Oct 15 17:21:07 2010 +0100
@@ -418,10 +418,12 @@
 
 fun typ_match tsig =
   let
-    fun match (TVar (v, S), T) subs =
+    fun match (T0 as TVar (v, S), T) subs = 
           (case lookup subs (v, S) of
             NONE =>
-              if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
+              if of_sort tsig (T, S) 
+              then if T0 = T then subs (*types already identical; don't create cycle!*)
+                   else Vartab.update_new (v, (S, T)) subs
               else raise TYPE_MATCH
           | SOME U => if U = T then subs else raise TYPE_MATCH)
       | match (Type (a, Ts), Type (b, Us)) subs =
diff -r eebfa0b93896 -r b654fa27fbc4 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Thu Oct 14 12:40:14 2010 +0200
+++ b/src/Pure/unify.ML	Fri Oct 15 17:21:07 2010 +0100
@@ -205,6 +205,14 @@
 exception ASSIGN;  (*Raised if not an assignment*)
 
 
+fun self_asgt (ix,(_,TVar (ix',_))) = (ix = ix')
+  | self_asgt (ix, _) = false;
+
+fun check_tyenv msg tys tyenv = 
+  if Vartab.exists self_asgt tyenv
+  then raise TYPE (msg ^ ": looping type envir!!", tys, []) 
+  else tyenv;
+
 fun unify_types thy (T, U, env) =
   if T = U then env
   else
@@ -715,7 +723,7 @@
         fun result env =
           if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
             SOME (Envir.Envir {maxidx = maxidx,
-              tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
+              tyenv = Vartab.make (filter_out self_asgt (map (norm_tvar env) pat_tvars)),
               tenv = Vartab.make (map (norm_var env) pat_vars)})
           else NONE;