Disable warning 40 (Constructor or label name used out of scope)

[SkySkimmer]

Typically this lets us do

let elimination_suffix = function
  | Sorts.InSProp -> "_sind"
  | InProp -> "_ind"
  | InSet -> "_rec"
  | InType -> "_rect"

instead of

let elimination_suffix = function
  | Sorts.InSProp -> "_sind"
  | Sorts.InProp -> "_ind"
  | Sorts.InSet -> "_rec"
  | Sorts.InType -> "_rect"

or having to open Sorts.

This change was previously proposed and rejected in
#11485 but more recent discussion with
@ejgallego indicated that opinions may have changed since.

[ppedrot]

I'm still not happy with this. While I do think OCaml shouldn't warn as soon as we qualify one constructor from a pattern-matching, completely deactivating the warning in general results in brittle code that depends on type-checking and loaded modules.

[SkySkimmer]

I wish I had been smart enough to avoid enabling this warning in #582

[ejgallego]

There is actually a coding style that I like that depends on this warning. Indeed, I have soften my stanza quite a bit since I really like that coding style, and actually I think you do too @ppedrot !

The coding style I'm talking about is when you put most datatypes in Foo_bar module, so the data type itself is Foo_bar.t.

We already do quite a lot of that in Coq, tho not always, but new code we are introducing tends to follow that pattern. When you do that, having to open / qualify constructors all the time is just too annoying.

Instead, I like to rely on a cool feature of the compiler that will allow to you skip the opening if you annotate the type, in @SkySkimmer 's example:

let elimination_suffix (s : Sorts.t) = match s with
  | InSProp -> "_sind"
  | InProp -> "_ind"
  | InSet -> "_rec"
  | InType -> "_rect"

There may be indeed concern about "results in brittle code that depends on type-checking and loaded modules", maybe @ppedrot you can refresh us with an example of the problem?

[Alizter]

I am also not happy with this. I would do

let elimination_suffix =
  let open Sorts in
  function
  | InSProp -> "_sind"
  | InProp -> "_ind"
  | InSet -> "_rec"
  | InType -> "_rect"

instead.

[ejgallego]

I am also not happy with this.

What makes you unhappy?

Note that there are many other cases (for example records) where this becomes a real PITA. The warning does not only help with pattern matching, but with construction and access.

[Alizter]

For this:

let elimination_suffix = function
  | Sorts.InSProp -> "_sind"
  | InProp -> "_ind"
  | InSet -> "_rec"
  | InType -> "_rect"

reordering branches now gets tricky.

For this:

let elimination_suffix (s : Sorts.t) = match s with
  | InSProp -> "_sind"
  | InProp -> "_ind"
  | InSet -> "_rec"
  | InType -> "_rect"

You have to type annotate.

[ejgallego]

You have to type annotate.

Yes, I prefer to type annotate (which helps with reading the function actually!) to a random let open.

[ejgallego]

I agree that the original form with just one annotation is ugly too.

[SkySkimmer]

@Alizter I don't like having to open here, in the general case the branches are non trivial and we can't open just for the patterns.

[Alizter]

We can also do the following:

let elimination_suffix = Sorts.(function
  | InSProp -> "_sind"
  | InProp -> "_ind"
  | InSet -> "_rec"
  | InType -> "_rect")

But in any case, my unhappiness should not block this PR. If it improves reading and writing maintainable code for you, then that is a good enough reason for me.

[ejgallego]

We can also do the following:

let elimination_suffix = Sorts.(function
  | InSProp -> "_sind"
  | InProp -> "_ind"
  | InSet -> "_rec"
  | InType -> "_rect")

That works of for this case, but as I mention the warning blocks some more interesting use cases, for example enable it in Dune's coq_rules.ml . I feel that the local open in this case doesn't really help.

But in any case, my unhappiness should not block this PR. If it improves reading and writing maintainable code for you, then that is a good enough reason for me.

