[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

[Makarius]

On Mon, 22 Aug 2011, Brian Huffman wrote:

> Isabelle prints out warning messages whenever anyone declares a 
> duplicate simp rule, intro rule, etc. It would be nice if Isabelle would 
> print a similar warning whenever a definition reuses a name that is 
> already in scope in the current context. For example, if a theory 
> defines a class like this...
>
> class complete_boolean_algebra = distributive_complete_lattice + 
> boolean_algebra
>
> ...and a class called "complete_boolean_algebra" is already in scope, 
> then a warning message ought to be printed.
>
> Such a warning message would be useful for constant names, lemma names, 
> etc. as well.

When I've seen the "complete_boolean_algebra" incident on the other thread 
my first impulse was to check how far the wiring of the class package wrt. 
the Isabelle document markup was.  In principle the prover can provide 
useful clues in non-intrusive ways here, if done right.  E.g. in 
Isabelle/jEdit one can hover over the text with COMMAND/CONTROL to ask 
"What is this?" and often get useful feedback already.

Unfortunately, the class package is still in a confusing state here, so I 
did not even put it on the list of things to be done, because it is just 
another instance of similar ongoing reforms, and there are so many really 
pressing things in the pipeline.  (Quite a bit has happened here already, 
like purging the name space module from historic cruft one more time, and 
assembling all syntax layers clearly in one place.)


Anyway, your above idea of "warning whenever a definition reuses a name 
that is already in scope in the current context" does not really remind me 
of how this works internally.  What means "name" here?  E.g. a package 
defining some "induct" rule is perfectly right to do so in the presence of 
another "induct", as long as additional name qualification makes things 
clear to the system and the user.

We have reasonably well-established concepts of "binding", "naming", and 
"morphisms" on bindings. Any new feature somehow needs to fit smoothly 
into the picture.  Also note that a special twist is the name space merge 
that happens at theory import time: independent specifications can 
silently cause a conflicting situation in the application context.

What could work, and is on my list for a long time already, is to give 
some feedback in situations where *ambiguity* occurs in name space 
resolution.  This would also follow the intention behind the names_unique 
(formerly unique_names) option, only that the prover would show such spots 
spontaneously and non-intrustively whenever they appear in input or 
output, both in defining and referencing positions. (BTW, in Scala 
ambiguity after additional imports is treated as an error, and causes the 
conflicting name entries to be canceled out.)


 	Makarius