[isabelle-dev] Fwd: A possible bug with Isabelle 2013

[Makarius]

On Wed, 27 Feb 2013, Tobias Nipkow wrote:

> definition my0 :: nat where "my0 = length []"
>
> into a definition of a constant of type "'a itself ⇒ nat" with an 
> additional parameter. Although this is a legal definition, I never 
> understood why this is done automatically. The user could also write it 
> explicitly if he really wanted it that way. Chances are he did not. Is 
> this functionality actually used in the distribution?

We've had a lot of strange crashes in the past, before it was all unified 
towards the implicit introduction of TYPE / itself arguments in a few 
well-defined spots.

There might be other conceptual problems luring, but they did not show up 
in the past few years.

All known incidents were of the category as the present one: someone who 
is not yet conditioned to watch out for excess polymorphism stumbles over 
it, and gets surprised how ond type parameters here suddenly shows up 
there.  But this can be avoided by indicating the spots where polymorphism 
happens in the sources in a comprehensive way.

(This implicitly assumes that users are using the Isabelle document model, 
not the TTY loop.  If this is up to discussion, it should go on another 
thread.)


 	Makarius