[isabelle-dev] auto raises a TYPE exception

[Makarius]

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.


 	Makarius