[isabelle-dev] Additional type variable(s) in specification

[Alexander Krauss]

Makarius wrote:
> 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.

Alex