[isabelle-dev] auto raises a TYPE exception

[Lawrence Paulson]

On 28 May 2013, at 19:52, Makarius <makarius at sketis.net> wrote:

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

This is never done, as far as I know. It is known to be intractable.

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

This approach sounds safer anyway.