--- 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 =
--- 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;