Failed to generate equality theorems

[rami3l]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Pasted from Zulip:

inductive Ty where
| star: Ty
notation " ✶ " => Ty.star

abbrev Context : Type := List Ty

inductive Lookup : Context → Ty → Type where
| z : Lookup (t :: Γ) t

inductive Term : Context → Ty → Type where
| var : Lookup Γ a → Term Γ a
| lam : Term (✶ :: Γ) ✶ → Term Γ ✶
| ap : Term Γ ✶ → Term Γ ✶ → Term Γ ✶

abbrev plus : Term Γ a → Term Γ a
| .var i => .var i
| .lam n => .lam (plus n)
| .ap (.lam _) m => plus m -- This case takes precedence over the next one.
| .ap l m => (plus l).ap (plus m)

-- I wish to be able to prove the following "by definition":
example : plus (.ap l m) = (plus l).ap (plus m) := by
  unfold plus
--^^ failed to generate equality theorems for `match` expression `plus.match_1`

Expected behavior: The plus definition gets unfolded. IIRC since it's recursive, it should be unfolded only once.

Actual behavior: The last line generates the following error message:

failed to generate equality theorems for `match` expression `plus.match_1`
Γ : Context
a : Ty
motive : Term Γ a → Sort u_1
n : Term ( ✶ :: Γ) ✶
h_1 : (i : Lookup Γ a) → motive (Term.var i)
h_2 : (n : Term ( ✶ :: Γ) ✶ ) → motive (Term.lam n)
h_3 : (a : Term ( ✶ :: Γ) ✶ ) → (m : Term Γ ✶ ) → motive (Term.ap (Term.lam a) m)
h_4 : (l m : Term Γ ✶ ) → motive (Term.ap l m)
⊢ Eq.rec (fun x motive h_1 h_2 h_3 h_4 h => (_ : Term.lam n = x) ▸ h_2 n) (_ : ✶ = a) (Term.lam n) motive h_1 h_2 h_3 h_4
      (_ : HEq (Term.lam n) (Term.lam n)) =
    h_2 n

Reproduces how often: 100%

Versions

lean-toolchain: leanprover/lean4:nightly-2023-05-16 OS: macOS Ventura 13.4 22F66 arm64

[nomeata]

Still the case with Lean 4.18.0-nightly-2025-02-11.

[nomeata]

The error message is similar to #9846, so when fixing one of the two, check the other!

[nomeata]

Ah, there is a simple workaround in this case: Explicitly include the index in the pattern matching:

def plus (t : Term Γ a) : Term Γ a := match a, t with
| _, .var i => .var i
| _, .lam n => .lam (plus n)
| _, .ap (.lam _) m => plus m -- This case takes precedence over the next one.
| _, .ap l m => (plus l).ap (plus m)