[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 11:36:09 CEST 2013
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
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
(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
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.
More information about the isabelle-dev