[isabelle-dev] auto raises a TYPE exception

[Tobias Nipkow]

Am 27/05/2013 18:13, schrieb 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.

it would be good to have an example of that.

> 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.

unless the need for additional type unification is inherent in the algorithm
itself rather than the violation of a precondition in the input, your change
masks something going wrong elsewhere. which is stefan's point.

tobias

> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev