A bit of history. The reason why the "all clauses guarded, bad style" warning was introduced (not by me) is that pedantic users objected to getting a "non exhaustive" warning for brilliant code such as

let abs = function
  | x when x >= 0 -> x
  | x when x < 0  -> -x

Personally, I don't care much for pedantry. But do keep in mind that this change will be viewed as a regression by some.

Could we arrange things so that:

let f = function
  | Some x when x -> foo

gives warning 8, whilst:

let f = function
  | Some x when x -> foo
  | None when true -> foo

gives warning 25.

That would seem to be in the spirit of the messages, and both the bug reports were complaining that they didn't get warning 8 even though the matches would still not have been exhaustive without the when clauses.

@lpw25 I don't understand what you suggest. Certainly you're not proposing to special case when true.

The point is as follows: when clause cannot make a pattern catch more cases than it already does, so if the clause patterns (without the when) are not exhaustive, we know for sure that the version with the when isn't either.

In Xavier's example,

let abs = function
  | x when x >= 0 -> x
  | x when x < 0  -> -x

the patterns without when cover all possible inputs, so (depending on the when clause that we are not trying to analyze) the pattern might be exhaustive. This is what justifies Xavier's point that warning for non-exhaustiveness could be seen as a regression.

On the contrary, see the example in the mantis PRs 7059 and 6438:

 match 1 with 1 when x = y -> 1;;

function Some x when x = 0 -> x;;

there it is the case that the clauses are clearly non-exhaustive, and users expect to see a non-exhaustivity warning.

Given that the non-exhaustivity warning is more objective and more interesting and more precise (it gives a non-matched example) than the "when bad style" warning, I think it would be good to see the non-exhaustivity warning in priority. If showing both warnings is too difficult for some reason, then we could try always showing the non-exhaustivity warning when we can, and only showing the "when bad style" warning when the without-when version is exhaustive.

(Luc says in PR#6438 that the exhaustivity information is already computed by first dropping the when clauses, anyway.)

I'm starting to doubt my memory. Perhaps the controversial example was the following buggy variant of abs:

let abs = function
  | x when x > 0 -> x
  | x when x < 0 -> -x

where no "not exhaustive" warning is displayed, even though it fails if x = 0. So, it was felt necessary to emit some other warning to cover this case.

At any rate, I agree that the "not exhaustive" warning should take precedence over the "all clauses guarded" one.

@gasche, currently guarded clauses are just ignored in the exhaustiveness check, and this is the only sound approach.
What you suggest would require to do the exhaustiveness check twice, which can be expensive, for a case which was already marked as bad style :)
Worse, to have any semblance of meaningfulness one should check that all guarded only cases appear at least twice, otherwise this would assume that the guard is always true, which is strange.

Indeed, I misread Luc's comment; exhaustiveness is not computed with when guards ignored, but after having removed all clauses that have a guard. This is very different.

However I still think that you could improve on the current behaviour without computing exhaustivity twice (which would be a good way to compute both over- and under-approximations of guards coverage). The current algorithm is (purely guessing):

1. If all clauses are guarded, emit "bad style warning" 25
2. Else, consider all clauses that are not guarded:
   • if exhaustive, pass
   • if not exhaustive, emit warning 8

The present PR proposes the following instead:

1. If all clauses are guarded, emit new variant of warning 8
2. Else, consider all clauses that are not guarded:
   • if exhaustive, pass
   • if not exhaustive, emit warning 8

With your constraint to call exhaustiveness only once, I would suggest the following:

1. If all clauses are guarded, consider all clauses with with their guard erased
   • if exhaustive, emit "bad style" warning 25
   • if not exhaustive, emit some variant of warning 8
2. Else, consider all clauses that are not guarded:
   • if exhaustive, pass
   • if not exhaustive, emit warning 8

Note that warning 8 already seems to be fairly clever in presence of some guarded clauses: it can tell whether one of the erased clause could have matched the proposed counter-example. I don't know how this is implemented (without checking exhaustiveness twice), but this aspect of the behaviour is good and need not change.

As I mentioned in my answer, this is not sufficient. The fact the guarded clauses are exhaustive after taking their guard does not mean the pattern-matching is exhaustive, and if all cases do not appear at least twice, it is probably not exhaustive.
If you have set -warn-error +8, you still want an error in that case.

I originally understood your remark as saying that my (or really Leo's) proposal was worse than what we currently have. If I understand correctly, you are saying that it is better, but that it could be improved further; with my last proposal, warning 25 is replaced by warning 8 in some cases, and you suggest to go even further by (reasonably) assuming that all guards may be either true or false for some values.

Your criterion is, however, not completely correct. Consider:

match blah with
| Some x when !Clflags.use_blah -> x
| None when !Cflags.use_blah -> failwith "missing blah"
| _ when not !Clflags.use_blah -> default_blah_value

This pattern-matching is exhaustive while no pattern is repeated twice: each value is matched by two distinct patterns. So a more complete refinement would be "every guarded pattern is included in the union of the other patterns" (otherwise whenever the guard is false the corresponding values raise match failure), and I don't suggest implementing it.

I don't think we need to enter the infinite bikeshedding hell of how to make this warning distinction perfect. The point is that today some users are surprised when they see the warning text of 25 instead of 8, and surprise is bad. If we can remove all cases where they are surprised, the problem is fixed.

Finally, you also remark that, if people set 8 as an error, they probably want 25 as an error as well. I think that is a reasonable idea. Let's hear some counter-arguments first. One may argue that people that are careful about this would have set 25 as an error as well; but it's fair to assume they haven't realized this is a problem (for the same reason our users are surprised). One may argue that raising an error (instead of a warning) in more cases is going to break code; but we are already proposing to turn some 25 into 8, which is going to break code as well.

So let me revise my proposition to take your remark into account -- bringing it closer to Alain's current change proposal.

1. If all clauses are guarded, consider all clauses with with their guard erased
   1. if exhaustive, emit Alain's 25-turned-8 warning variant talking about "bad style" (no exhaustiveness counter-example)
   2. if not exhaustive, emit some more precise variant of warning 8 (with exhaustiveness counter-example)
2. Else, consider all clauses that are not guarded:
   1. if exhaustive, pass
   2. if not exhaustive, emit warning 8 (with provision is some clauses are guarded)

Actually, your example precisely falls into my criterion. I've never said that the clause itself should be duplicated, but that all the values matched should be matched by at least two clauses, to have a chance of having something exhaustive.
My point is that it is too hard to do in practice, and that it would not guarantee exhaustiveness anyway.
So I don't see why we should do anything special about these "improbable by construction" pattern-matchings, other than marking them as non-exhaustive, with a statement of the reason.
Is there really any reason to support that kind of code?

Sorry, this was "unprovable" of course.
Giving a counter-example is misleading, because adding the corresponding clause will not make the pattern-matching exhaustive.

The counter-example says "Here is an example of a value that is not matched: ...", I don't think it would be misleading. But it is true that, in the cases we are discussing, adding all missing clauses still results in a warning (2.ii instead of 1.ii).

Sorry, the discussion is getting too long to follow... Do we all agree that as soon as warning 8 is enabled, one should never get a runtime failure because of a incomplete pattern matching? Since we are not going to analyze guard expressions, we must check exhaustivity after excluding clauses with guards (as of today) to be on the safe side. The "all clause guarded" is perhaps a bad style worth reporting by tweaking the warning text, but it should certainly trigger the "non exhaustive" warning.

Can participants to this discussion provide examples where the behavior implemented in the PR is not satisfactory?

Can participants to this discussion provide examples where the behavior implemented in the PR is not satisfactory?

  let f x y = match x with 1 when x = y -> 1;;
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
val f : 'a -> 'a -> int = <fun>

This is not satisfactory. I would like to see instead

  let f x y = match x with 1 when x = y -> 1;;
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
0
val f : 'a -> 'a -> int = <fun>

or even:

  let f x y = match x with 1 when x = y -> 1;;
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
0
Besides, all clauses in this pattern-matching are guarded.
val f : 'a -> 'a -> int = <fun>

This change of behaviour is precisely what the two Mantis tickets you linked to are asking for. (You and Jacques also interpret it, from a tooling perspective, thinking of situations where 8 is enabled but not 25, or where 8 is an error. This is also a valid concern and your change does improve things in this regard. But the users, at least for PR#6438, are actually asking for non-coverage counter-example(s).)

Edit: below is a my proposal for a warning logic that adresses this issue:

1. If all clauses are guarded, consider all clauses with with their guard erased
   1. if exhaustive, emit Alain's 25-turned-8 warning variant talking about "bad style" (no exhaustiveness counter-example)
   2. if not exhaustive, emit some more precise variant of warning 8 (with exhaustiveness counter-example)
2. Else, consider all clauses that are not guarded:
   1. if exhaustive, pass
   2. if not exhaustive, emit warning 8 (with provision if some clauses are guarded)

Thanks, this is clearer. So you are not arguing against the merger of warning 8 and 25, only about improving the text to show a certain counter-example. I propose to accept the current PR and postpone the discussion. FWIW, I don't like the "binary" logic you propose: if some clauses are non-guarded, it would still be useful to report certain counter-examples (i.e. values which are not matched by any clause even without taking their guard into account); I guess the argument against this approach is that running the check twice can be costly.

I propose to accept the current PR and postpone the discussion.

I'm not against this, but I suspect it corresponds to burying the issue.

FWIW, I don't like the "binary" logic you propose: if some clauses are non-guarded, it would still be useful to report certain counter-examples (i.e. values which are not matched by any clause even without taking their guard into account)

The current implementation is already rather good when there is a mix of guarded and non-guarded clauses

# type test = A | B | C;;
# function A when Random.bool () -> () | B -> ();;
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(A|C)
(However, some guarded clause may match this value.)

and I am not suggesting to change that. Indeed, calling coverage checking twice would be better in this case (to distinguish pattern C that we are sure are not covered and pattern A that is covered by a guard), but it costs and the benefits are not as clear as the changes discussed here.

In other words, the current compiler implements (2.i) and (2.ii) correctly. Your PR implements (1.i) (this arguably closes MPR#7059); I think we should implement (1.ii) as well (to close MPR#6438).

Ok, understood. But is anyone willing to spend time on providing a more helpful text for a discouraged style anyway? Perhaps this is burying the issue, but I prefer to fix now what I consider to be a bug (not getting warning 8 but having a runtime failure) and to leave the improvement I don't care about for later and/or someone else.

Btw, I was wondering if anyone would be opposed to turning warning 8 into an actual type-checking error? The idea that language features can implicitly raise exceptions is fine for a dynamically typed language, but it defeats the idea that statically well-typed program cannot go wrong. (I know there are other cases, such as recursive modules or circular lazy values, but they are more advanced stuff than pattern matching.)

Btw, I was wondering if anyone would be opposed to turning warning 8 into an actual type-checking error?

I am. Not that I would ever ignore it or turn it off, but because I think that type errors should be for genuine errors of soundness. I also don't think errors should be issued for things which cannot decidably be checked fully.

There are also various cases where you know by not-match-local reasoning that a case or family of cases cannot be reached (because you caught them in a matching on the same value that dominates this match's control flow); some people use _ -> assert false in this case, but others prefer clutter-free code (or even using let <pat> = ... when there is a single case), and it is reasonable that they can disable the warning on this match only.

Note that you can use a final _ -> . to turn unprovable-exhaustiveness into a hard error.

errors of soundness

For me, that's the difference between static and dynamic type systems: both "prevent segfaults", but dynamic type systems do it by allowing themselves to raise (or return dummy results) on apparently harmless operations, while static type system require users to be explicit about "dynamic checks".

while static type system require users to be explicit about "dynamic checks".

A warning still requires users to be explicit.

A warning still requires users to be explicit.

You mean, by explicitly ignoring the warning? But if the warning is not turned into an error, it is in practice invisible to many users, so I don't see how this can be qualified as an explicit action.

But if the warning is not turned into an error, it is in practice invisible to many users

My sympathy for users who ignore warnings is not particularly high.

If people accept warnings in their code base (i.e. they don't turn them into errors), they will necessarily have their console filled of them quickly and will thus soon enough start ignoring them. I guess that what I don't understand is the notion of warning not turned into errors; except for polluting the console, I don't see the point.

I guess that what I don't understand is the notion of warning not turned into errors; except for polluting the console, I don't see the point.

I agree, but warnings are still errors that you can turn on and off, as well as indicating (by the very fact you can turn them off) that they are not related to proper soundness.

Warnings are also generally ignored in released packages, which is good for things which check conditions that are undecidable in general or difficult to predict. I would be disappointed if my working program (inevitably featuring GADTs) was broken by a change to the exhaustivity check in the compiler, but such things can be inevitable when trying to check such awkward conditions.

Warnings are also generally ignored in released packages

They must be. There's nothing more annoying than packages failing to compile with a new release of the compiler because new warnings were introduced or tweaked since the last release of the package. -warn-error shouldn't never be used in the build system of distributed packages.

Reading again both #6438 and #7059, it seems to me that both reporters complain that warning 8 is not raised because of the guard, and that this is bad. So I've merged this PR. One could indeed refine the warning message when all clauses are guarded, but since this is considered bad style, I'm not sure it's worth the trouble.