[isabelle] Additional Type Parameter when Interpreting Locale Using 'for' Clause

Dear all,

I recently stumbled upon the following behavior in Isabelle which I
find surprising and which affects me negatively. In the attached
theory, the constant "bar" is defined in the locale "foo". This locale
is then interpreted as "baz" using a 'for' clause to retain the
parameter "f".

I had expected that "baz.bar" would be "% f. foo.bar f 0" :: "('a =>
'b) => 'b". Instead, it is "% type f. foo.bar f 0" :: "'a itself =>
('a => 'b) => 'b". Why is there a type parameter, given that the type
variable "'a" is already determined by the parameter "f"? It seems
that Andreas Lochbihler has already stumbled upon the same issue
but it did not get any replies. It seems that everything works when I
instantiate the parameter "type" with "TYPE('a)", but I would prefer
if I didn't have to do that.


Attachment: TypeParameter.thy
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.