Jerome Hugues (May 12 2022 at 15:57): Jerome Hugues (May 12 2022 at 15:57):Hi,
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.
Thanks
Guillaume Melquiond (May 12 2022 at 16:01):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.
Guillaume Melquiond (May 12 2022 at 16:02):(But if you swap both lines in the match with, you should get an error message.)
Jerome Hugues (May 12 2022 at 16:03):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?
Jerome Hugues (May 12 2022 at 16:04):If I had another stupid names, it indicates it is redundant with the previous one. Should I understand it acts as _ ?
Guillaume Melquiond (May 12 2022 at 16:05):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.
Jerome Hugues (May 12 2022 at 16:08):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.
Notification Bot (May 12 2022 at 16:09):Jerome Hugues has marked this topic as resolved.
Gaëtan Gilbert (May 12 2022 at 16:13):why is this not triggering the unused-pattern-matching-variable warning?
Guillaume Melquiond (May 12 2022 at 16:18):Does that exist? I don't think I have ever seen that warning.
Gaëtan Gilbert (May 12 2022 at 16:19):Definition is_zero (o : option nat) :=
match o with
| Some 0 => true
| x => false
end.
says Warning: Unused variable x catches more than one case.
I guess it's because when it's exactly 1 case there's no warning
Gaëtan Gilbert (May 12 2022 at 16:21):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
Jerome Hugues (May 12 2022 at 16:51):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.
Notification Bot (May 12 2022 at 19:01):Paolo Giarrusso has marked this topic as unresolved.
Paolo Giarrusso (May 12 2022 at 19:01):There seems to be something else going on...
Paolo Giarrusso (May 12 2022 at 19:01):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
Paolo Giarrusso (May 12 2022 at 19:02):but this might not be the first warning that's omitted by VsCoq, so that might be an orthogonal problem
Gaëtan Gilbert (May 12 2022 at 20:47):I see the warning fine with it enabled-not-error
Jerome Hugues (May 12 2022 at 21:09):Thanks for the investigation
I tested the snippet provided by Paolo with "unused-pattern-matching-variable".
|w_args x ... is commented out, I see a warning (or error if "+" used) both in VSCoq and when building from the command ilneSince 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
Gaëtan Gilbert (May 12 2022 at 21:18):it looks like intentional behaviour, I just don't know the reasoning
Théo Zimmermann (May 13 2022 at 12:07):The reasoning seems to be explained here: https://github.com/coq/coq/pull/12768#issuecomment-700227387
Théo Zimmermann (May 13 2022 at 12:08):I.e., many more warnings would have been triggered in the stdlib in this case.
Théo Zimmermann (May 13 2022 at 12:08):I don't think this makes a strong argument, so this should be possible to evolve this warning to also include this case.
Gaëtan Gilbert (May 13 2022 at 18:15):I tried changing it and it only triggered about 5 times in the stdlib
Gaëtan Gilbert (May 13 2022 at 18:15):maybe I should submit
Gaëtan Gilbert (May 13 2022 at 18:15):(I ended up unsure how to phrase the warning and doc so I deleted my branch)
Jerome Hugues (May 19 2022 at 13:46):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.
Gaëtan Gilbert (May 19 2022 at 13:55):you can make an issue
Jerome Hugues (May 19 2022 at 14:03):Will do. Yet the title I use here is inaccurate. Do you have one to suggest? Thanks!
Pierre Roux (Jun 03 2022 at 11:47):@Jerome Hugues I just made a PR: https://github.com/coq/coq/pull/16135 is there an issue I should mark as closed?
Jerome Hugues (Jun 07 2022 at 14:10):@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