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

[Makarius]

On Wed, 27 Feb 2013, Tobias Nipkow wrote:

>> 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 neither fixed a bug, nor introduced a feature.  You were also not there 
yourself when we've had a lot of spurious exception TYPE of TERM raised 
from the bottom of the pits over many years.

The "bubbling" of certain results that might turn out as errors later was 
in fact a quite succesful strategy to get more useful user feedback of the 
system in recent years. These things are more easy to see in the syntactic 
processing of Isabelle symbols, tokens, parse trees, but it is getting 
more complex when approaching the type-inference phase.


Just to get on-topic for this off-topic thread again (which has been an 
FAQ occurring 1-2 times a year on isabelle-users): Larry was surprised to 
see that "..." was not just the argument term literally.

I actually had that in an early version of Isar around 1998/1999, but it 
turned out hardly usable without the Hindley-Milner type generalization 
within the proof text.  So I added that, while realizing the problem that 
was later formally called "hidden polymorphism".  Back then I had a 
slightly awkward indication of the excess polyorphism that would now cause 
much more surprise if it were still there.  When the 'a itself argument 
emerged as the standard way to represent that situation, I merely cleaned 
up that old code.

Note that the deeper problem here is that the system cannot just complain 
at the first occurrence of something that is in itself not yet an error.
And even hard errors are often better reported in a different spot that 
knows more about the context of the problem.


Anyway, the user report by Larry is a reminder that the error-reporting of 
type-inference (notable the version with coercions) needs more work. 
Hopefully, I will soon find some time to convene with Dmitriy to see how 
the detailed PIDE markup that is already routine in most other syntax 
layers can be used for type check errors or exceptional situations that 
are not errors at all, just boundary cases of Hindley-Milner polymorphism.

These will not be warnings (which are a TTY concept), but some color 
scheme on the source text.


 	Makarius