Allow retyping as-patterns that contain existentials

[OlivierNicole]

This is oxcaml/oxcaml#3374. It lifts certain restrictions on existentials in as-patterns as the title says—see also the added test. I am opening this PR as part of the partnership between Tarides and Jane Street to reduce their diff with upstream.

Disclaimer: I am not sufficiently versed in GADTs to validate whether this change is sound.

[nojb]

cc @garrigue: what do you think about this change?

[OlivierNicole]

This seems to cause a regression: it seems to prevent from mixing constructors with an existential type and constructors without:

type 'a boxed_int

type t =
  | Value_int of int
  | Value_boxed_int : 'a boxed_int -> t

let f (x : t) : t =
  match x with
  | Value_int _ | Value_boxed_int _ as y -> y

Line 9, characters 34-35:
Error: This pattern matches values of type "$a boxed_int"
       but a pattern was expected which matches values of type "'a boxed_int"
       The layout of $a is any
         because the .cmi file for $a is missing.
       But the layout of $a must be a sublayout of value
         because of the definition of t at lines 3-5, characters 0-39.
       No .cmi file found containing $a.

This error is triggered on this PR and on current OxCaml (5.2.0+jst), but not on trunk.

Cc @TheNumbat

[gasche]

As a first step, a PR to add this example to the testsuite would be welcome.

[TheNumbat]

It's expected that this isn't quite backwards compatible--internally, there were a couple places where we had to split match cases to fix that error. Not sure if that poses a problem for upstreaming, but probably need to check if breaks opam packages.

[garrigue]

I think this needs to be carefully thought out.
There reason I introduced this restriction is probably related to your counter-example.
My position is that as-pattern retyping should not break existing code, even if it is sound otherwise.

[garrigue]

To clarify: I agree with @gasche, we should first see what this change breaks, if there are already known examples.
I suppose I could also come up with one myself, but this sounds like a loss of time if they are readily available.

[OlivierNicole]

As a first step, a PR to add this example to the testsuite would be welcome.

I’m not fully sure which example you mean, between the test from the PR or the example I posted.

[garrigue]

Sorry, you had indeed given the example.
For me this is a show stopper.
Retyping as-patterns is a refinement of the typing of patterns, so it should not break code that would work without it (at least in principal mode).
I don't know if there is a way to do it in presence of existentials without breakage.