failed to generate equality theorem for `match` expression with array patterns

A sub-issue of https://github.com/leanprover/lean4/issues/9713 is that match statements with array patterns fail to produce equations:

def testMatch : Array α → Unit
  | #[a] => ()
  | _ => ()

/--
error: Failed to realize constant testMatch.match_1.eq_1:
  failed to generate equality theorems for `match` expression `testMatch.match_1`
  case isTrue
  α✝ : Type u_1
  motive✝ : Array α✝ → Sort u_2
  x✝¹ : Array α✝
  h_1✝ : (a : α✝) → motive✝ #[a]
  h_2✝ : (x : Array α✝) → motive✝ x
  x✝ : ∀ (a : α✝), x✝¹ = #[a] → False
  h✝ : x✝¹.size = 1
  ⊢ (⋯ ▸ fun h => ⋯ ▸ h_1✝ (x✝¹.getLit 0 ⋯ ⋯)) ⋯ = h_2✝ x✝¹
---
error: Unknown constant `testMatch.match_1.eq_1`
-/
#guard_msgs in
#print testMatch.match_1.eq_1

Version

Lean 4.23.0-nightly-2025-08-11

Impact

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

Start by reproducing the testMatch definition and its #guard_msgs/#print testMatch.match_1.eq_1 checks from the issue. Investigate the compiler path that generates equality theorems for match expressions with array patterns. Done means the equality theorem is generated and the guarded output no longer reports the failed realization or unknown constant.