[isabelle-dev] auto raises a TYPE exception

[Tobias Nipkow]

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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev