Matching against GADT tuple when multiple patterns result in the same expression produces an error

[alex35mil]

I'm not sure if it's a bug or by design but match in fn produces an error:

type 'a t =
  | A: [ `a  | `z ] t
  | B: [ `b  | `z ] t

let fn: type a . a t -> a -> int = 
  fun x y ->
    match (x, y) with
    | (A, `a)
    | (B, `b) -> 0
    | (A, `z)
    | (B, `z) -> 1

Error: This pattern matches values of type [ `a | `z ] t
       but a pattern was expected which matches values of type a t
       Type [ `a | `z ] is not compatible with type a

P.S. I'm building against ocaml: ~4.6.1000

[nojb]

Thanks for the report. I tried to reproduce on trunk, but there it is even worse :) The code produces an assertion failure:

Fatal error: exception File "typing/patterns.ml", line 199, characters 21-27: Assertion failed

cc @trefis @garrigue

[alex35mil]

Building against recent version (~4.09.0) gives fatal error:

Fatal error: exception File "typing/parmatch.ml", line 777, characters 9-15: Assertion failed

[alex35mil]

@nojb Haha yeah, just tried against the recent version and got almost the same result.

[lpw25]

Note that the old behaviour was expected: GADTs did not support or-patterns until 4.08. The new behaviour (i.e. a fatal error) is obviously a bug.

[trefis]

Having had a brief look, I'm a bit surprised by this: in parmatch when deciding if a match on a polymorphic variant is exhaustive, we expand the type of the variant pattern, which we expect to be a variant type.
That seems sensible to me, but here apparently we do not get that (I assume that we get a Tconstr "a"), which wouldn't surprise me if we did the expansion in the outer environment, where the equation will have been dropped. But here we do it in the inner environment… could it be that unification didn't add the equation?

I'll look into it when it's not Sunday anymore.

[trefis]

Indeed the environment is not the one I expected, due to this line:

ocaml/typing/typecore.ml

Line 1887 in ea16b1c

map_general_pattern { f = fun p -> { p with pat_env = !env } } r

Which was first introduced in commit: ff78b8e

If I remove that line, everything works fine.
I'll open a PR.