From the patch I have no idea what the problem really is, and I find it very surprising that the problem is specific to extension constructors (there is no rebinding going on for example). Why is forget_extension_with_arg a good idea (can you remind us what as_matrix is doing?).

The fix you comment was not a good idea, I have committed a new fix. The new fix simply avoids to extract arguments from pattern matrices when type mismatch on arguments may occur. A more radical fix would change the approximate constructor equality function Types.may_equal_constr, so that, when it returns true, the types of pattern arguments are guaranteed to be equal, or compatible. I do not know how to do that.

Now that you understand the bug, does the reproduction case really need to be that large, or can you write a smaller program that runs in the same argument-typing issue with extension constructors?

This can be done, but well...

The point in a smaller repro case is that it also increases the chance that someone else than you understands what the problem is: looking at the repro case is an interesting part of understanding the whole fix when the repro case has no unnecessary cruft that obscures understanding.

From your second message I understand the problem better: because we equate A (pa, qa) and B (pb, qb) without looking at the types of the sub-patterns, it may be that they are incompatible and that pa, pb could form a column matching on variant constructors from distinct types.

I find it ironic that this seems very related to the refinement of may_equal_constr that I suggested in the first patch. Note that we cannot restrict may_equal_constr to only equate patterns whose arguments have equal types, because the types on one side may be abstract and not known to be equal to the other:

type t = A | B
exception Foo of t

module M : sig
  type u
  exception Bar of u
end = struct
  type u = t
  exception Bar = Foo
end

Types, like patterns, can be "equal", "known to be different" ("incompatible"), and "maybe equal" ("not incompatible"), so two extension constructions with not-incompatible types may be equal.

If my intuition of what you say is correct, the issue here only comes up when argument types on both sides can have sub-patterns that clearly belong to distinct types, and this is only possible if the types are really incompatible; so maybe accepting in may_equal_constr argument types that are not incompatible but are not known to be equal either is not an issue, and the further restriction I previously suggested is a good fix.

If my intuition of what you say is correct, the issue here only comes up when argument types on both sides can have sub-patterns that clearly belong to distinct types, and this is only possible if the types are really incompatible; so maybe accepting in may_equal_constr argument types that are not incompatible but are not known to be equal either is not an issue, and the further restriction I previously suggested is a good fix.

It may be a good fix, but I do not know to implement it.

It may be a good fix but I do not know to implement it.

I might give it a try tomorrow, I have a long flight ahead of me.

Btw, a smaller code reproducing the problem could be:

# type t1 = { x : int; y : string }
  type t2 = { a : int; b : string; c : string list };;
type t1 = { x : int; y : string; }
type t2 = { a : int; b : string; c : string list; }
# type t = ..
  type t += C1 of t1 | C2 of t2;;
type t = ..
type t += C1 of t1 | C2 of t2
# let f (x : t) = match x with C1 { x; y } -> () | C2 { a;b;c } -> () | _ -> ();;
Fatal error: exception Invalid_argument("index out of bounds")
...

Note: the central code pattern in the last fix proposed by Luc

if Types.may_equal_constr cstr cstr' then begin
  if Types.equal_tag cstr.cstr_tag cstr'.cstr_tag
  then ...
  else ...
end else ...

would have been nicely represented as pattern-matching on a three-way return type:

match Types.compare_constr cstr cstr' with
| Equal -> ...
| Compatible -> ...
| Incompatible -> ...

Ok I use @trefis example as an additional test.

I had a look at how to define a "non-incompatibility test" for types, and it's not easy to implement (just as @maranget thought!). In particular, the comment #1468 (comment) by @garrigue suggests that mcomp (which I thought, after looking at ctypes.ml a bit, was the right thing to use) is not as convincing as it looks.

In this context, I agree with the idea of finishing the current patch and merging it (to fix the issue), before we try to refine may_equal_constr using type information.

I think the underlying issue here was misunderstood (the bug can be reproduced without matching on extensible types) and this PR, while fixing the issue in the context of extensible variants is incomplete.

Before getting into more details, I'd like to clarify the context. If I understand the issue correctly, I think @gasche's previous intuition

From your second message I understand the problem better: because we equate A (pa, qa) and B (pb, qb) without looking at the types of the sub-patterns, it may be that they are incompatible and that pa, pb could form a column matching on variant constructors from distinct types.

is not exactly correct/correctly formulated: we never have pa, pb in a column.
The issue happens when specializing/refining our list of reachable trap-handlers.

