On 28 May 2013, at 19:52, Makarius <[email protected]> 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
