Stream: Coq users

Topic: match and long identifiers


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (May 12 2022 at 16:02):

(But if you swap both lines in the match with, you should get an error message.)

view this post on Zulip 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?

view this post on Zulip 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 _ ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (May 12 2022 at 16:09):

Jerome Hugues has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (May 12 2022 at 16:13):

why is this not triggering the unused-pattern-matching-variable warning?

view this post on Zulip Guillaume Melquiond (May 12 2022 at 16:18):

Does that exist? I don't think I have ever seen that warning.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Notification Bot (May 12 2022 at 19:01):

Paolo Giarrusso has marked this topic as unresolved.

view this post on Zulip Paolo Giarrusso (May 12 2022 at 19:01):

There seems to be something else going on...

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (May 12 2022 at 19:02):

so if the warning is enabled, or by default, I see nothing, but if I make it an error the code fails

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (May 12 2022 at 20:47):

I see the warning fine with it enabled-not-error

view this post on Zulip Jerome Hugues (May 12 2022 at 21:09):

Thanks for the investigation

I tested the snippet provided by Paolo with "unused-pattern-matching-variable".

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

view this post on Zulip Gaëtan Gilbert (May 12 2022 at 21:18):

it looks like intentional behaviour, I just don't know the reasoning

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 13 2022 at 12:08):

I.e., many more warnings would have been triggered in the stdlib in this case.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 13 2022 at 18:15):

I tried changing it and it only triggered about 5 times in the stdlib

view this post on Zulip Gaëtan Gilbert (May 13 2022 at 18:15):

maybe I should submit

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 19 2022 at 13:55):

you can make an issue

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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: May 19 2024 at 16:02 UTC