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