The Coq mailing list

[Cédric <sedrikov AT gmail.com>]

Le Sun, 03 Aug 2014 17:00:13 +0200, Matej Kosik  
<5764c029b688c1c0d24a2e97cd764f AT gmail.com> a écrit:

> On 03/08/14 13:06, Gabriel Scherer wrote:
> > One man's random garbage is another's perfectly valid variable name.
> > Matej was, however, getting an error message, highlighting the extra
> > cases after the free variable.
> >
> > > Error: this clause is redundant.
> >
> > It's delicate to design languages with pattern-matching that never
> > behave confusingly. In OCaml, variables may not start with an
> > uppercase, precisely to avoid this problem. In some other languages,
> > variables are not patterns by themselves, you have to use some
> > explicit marker to turn a variable in a binder pattern. That's also
> > rather heavy.
>
> My caution against typos in variable names was dulled by Ocaml.
>
> There, instead of:
>
>         Toplevel input, characters ...-...:
>         >     | April | June | September | November => true
>         >       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>         Error: this clause is redundant.
>
> I would get:
>
>         Toplevel input, characters ...-...:
>               | Feburary => negb leap
>                 ^^^^^^^^
>         Warning: Unused variable "Feburary"
>
>         Toplevel input, characters ...-...:
>         >     | April | June | September | November => true
>         >       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>         Error: This clause is redundant.
>
> which, however simple it sounds, would lead me to the right direction.
>
> Until unused variables are detected by Coq automatically, I just have to  
> be more careful.

I guess Coq will never warn against unused variables:
that would not mix very well with the interactive features.
"refine (match x with A => _ | B => _ end)." will never raise a warning as  
'_' is to be filled later.

I would prefer to disallow variables as patterns, but that would break  
compatibility with already existing developements, and many people won’t  
be happy if this feature were to be removed (I am not one of them as I  
never need nor use it, and because as far as I can remember, there is no  
support internally for this, and the matching is expanded, well I may be  
wrong on this last point and/or things can have changed).

> Thank you guys.


--
---
Cédric AUGER