One reason to disable the partiality check when the warning is off is that the check itself can be costly.
Before turning it off we should check that there is a simple way to avoid this check (for instance by adding a failing catch-all clause at the end, which is equivalent to assuming it is partial without warning).

Yes indeed.
IIUC get_mins will reduce any matrix containing a "wildcard row" to just that row.
However if the matrix contains n rows it will require O(n²) calls to le_pats to do that reduction, which might be costly.

We could make it quicker by explicitly looking for a wildcard row at the start of get_mins and reduce then. Such a check would be linear in the number of patterns in the matrix I believe (the worst case being when there is no such "wildcard row"/catch-all clause).
However Luc already considers such an optimization in section 7.2 of this paper before settling for the more generic, though more costly, one.
It could be argued that we should revisit this choice, since we previously had the option of avoiding all the cost of the check and we don't anymore. I'm not too keen on the idea, but someone might have a different/more informed opinion?

(N.B. by "revisit this choice" I mean "have both safe guards")

One reason to disable the partiality check when the warning is off is that the check itself can be costly.

Is anyone aware of people actually disabling the partiality check (resp. doing so for compilation-time performance)?

I reviewed the code and I believe that the proposed code is correct (I'm not sure the previous behavior was fully equivalent, see comment above). On the other hand, I find Jacques' performance concern interesting and I would like to have some information on that before considering a merge.

@trefis, could you measure the time of "make world" with the patch applied, versus the time of "make world" without the patch and with all exhaustivity warnings disabled? Is there a noticeable difference? (Note: this uses only bytecode compilation, as native code production would risk drowning out this cost, and this is assuming that the OCaml compiler code is somewhat representative of average code full of pattern matchings -- but it doesn't tell us anything about degenerate cases.)

I would be interested in having the heuristic you describe implemented (not doing any check when there is an all-omega row), but I don't really understand your comment on get_mins (or rather, cursorily looking at the code did not help me locate this function as the place to change). Do I correctly understand that only exhaust_gadt is ever used (the non-_gadt variants are commented out and never used), and that it is the function to change to apply the heuristic? I don't see how it relies on get_mins, how does that work?

Thanks for having a look :)

For the "benchmark" you propose I doubt we'd notice much difference on the compiler but I don't mind trying it. Question though: to test compiling the compiler with a compiler containing these patches, do I want to make bootstrap or something of the sort? ( ping @adrien-n who also knows about this sort of things).

Btw, #1195 is not the first bit of code using the partiality information stored in the typedtree: if I am not mistaken bytecomp/matching.ml also relies on this information to do some optimizations (Optimizing pattern matching (I love the anchor name btw) says for example that you can eliminate the branch raising Match_failure if you know the matching is exhaustive).

I wouldn't change exhaust: it does what it's supposed to do, why obfuscate it with unrelated heuristics?
get_mins gets called from check_partial just before we call exhaust. The function is already charged of reducing the matrix (see section 7 of Warnings for pattern matching on pages 26 to 28 for a detailed explanation of what get_mins does).
My previous comment only proposed to make that reduction quicker; the reason being that exhaust is (I believe) going to run fast on a matrix reduced to a single wildcard row, while performing the reduction to such a matrix will be expensive.

Rather than the whole compiler, it would probably be sufficient to test compiling the stdlib, as it contains a lot of GADT code (this is where I saw most of the difference when I changed the exhaustivity check).

I compiled the stdlib a few times with trunk and with the this branch.
The results are as expected, i.e. there is no noticeable difference.

I then compiled camlinternalFormat.ml a bunch of times with both compilers, as it contains some GADT matching.
There is a difference here, but I would say it's negligeable.

Of course, there's AFAIK nothing in these test cases which would exhibit the degenerate behavior of parmatch...

stdlib

Warnings 4, 8, 25 disabled (using this patch).

$ make clean && time make -j1

trunk

GPR1227

camlinternalFormat

$ time for i in {1..20}; do ../boot/ocamlrun ../ocamlc -strict-sequence -absname -w +a-4-8-9-25-41-42-44-45-48 -g -warn-error A -bin-annot -nostdlib -safe-string -strict-formats -w Ae-4-8-25 -c camlinternalFormat.ml; done

Btw, I think the second commit actually has no impact at all.
While the first commit does not appear to be correct, I believe it actually is as Location.prerr_warning actually checks that the warning is active before printing anything.

FWIW, I asked internally at facebook and no one admitted to disabling the partiality check. The potential of missed optimization seemed to be considered a much more important "gotcha". So support for this PR on those grounds.

@maranget should look at this PR and confirm, but as far as I remember the worst case is exponential in the size of the matching. A workaround that is quadratic is no big deal.

@garrigue and @xavierleroy are right: adding a catch all clause at the end of a matching will
reduce the cost from a (potential) exponential to a certain quadratic. Given experiments, It does not seem useful to add code for reducing this to constant cost (or linear, the catch all clause is at the end of a list...). As usual, some future PR may call for this extra cost decrease on an "example of interest".
Let us wait for this.

My real objection against @garrigue suggestion is: if the matching was exhaustive then we'll have a unsused match clause warning. But again, this is a potential problem not a reported one.
A real and complete solution would be a specific option that would disable PM analysis attogether.
Such an option might be useful for compiling generated code.

So I'll (squash and) merge the patch(es).