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 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: Feb 08 2023 at 23:03 UTC