The current mode_coerce has a soundness bug wrt its treatment of tuple_modes. The bug was exposed during development of #2741, but in the end worked around so it won't be exposed in that particular way.

It is still a bug and needs to be fixed. In this PR:

• The first commit adds some tests wrt tuple_modes.
• The second commit removes the workaround introduced by Migrate modes into the parsetree #2741 to expose the bug.
• The last commit fixes the bug.

The design

I tried to understand the current design of tuple_modes but found it difficult (partially because I've messed it up over time). So instead I came up with a new design that works as follows. Consider the example:

match e0, e1 with
| x0, x1 -> ..

The simplest design, which is to not have tuple_modes at all, is to have a single mode that will the mode of (e0, e1) and (x0, x1). That means if any of e0/e1 is local, both x0/x1 will be local. However, a typical ocaml programer thinks tuples as primitive langauge construct, and they would expect x0 to be global if e0 is global regardless of e1.

To that end, we consider a canonical example to motivate our design:

match if b then e0, e1 else e with
| x0, x1 -> ..
| x -> ..

We want the following two groups of mode constraints to hold.

regional_to_local(join(e0,e1)) <= x 
e0 <= x0
e1 <= x1 

OR equivalently:
e0 <= meet(x0, regional_to_global x)
e1 <= meet(x1, regional_to_global x)

e <= x0
e <= x1
e <= x

OR equivalently:
e <= meet(x, x0, x1)

The regional_to_local mapping is to represent allocation: if both e0 and e1 are regional, the tuple will be allocated in the current region local instead of the parent region regional. In implementation we move it to the RHS of <= as regional_to_global.

Following the existing design, we first look at the pattern: If the pattern is a tuple pattern, we create a mode variable mode for the tuple, and a list of mode variables tuple_modes corresponding to tuple fields. If the pattern is not tuple pattern, we let tuple_modes = None. Both mode and tuple_modes are used to construct expected_pat_mode and expected_mode, passed to patterns and expressions accordingly.

The type checking of patterns will try to make use of tuple_modes to get better modes; but it's sound to ignore that field. For the above example, x will enjoy mode, and [x0;x1] will enjoy tuple_modes.

The type checking of expression is responsible for enforcing the above constraints. If the expression is Pexp_tuple [e0; e1], we enforce the first group of constraints. Otherwise the expression is some general e, we enforce the second group of constraints. In any case, if tuple_modes = None, then we don't need to enforce the related constraints.

Note: it's unsound for the type-checking of expressions to ignore expected_mode.tuple_modes. Therefore, I replaced all usage of expected_mode.mode with as_single_mode expected_mode or get_single_mode_exn expected_mode. The former allows treating expected_mode as a single mode. The latter is used when we are sure tuple_modes will be None. To do this properly we should make expected_mode abstract (future work 😉 ).