Well, I don't see this as a matter of "blocking/non blocking" ; I think that if you and Pierre-Marie are unhappy we should understand what makes you unhappy, same for Gaëtan, and see what makes everyone unhappy.

For example, my initial opposition to removing 40 was that indeed I much prefer let open to that ugly add the module to just one constructor, but once I discovered type annotation worked much better for me in all cases I'm happy taking advantage of that.

[ejgallego]

But indeed, if we remove warning 40, we should def try to come up with a single style for using this feature of the compiler.

[SkySkimmer]

I agree the type annotation is nicer. I just always forget that it's possible since currently the warning prevents it from being useful.

[ejgallego]

If you are available today we can discuss about it in the meeting.

[ejgallego]

Good to me. Can we document the preferred (and IMHO) safer use of this feature by adding a type annotation to the variable at play?

Do we have a coding style guide file?

[Alizter]

From the call:

@ppedrot says that this will encourage fragile code and I somewhat agree.
@SkySkimmer @ejgallego say that they can write better/easier code.

I will therefore side with going this direction, but if it does cause demonstrable issues in the future we can think about re-enabling the warning. The core issue here is that OCaml has a missing feature, and complaining about this will not help.

[ejgallego]

@ppedrot says that this will encourage fragile code and I somewhat agree.

Can you write down an example of fragile code (when using a type annotation) so others can weight in about the problem (for example rest of kernel maintainers) ?

[Alizter]

@ppedrot says that this will encourage fragile code and I somewhat agree.

Can you write down an example of fragile code (when using a type annotation) so others can weight in about the problem (for example rest of kernel maintainers) ?

No which is why I am OK with merging this and finding out if it was the wrong decision in the future.

[Alizter]

@ejgallego A style guide for the entire repo is a sure way to make everybody unhappy. It would be yet another piece of developer documentation to keep track of (our actual dev docs are poor anyway). I think it is better to let everybody do their own thing and fight about it in review rather than imposing a particular style.

Coq's main focus should be getting people to write code rather than restricting the code they are writing. Trends change, technologies change, lets focus on more important things.

[ejgallego]

No which is why I am OK with merging this and finding out if it was the wrong decision in the future.

Well I mean if we wrote in the summary that "this will encourage fragile code" we either write the example down here (or maybe @ppedrot can do) or else we will forgot about what we were meaning in the future. Or if we don't have an example of such code, then we should amend that statement.

[ejgallego]

A style guide for the entire repo is a sure way to make everybody unhappy.

Maybe this does explain why people is unhappy as we actually have 2 style guides in the repos (CONTRIBUTING.md and dev/doc/style.txt)

Even if we didn't have them, how does a style guide makes everybody unhappy?

For example, such guides do make me happy and I have learnt a lot of useful coding tips, such as the proper utilization of Warning 40.

Coq's main focus should be getting people to write code rather than restricting the code they are writing. Trends change, technologies change, lets focus on more important things.

Coq main focus should indeed be that, however, as noted in the beginning of the style guide, we aim for a high standard of quality in Coq, an style uniformity is also essential so people can first understand and easily read Coq's codebase, which is not exactly small. Moreover, the addition I'm suggesting does make contributing to Coq in code much more pleasant!

Anyways, I think it is a good idea to add the tip for using correctly OCaml's type-based disambiguation to the style guide, as both Gaëtan and I agree on the preferred way, problem-free way which is to hint the type-checker at binding introduction time.

[Alizter]

I'm removing my assignment, since I don't care enough to get it merged. If you want to disable the warning or add style documentation that is fine by me.

[ejgallego]

Ok I suggest we merge, @SkySkimmer , would you mind adding a small section to the style guide about this?

IMHO the

match x with
| Foo.Bar -> ...
| Baz -> ....

style is ugly and we should avoid it.

[ejgallego]

Merci. @ppedrot you OK then?

[ejgallego]

@coqbot: merge now