The Pattern-Matching Bug: fix totality information

[gasche]

This PR is part of the #7241 fix; it is the first un-merged PR in the stack and is ripe for review.)

#13138 introduces information on the "transitive mutability" of argument positions in pattern-matching submatrices: an argument is transitively mutable if it is located transitively under a mutable field (from the root of the value).

The present PR uses this information to pessimize the compilation of switches generated by the pattern-matching compiler. All switches that are in a transitively mutable position are assumed to be Partial, even if the type-checker says that they are Total. (If you want, there is a longer explanation as a code comment in the PR itself.)

This change fixes all known remaining instances of the issue describe in #7241 (unsound interaction between pattern-matching and mutation), in particular all known-wrong behaviors in the testsuite.

(TODO: this is missing a Changes entry.)

Degradation in generated code

The code generated by the pattern-matching compiler will be degraded if the following conditions are all met:

1. The position is transitively mutable.

2. At the position that we are generating a switch for, a language construction is used for which Total improves the quality of generated code. This can happen if either (A) only a strict subset of possible constructors is handled at in this submatrix, with the rest having been handled before, or (B) all valid constructors are handled by this submatrix, but this relies on checking that GADT equations are unsatisfiable, and the pattern-matching compiler does not know this. (On the other hand, the pattern-matching compiler does know about the set of constructors possible for a non-GADT sum type or for closed polymorphic variants.)

So the affected code looks like one of those:

(* case (A) above *)
let f : bool option ref -> ... = function
| { contents = None } -> ...
| { contents = Some true } -> ...
| _ when guard () -> ...
| { contents = Some false } (* here *) -> ...

type _ gadt = Int : int t | Bool : bool t

(* case (B) above *)
let g : int gadt ref -> ... = function
| { contents = Int } (* here *) -> ...

In the case (A) (example f), the behavior was previously unsound (in particular if we consider concurrent mutations). There are instances of (B) (example g) where the compiler was sound, and now generates slightly worse code -- the function g above is one such example -- by including a test with a Match_failure case.

In a follow-up PR I implement a simple heuristic that re-optimizes the compilation of some GADT matchings in mutable position, so that the function g above is not pessimized anymore.