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

[Makarius]

On Thu, 2 Dec 2010, Alexander Krauss wrote:

> 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.

In fact I've made this error already in 2005, and it was Alex himself who 
convinced me more recently that packagages cannot realistically do any 
check here, because the thing is so obscure that hardly any package author 
will get to the point.

Back to history: in 2005 Brian had a paper on TPHOLs with a footnote about 
an unexpected crash of the typedef package due to hidden polymorphism in 
the set involved, not the type.  What I did then is to make the typedef 
package insert "itself" arguments in the way one would think of as a first 
idea.  This made the problem go away for the moment, although it 
complicated the package implementation.  When Larry was asking me about 
that change of typedef later, I also failed to explain to him both the 
problem and its solution.

After Local_Theory.define started handling the problem uniformly once and 
for all, I could remove lots of strange code from typedef, and be sure at 
the same time that all other (localized) packages would stop crashing
on the same kind of problem.


When we speak about "users" of packages it covers both ML and Isar theory 
sources, e.g. the function package is a user of the inductive package. 
It is important to keep modularity here.

The system is able to distinguish between things that are visible in the 
source vs. internal uses of the same specifciation mechanisms to some 
extent, but one needs to look very closely at that when modifying the 
behaviour here.  We have already a long track record of very abscure 
crashes due to errors that are emitted too eagerly, e.g. in declaration 
attributes that insist in certain input and choke on the transformed 
version after some interpretations.

Part of the inherent complexity of local theory specifications is due to 
interpretation wrt. the "target context", which always happens when 
writing down specifications like 'definition' or 'inductive'.  This is not 
the primitive consts + defs that we had many yours ago.  And of course, 
the extra complexity localized specifications was not introduced for fun, 
but to address concrete problems that had accumulated over a couple of 
years of less systematic treatment of these issues.  Compared to the 
situation before it, there are very little problems left that need some 
fine tuning.


 	Makarius