[isabelle-dev] Fwd: A possible bug with Isabelle 2013
makarius at sketis.net
Fri Mar 1 12:35:59 CET 2013
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.
More information about the isabelle-dev