[isabelle-dev] Additional type variable(s) in specification
krauss at in.tum.de
Thu Dec 2 19:22:12 CET 2010
> Maybe Florian (and Alex) can post again the concrete examples they were
> mentioning to me 1 or 2 years ago.
The original problem was that the function package sometimes issues an
inductive definition with hidden polymorphism whenever there are type
variables in the function type that do not occur in the argument type.
Prior to 09e238561460, this would lead to an inexplicable low-level
error in the primitive definitions issued by inductive, and the only way
of preventing this would be that function adds the type argument itself
in this special case. Now this is done by the local theory
infrastructure, and this is clearly where it belongs; transparently
adding type arguments greatly simplifies correct package development.
All this applies to internal definitions which are just for the
foundation. There the actual form of the underlying constant is
irrelevant and hidden.
The situation is different for specifications issued by the user. Here,
hidden polymorphism should simply be rejected completely. As an instance
of "explicit is better than implicit" you should always get what you
specify. If you specify something that you cannot get, you should get
an error, not something different and a warning.
I'll have a look at the code and see if packages can reject this from
the user, while still being composable. This applies to all packages.
More information about the isabelle-dev