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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