One could then assume that the issue is that because of extensible types we've allowed things of incompatible types (that is: unreachable trap handlers) to remain in our list of reachable trap handlers and that is what causes our specializing function to crash (because it makes the assumption that things are of the same type).

In this PR, Luc proposes to fix this problem by making the matrices we put in our list of reachable trap handlers more lax when specializing with constructor of extensible types, to avoid such issues in recursive calls (which IIUC means that we're disabling optimizations allowing us to skip some tests).

However:

• If the stated problem is the actual one, then the following code should trigger the bug as well:

  type r = { x : int; y : int; }
  
  type t = ..
  type t += I of int | R of r
  
  let f (x : t) =
    match I 2 with
    | I 3 -> ()
    | R { x; y } -> ()
    | _ -> ()

  But it doesn't.

  In this case, when specializing our list of reachable trap-handlers we end up checking the compatibility of 3 with { x; y } and conclude that they don't match (and so we can eliminate that element from our list).
  The specialization function seems robust enough to handle matrices filtering values of different types and the issue seems to be limited to the comparison of records of different types.

• Extensible types are not the only thing that can allow unreachable branches to remain in the list of reachable trap-handlers.
  The following code, which doesn't use extensible types, exercises the same bug:

  type r1 = { x : int; }
  type r2 = { a : int; b : int; }
  type _ repr = R1 : r1 repr | R2 : r2 repr
  let f (type a) (r1 : a repr) (r2 : a repr) (a : a) =
      match r1, r2, a with
      | R1, _, { x } -> ()
      | _, R2, { a; b } -> ()
      | _ -> ()

Considering this I would suggest

• making matcher_record more robust by catching Invalid_argument and raising NoMatch instead.
• not including the changes proposed in this feature because it would then become unneeded (and, I believe, implies potentially generating more tests than necessary)
• do the required change in a separate PR with a name that reflects the underlying problem, as it is indeed unrelated to MPR#7661

@trefis "Bien vu", I need to think about it, I acknowledge you comment.

Another one:

type _ repr = R1 : int repr | R2 : string repr

let f (type a) (r1 : a repr) (r2 : a repr) (a : a) =
    match r1, r2, a with
    | R1, _, 0 -> ()
    | _, R2, "coucou" -> ()

yields "assertion failed" somewhere in parmatch. The fact is that PM code assumes that patterns of different types "just don't mix". Obviously, this is untrue.

Note: the fact that jbuilder is broken in trunk is actually a Big Deal, because it blocks a lot of software from building on trunk. I think we should seriously consider a short-term way to make this particular issue go away; for example (to start a discussion), I propose to revert the change of #1459 while a solution here is being worked out.

I propose to revert the change of #1459 while a solution here is being worked out.

I wouldn't do that.
As Luc noted, the problem is pervasive in matching and parmatch and might take some work to properly fix everywhere, however if you're just worried about making jbuilder compile, the particular instance of records of different lengths should be easy to fix. I wouldn't reintroduce a bug causing miscompilation for that.

We know of no code in the wild that is affected by the miscompilation bug (some may exist, but we don't know about it, and the fact that the bug was undercover for so long suggests that no path that people actually test is affected). Keeping the bug in trunk for a few more weeks seems harmless to me.

The alternative you propose requires (1) to prepare a PR for jbuilder to work-around that may reduce code readability and will only ever makes sense for a couple week, (2) explain to the jbuilder developers why they should merge this PR while their code is obviously correct, (3) make a release of jbuilder to reach opam-repository. This is strictly more work for a handful of people and, I think, not a good example of how upstream should deal with its own issues.

Sorry, I wasn't actually suggesting to "fix" anything in jbuilder.
I just meant we could make that particular part of matching.ml more robust, as it fixes an actual problem people have encountered in practice, while we work on properly fixing the bigger issue that doesn't seem to be hurting people yet (at least that we know of).

Oh, I misunderstood. That sounds reasonable to me. If you can make a fix to unblock jbuilder, is not a waste of time, and is submitted and reviewed relatively swiftly (this week? next week?), I think that's a good option. If that does not sound realistic, then I will propose reverting again.

Just FYI I've started working on a full fix.
I believe I've fixed all such issues in parmatch (it was fairly easy) and I am now working on a proper fix for matching (basically, everything going through divide_line can be made to fail).

I'll make a PR before the end of the day (potentially with some bits left missing).

Superseeded by #1538 .