Comment author: @yallop

Hmm. I'm not sure I agree that we should be giving a warning here. The pattern 'Left _' is valid in that context (since it doesn't introduce new type equalities) even if there are no values that match it (which is something we can't determine in general).

We also accept the following simpler examples, and should probably continue to do so, even though neither function can ever be called by a well-typed program:

Example 1 (note that replacing '_' with 'Refl' causes typechecking to fail):

type (_, _) eq = Refl : ('a, 'a) eq;;
let unexamined : (int, bool) eq -> unit = fun _ -> ()

Example 2 (no GADTs, but there's no value that can be bound to 'bottom'):

type empty = { bottom: 'a. 'a }
let ex_falso_quodlibet : empty -> 'a = fun { bottom } -> bottom

Comment author: @garrigue

The exhaustiveness check is known to be incomplete: it cannot prove all impossible cases to be impossible. So this is not really a bug.
This example comes from the fact it only tries to negate positions that are at least matched once, to avoid a combinatory explosion.
I'll try to see whether this can be improved, without changing the complexity.

Comment author: @garrigue

There is no real need to fix, as this is not a bug, but a more clever algorithm could help.

Comment author: @garrigue

The attached patch fixes the problem.
The idea is to expand gadts that appear as arguments to a non-gadt sum type.
(The restriction to non-gadt sum types is to avoid the need to backtrack unification)

In the above example it means that the missing pattern (Left _) is converted to (Left Refl), which is eventually disproved.
More experiments would be needed to see whether there is a large associated cost.

Comment author: @yallop

Is it possible to extend the patch to do a little more with redundancy? For example, the following code no longer gives an exhaustiveness warning:

let f : (int, (int, string) eql) sum -> unit =
function Left _ -> ()

but if you add a case for Right then there's no warning that it's redundant:

let f : (int, (int, string) eql) sum -> unit =
function Left _ -> () | Right _ -> ()

Comment author: @garrigue

The problem with redundancy is orthogonal.
The algorithm used there is a bit optimized, and doesn't take gadts into account.
It would be easy to just reuse the code for exhaustiveness, but this would mean repeating the same computation again for each extra line.

I personally never cared much about redundancy (it is not a soundness problem), but do you see cases where missing a warning makes a difference?

Comment author: @yallop

I think consistent warnings make a difference in understanding the code. Long-time ML programmers tend to interpret a lack of redundancy warnings as an indication that every branch is reachable.

It's useful to have the properties that

(1) removing cases from the end of an exhaustive match causes an exhaustivity warning
(2) adding cases to the end of an exhaustive match causes a redundancy warning

(Of course, guards already violate these properties, but I still think there's value in maintaining them as far as possible.)

Comment author: @garrigue

See #6437 for a more powerful patch.

Comment author: @garrigue

Branch gadt-warnings was merged in trunk at revision 16532.