[isabelle] Infinite variable chasing

Hello all,

I'm having a problem with looking up the instantiation to a variable in a matcher with Envir.lookup. The particular matcher is:

ML{* fun rtac' rl i j st = (snd o Seq.chop j) (rtac rl i st) *}

fixes g :: "nat => nat"
shows "((?f :: (?'a => ?'b) => ?'c) ?s = ?v) = (g a = x) & Q ?f ?s ?v"
apply rule
apply(tactic {* rtac' refl 1 1712 *})

goal (1 subgoal):
 1. Q (%a::?'a => nat. a (?f9 a)) (%b::?'a. g a) x
  a, x :: nat
  g :: nat => nat
  ?f9 :: (?'a => nat) => ?'a
  Q ::
    ((?'a => nat) => nat) => (?'a => nat) => nat => bool
type variables:
  ?'a :: type

If I lookup the instantiation to the variable ?s in this particular matcher, which here has the type ?'a => nat, I run into an infinite recursion. The infinite recursion seems to be caused by an infinite chasing of type variable assignment at Type.devar:

(*chase variable assignments; if devar returns a type var then it must be unassigned*)
fun devar tye (T as TVar v) =
      (case lookup tye v of
        SOME U => devar tye U
      | NONE => T)
  | devar _ T = T;

Put simply, there's no variable assignment for it to be chased.

In the implementation, Envir.lookup indirectly invokes Type.equal_type, which checks over each type variable -- in this case, that's ?'a and ?'b. ?'b is fine, and only ?'a is problematic. Now let's look at the tye:

val tye =
      (Empty, (("'a", 0), (["HOL.type"], "?'a")),
     (("'b", 0), (["HOL.type"], "RealDef.real")),
       (("'a", 1), (["HOL.type"], "RealDef.real")),
   : Type.tyenv

If we call devar tye on (?'a, 0), we'll run into an infinite recursion because lookup tye (TVar ("'a", 0), ["HOL.type"])) also gives (TVar ("'a", 0), ["HOL.type"])).

Why isn't the variable chasing procedure given a maximum depth?

Any help will be appreciated.


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.