I am scratching my head on the following issue
I have this basic test
Inductive foo := | stupid_long_name_1 | stupid_long_name_stupid_long_name_1. Definition bar (f : foo) := match f with | stupid_long_name_1 => true | stupid_long_name_stupid_long_name_2 => false (* <- typo *) end.
I would have expected Coq (8.14) to report an issue on this line, since there is an obvious typo. However, stepping in VSCoq and compilation from the command line using Dune reports no issue.
Is there any limits on the length of identifiers used in such case? Can someone test in his setup and confirm?
Generally speaking, is there a list of known implementation restrictions? I cannot find one in the reference manual.
You are under the assumption that this is actually a typo. It is not. It is perfectly legal Coq code. That is why you get no error.
(But if you swap both lines in the
match with, you should get an error message.)
Indeed, I get
Pattern "stupid_long_name_1" is redundant in this clause.
So this is counterintuitive to me. What is the rationale to accept this? Does this apply only to the last element?
If I had another stupid names, it indicates it is redundant with the previous one. Should I understand it acts as
If a pattern is not a constructor (e.g., due to a typo), it is parsed as a pattern variable. So, it is
x rather than
_, in that you can actually refer to that variable in the branch.
oh, that makes perfect sense then. And indeed this is implied in the reference manual.
The full syntax of match is presented in Definition by cases: match. Identifiers in patterns are either constructor names or variables. Any identifier that is not the constructor of an inductive or coinductive type is considered to be a variable.
I overlooked this part. Thanks a lot for the fast answer.
Jerome Hugues has marked this topic as resolved.
why is this not triggering the unused-pattern-matching-variable warning?
Does that exist? I don't think I have ever seen that warning.
Definition is_zero (o : option nat) := match o with | Some 0 => true | x => false end.
Warning: Unused variable x catches more than one case.
I guess it's because when it's exactly 1 case there's no warning
see also https://github.com/coq/coq/pull/12768
it doesn't seem to explain why there should be no warning when there's just 1 case
Good question. I am either using default settings or a library that are changing these. I would have also expected a warning that mentions that the variable is not used on the right side.
Paolo Giarrusso has marked this topic as unresolved.
There seems to be something else going on...
In VsCoq I see this:
Inductive foo := | stupid_long_name_1 | stupid_long_name_stupid_long_name_1 | w_args (x : nat). Set Warnings "unused-pattern-matching-variable". (* Nothing shown below *) (* Set Warnings "+unused-pattern-matching-variable". gives an error instead*) Definition bar (f : foo) := match f with | stupid_long_name_1 => true (* | w_args x => true *) | x => false (* <- typo *) end.
so if the warning is enabled, or by default, I see nothing, but if I make it an error the code fails
but this might not be the first warning that's omitted by VsCoq, so that might be an orthogonal problem
I see the warning fine with it enabled-not-error
Thanks for the investigation
I tested the snippet provided by Paolo with
|w_args x ...is commented out, I see a warning (or error if "+" used) both in VSCoq and when building from the command ilne
Since the behavior is consistent from the command line and from within VSCoq, this looks like an issue with Coq itself. I am using 8.14 at the moment, I need to upgrade to 8.15 to see if this is still an issue
it looks like intentional behaviour, I just don't know the reasoning
The reasoning seems to be explained here: https://github.com/coq/coq/pull/12768#issuecomment-700227387
I.e., many more warnings would have been triggered in the stdlib in this case.
I don't think this makes a strong argument, so this should be possible to evolve this warning to also include this case.
I tried changing it and it only triggered about 5 times in the stdlib
maybe I should submit
(I ended up unsure how to phrase the warning and doc so I deleted my branch)
Hi, (sorry this felt off my radar)
@Gaëtan Gilbert , is there a GitHub issue in Coq dev or PR to track this? I find the idea of an additional warning great. Thanks for investigatin this.
you can make an issue
Will do. Yet the title I use here is inaccurate. Do you have one to suggest? Thanks!
@Jerome Hugues I just made a PR: https://github.com/coq/coq/pull/16135 is there an issue I should mark as closed?
@Pierre Roux sorry i missed this message. Sure, this could be considered as closed per the reviews on Github. Thanks!
Last updated: Sep 26 2023 at 12:02 UTC