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

/--
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✝ : (head : α✝) → motive✝ #[head]
  h_2✝ : (x : Array α✝) → motive✝ x
  x✝ : ∀ (head : α✝), x✝¹ = #[head] → 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