[isabelle-dev] auto raises a TYPE exception

[Makarius]

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