merged
authorpaulson
Fri Oct 15 17:21:37 2010 +0100 (2010-10-15)
changeset 39998b253319c9a95
parent 39996 c02078ff8691
parent 39997 b654fa27fbc4
child 40027 98f2d8280eb4
merged
     1.1 --- a/src/Pure/type.ML	Fri Oct 15 21:50:26 2010 +0900
     1.2 +++ b/src/Pure/type.ML	Fri Oct 15 17:21:37 2010 +0100
     1.3 @@ -418,10 +418,12 @@
     1.4  
     1.5  fun typ_match tsig =
     1.6    let
     1.7 -    fun match (TVar (v, S), T) subs =
     1.8 +    fun match (T0 as TVar (v, S), T) subs = 
     1.9            (case lookup subs (v, S) of
    1.10              NONE =>
    1.11 -              if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
    1.12 +              if of_sort tsig (T, S) 
    1.13 +              then if T0 = T then subs (*types already identical; don't create cycle!*)
    1.14 +                   else Vartab.update_new (v, (S, T)) subs
    1.15                else raise TYPE_MATCH
    1.16            | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.17        | match (Type (a, Ts), Type (b, Us)) subs =
     2.1 --- a/src/Pure/unify.ML	Fri Oct 15 21:50:26 2010 +0900
     2.2 +++ b/src/Pure/unify.ML	Fri Oct 15 17:21:37 2010 +0100
     2.3 @@ -205,6 +205,14 @@
     2.4  exception ASSIGN;  (*Raised if not an assignment*)
     2.5  
     2.6  
     2.7 +fun self_asgt (ix,(_,TVar (ix',_))) = (ix = ix')
     2.8 +  | self_asgt (ix, _) = false;
     2.9 +
    2.10 +fun check_tyenv msg tys tyenv = 
    2.11 +  if Vartab.exists self_asgt tyenv
    2.12 +  then raise TYPE (msg ^ ": looping type envir!!", tys, []) 
    2.13 +  else tyenv;
    2.14 +
    2.15  fun unify_types thy (T, U, env) =
    2.16    if T = U then env
    2.17    else
    2.18 @@ -715,7 +723,7 @@
    2.19          fun result env =
    2.20            if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
    2.21              SOME (Envir.Envir {maxidx = maxidx,
    2.22 -              tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
    2.23 +              tyenv = Vartab.make (filter_out self_asgt (map (norm_tvar env) pat_tvars)),
    2.24                tenv = Vartab.make (map (norm_var env) pat_vars)})
    2.25            else NONE;
    2.26