Am 28/05/2013 20:52, schrieb Makarius: > On Tue, 28 May 2013, Lawrence Paulson wrote: > >> the disagreement pairs should be fully eta-expanded by this point > > I've spent further thoughts on that: somehow it increases my uneasyness, since > it looks like the full type information needs to be known at some point to > make > eta-expansion work, but you do type unification of Free/Const/Bound > incrementally as you go. So some ?x::'?a could become a function indirectly, > e.g. by unifying c::'?a with c::nat=>bool elsewhere. > > Anyway, I better not claim any expertise here, after looking through the > sources > only for a few days. > > > How about this alternative approach: > > * No change to unify.ML (and especially pattern.ML, which was not really > covered so far). My 3b9c31867707 is backed-out. > > * Instead Thm.bicompose_aux in the non-lifted case (i.e. the "compose" > variants) ensures that the types of all Vars are unified > beforehand. So mentioning some ?x::?'a here and some ?x::nat=>bool > there means they become both ?x::nat=>bool before entering > Unify.unifiers (and Pattern.unify as well).
i would be very happy with it. > Thus we acknowledge the observation that the old code from 25 years ago does > not > work with Vars of different type: Stefan's check from 2005 raises suitable > exceptions, and the above pre-stage avoids that this happens. > > > What is a bit unstisfactory here is that it merely avoids certain crashes of > SELECT_GOAL (and maybe other crashes), but the example from this thread would > still not quite work, since the unification problem is presumably too > difficult. i thought the only limitation of the unification code is that it does not instantiate type vars to function types (to avoid another dimension of search). if that is happening here, so be it. 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
