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

[Tobias Nipkow]

Am 27/02/2013 16:44, schrieb 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.

You fixed a problem in one place and it bubbles up as a dubious feature in other
places where there was no problem (eg the definition command). Nobody needs the
implicit introduction of type arguments in those places because it can be done
explicitly (and no example of its usage is seems to exist). Yet your recipe for
avoiding the reported confusions is to put out some kind of warning because most
likely the system did something the user did not want. Which gets overlooked
until the user has been "conditioned". I rest my case.

Tobias

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