[isabelle-dev] auto raises a TYPE exception
lp15 at cam.ac.uk
Wed May 29 14:39:21 CEST 2013
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.
More information about the isabelle-dev