[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Makarius wrote:

>  * 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.

I've done this now in c4264f71dc3b .. 568b2cd65d50.  The main thing is 
0fa3b456a267 to "unify types of schematic variables in non-lifted case".

This was rather trivial, but there were some surprises nonetheless: Metis 
proof reconstruction seems to require the non-unification of types of 
Vars, despite having a separate workaround for exactly that problem
(see resolve_inc_tyvars in 568b2cd65d50).

Without the latter, src/HOL/Metis_Examples/Clausification.thy crashes at 
the very end, due to divergence of types of certain Vars, types that 
cannot be unified.  This is very odd, but should not be a problem at the 
moment: Metis should work as before.

If any of the experts on Metis proof reconstruction want to clean that up: 
Thm.bicompose {incremented = false, ...} means types get unified, while 
{incremented = true, ...} means there is no need for it since variables 
have been incremented as for resolution.  If it works one day without the 
extra toggle, we can simplify the low-level Thm.bicompose once again. (And 
all these "compose" variants are definitely outside normal user space.)


Anyway, apart from having seen a lot of boundary cases of the unification 
code -- things we've seen more often in distant past -- the conclusion is 
inconclusive.  The system cannot be changed substantially at its very 
bottom, but we knew that already.


 	Makarius