[isabelle-dev] auto raises a TYPE exception
nipkow at in.tum.de
Tue May 28 02:15:52 CEST 2013
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
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev