"Failed to generate splitter"

[Smaug123]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

simp and unfold are unable to unfold certain functions.

Context

Discussion on Zulip.

(Seen in the wild while editing a file in Mathlib.)

Steps to Reproduce

On https://live.lean-lang.org/, type the following:

def thingy : List (Nat ⊕ Nat) → List Bool
  | Sum.inr (n + 2) :: l => thingy l
  | _ => []
  termination_by l => l.length

theorem thingy_empty : thingy [] = [] := by
  unfold thingy

Expected behavior:
Error "Unsolved goals: [] = []"

Actual behavior:

failed to generate splitter for match auxiliary declaration 'thingy.match_1', unsolved subgoal:
case x
motive : List (Nat ⊕ Nat) → Sort u_1
x✝ : List (Nat ⊕ Nat)
h_1 : (n : Nat) → (l : List (Nat ⊕ Nat)) → motive (Sum.inr n.succ.succ :: l)
h_2 : (x : List (Nat ⊕ Nat)) → (∀ (n : Nat) (l : List (Nat ⊕ Nat)), x = Sum.inr n.succ.succ :: l → False) → motive x
head✝ : Nat ⊕ Nat
val✝ n✝ n : Nat
l : List (Nat ⊕ Nat)
n_eq : 0 = n + 1
⊢ False

Versions

Tested on "4.11.0-rc2" and on "4.12.0-nightly-2024-08-15".

Additional Information

Deleting the termination_by, or turning the 2 into a 1, makes this go away.

Impact

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