[isabelle-dev] auto raises a TYPE exception

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

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