[isabelle-dev] auto raises a TYPE exception

[Lawrence Paulson]

Historical note: when the original high-order unification code was written, there was no user-level polymorphism. If my memory is correct, the TVar constructor did not even exist. Polymorphism was only used for type inference in terms. Any idea to unify types while at the same time identifying previously distinct variables needs to be scrutinised with very great care. Better to have an exception raised than to have unsound reasoning.
Larry

On 28 May 2013, at 10:36, Makarius <makarius at sketis.net> wrote:

> On Tue, 28 May 2013, Stefan Berghofer wrote:
> 
>> Types as well as terms are unified.  The outermost functions assume
>> the terms to be unified already have the same type.  In resolution,
>> this is assured because both have type "prop".
>> 
>> So it is the expected behaviour that the unification functions cannot cope with the above example, since it does not satisfy this precondition.
> 
> I am getting a bit uneasy about that for two reasons:
> 
>  (1) There might be really something wrong in Thm.bicompose_aux or
>      Thm.assumption that fails to "assure" such implicit assumptions of
>      unify.ML.
> 
>  (2) The notorious problem of "hidden polymorphism", i.e. extra
>      generality of types that is not seen on the surface, and thus needs
>      to be treated while walking into the term structure.
> 
> The second point might be relevant for Pattern.match as well: it does one typ_match thy on the outside, and then only for Free/Const/Bound, but not for Var.
> 
> So we seem to be back at the implicit global assumption that the types of Vars happen to work out "magically", without further ado.  There used to be that comment in really ancient Isabelle versions, before Stefan made an explicit check that it does not go wrong, but here it did go wrong.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev