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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
