split fails on Array matches

[digama0]

def foo {α} : Array α → Array α 
  | #[a] => #[a]
  | as => as

theorem foo_eq {α} (as : Array α) : foo as = as := by
  unfold foo; split <;> rfl -- split failed

Using simp [foo] instead gives the more helpful error message failed to generate equality theorems for `match` expression `foo.match_1` .

Tested on Lean (version 4.7.0-nightly-2024-02-23, x86_64-unknown-linux-gnu, commit 5a32473f6695, Release)

[Kha]

Now covered by #5339