[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Mon May 27 18:13:52 CEST 2013
On Mon, 27 May 2013, Stefan Berghofer wrote:
> As I pointed out in my previous mail, it is an error to supply
> disagreement pairs to unify containing Vars that have the same name but
> different types. So I don't think one should change pattern.ML and
> unify.ML so that it unifies these different types and pretends that
> everything is all right, but one should find and correct the function
> that supplies these erroneous disagreement pairs to unify. Do we have an
> idea where these disagreement pairs came from? Maybe someone just forgot
> to increment the indices of variables before invoking bicompose?
According to my understanding, the disunity of types came recursively from
the pattern/unify implementation itself. My guess is that certain
schematic variables first started as ?x::?'a and then diverged with more
concrete type here, and the original general type there.
The change ensures that variables with equal name are unified, in the same
manner as the types of Free or Const are unified, before doing the real
work of HO-unification.
More information about the isabelle-dev