failed to generate equality theorem when mixing patterns on index and indexed type

Matches that mix pattern matching on indexed types as well as their indices are notorious tricky. Here is another example:

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


partial def natToBin3 : (n : Nat) → Parity n →  List Bool
| 0, _             => []
| _, Parity.even j => [false, false]
| _, Parity.odd  j => [true, true]

/--
error: Failed to realize constant natToBin3.match_1.splitter:
  failed to generate equality theorems for `match` expression `natToBin3.match_1`
  motive✝ : (x : Nat) → Parity x → Sort u_1
  j✝ : Nat
  h_1✝ : (x : Parity 0) → motive✝ 0 x
  h_2✝ : (j : Nat) → motive✝ (j + j) (Parity.even j)
  h_3✝ : (j : Nat) → motive✝ (j + j).succ (Parity.odd j)
  x✝ : ∀ (x : Parity 0), j✝ + j✝ = 0 → Parity.even j✝ ≍ x → False
  ⊢ Nat.rec (motive := fun t =>
        (Nat.hasNotBit 1 t.ctorIdx → (fun x => (x_1 : Parity x) → motive✝ x x_1) t) →
          (fun x => (x_1 : Parity x) → motive✝ x x_1) t)
        (fun x x_1 => h_1✝ x_1) (fun n n_ih x => x ⋯) (j✝ + j✝)
        (fun h x =>
          Parity.casesOn (motive := fun a x_1 => j✝ + j✝ = a → x ≍ x_1 → motive✝ (j✝ + j✝) x) x
            (fun n h_1 =>
              Eq.ndrec (motive := fun x =>
                Nat.hasNotBit 1 x.ctorIdx → (x_1 : Parity x) → x_1 ≍ Parity.even n → motive✝ x x_1)
                (fun h x h_2 => ⋯ ▸ h_2✝ n) ⋯ h x)
            (fun n h_1 =>
              Eq.ndrec (motive := fun x =>
                Nat.hasNotBit 1 x.ctorIdx → (x_1 : Parity x) → x_1 ≍ Parity.odd n → motive✝ x x_1)
                (fun h x h_2 => ⋯ ▸ h_3✝ n) ⋯ h x)
            ⋯ ⋯)
        (Parity.even j✝) =
      h_2✝ j✝
---
error: Unknown constant `natToBin3.match_1.splitter`
-/
#guard_msgs in
#print sig natToBin3.match_1.splitter

That the match statement even compiles is somewhat new, a side-effect of #10823. But then the equation theorem calculation goes wrong.

The problem is that the matcher is doing case analysis on (j✝ + j✝) which proveCondEqThm is not able to make progress on.

Maybe it would be able to make progress by generalizing the scrutinee ((j✝ + j✝)), notice that one branch is unreachable (using x✝ : ∀ (x : Parity 0), j✝ + j✝ = 0 → Parity.even j✝ ≍ x → False) and then continuing. But it’s tricky, and this is a somewhat obscure function, so for now just recording this here.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the natToBin3 example and inspect the matcher and equation-theorem generation around proveCondEqThm, especially the handling of the (j✝ + j✝) scrutinee. The issue suggests generalizing that scrutinee and using the unreachable branch; done means the equality theorem is generated and #guard_msgs no longer reports an unknown splitter constant.