RFC: divide-and-conquer match compilation

Issue 1: Duplicated code

If a match statement has multiple alternatives, and the first pattern can fail in two ways, then the reminder of the pattern is currently compiled twice.

Consider this example:

inductive N where | z | s (n : N)

def anyTwo : N → N → Bool
  | .s .z, _     => true
  | _,     .s .z => true
  | _,     _     => false

/--
info: def anyTwo.match_1.{u_1} : (motive : N → N → Sort u_1) →
  (x x_1 : N) → ((x : N) → motive N.z.s x) → ((x : N) → motive x N.z.s) → ((x x_2 : N) → motive x x_2) → motive x x_1 :=
fun motive x x_1 h_1 h_2 h_3 =>
  N.casesOn x (N.casesOn x_1 (h_3 N.z N.z) fun n => N.casesOn n (h_2 N.z) fun n => h_3 N.z n.s.s) fun n =>
    N.casesOn n (N.casesOn x_1 (h_1 N.z) fun n => N.casesOn n (h_1 N.z.s) fun n => h_1 n.s.s) fun n =>
      N.casesOn x_1 (h_3 n.s.s N.z) fun n_1 => N.casesOn n_1 (h_2 n.s.s) fun n_2 => h_3 n.s.s n_2.s.s
-/
#guard_msgs in
#print anyTwo.match_1

The subexpression starting with N.casesOn x_1 … is essentially duplicated three times. This can quickly blow up.

Issue 2: Refined match compilation breaks dependent pattern matching

Another issue with the current compilation approach is shown by

inductive Parity : Nat -> Type
| even (n) : Parity (n + n)
| odd  (n) : Parity (Nat.succ (n + n))

/--
error: Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern
  .(j + j)
-/
#guard_msgs in
partial def natToBin : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| .succ 0, _       => [true]
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

This dependent pattern match goes through if the first two alternatives are not there (and it goes through with just the first one once #10823 is merged). But it fails if written as is, because if n := .succ (.succ _), then the second pattern falls through, but now n is no longer a variable and dependent cases fails.

Proposed solution

Based on these examples, it is desirable that

• the remainder of a match statement is only compiled once, independent of how alternatives further up can fail
• a failing pattern must not affect how further alternatives are compiled, in particular, no refining from case splitting should happen.

The proposed solution would be to introduce a join-point for the “remainder” of the match, and essentially transform

match x with
| pat1 => 
| pat2 => 
| pat3 => 
| pat4 => 

to

have cont :=
      match x with 
      | pat3 => 
      | pat4 => 
match x with
| pat1 => 
| pat2 =>
| _ => cont

whenever

• pat1 … pat2 are constructors
• pat3 is not a constructor pattern
• pat3 is not a final catch-all pattern

Difficulties

The above transformation works fine if pat4 is a catch-all pattern (as in the first example); see #11105 for an experiment.

If not, then we would have to pass to cont a proofs of x = pat1 → False, x = pat2 → False in case these assumptions are needed for the final completeness proof. This seems doable, but adds a considerable amount of bookkeeping to the translation

The other difficulty is that the way splitter generation works right now is not really compatible with that scheme. Even if splitter proof generation zeta-reduces the have it doesn't work yet, because the cont is generalized by mvarId.cases during the match compilation of pat1, so the extra proof obligation that the splitter has to provide to its alternatives cannot be proven.

Maybe fixing the first issue will actually also address the second (and even without zeta-reducing), because it precisely puts the no-overlap assumptions into the context of cont’s body that are needed there 🤔

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with the match-compilation and splitter-generation behavior described in the examples, including mvarId.cases, and compare the proposal with the experiment in #11105 and the context in #10823. Done means compiling the remainder only once while preserving dependent pattern matching and the completeness obligations for non-catch-all alternatives.