"Dependent elimination failed" when index accesses struct field

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

When a type's index is defined in terms of an argument's structure field, a straightforward match or cases on its values will fail.

Context

Lean Zulip discussion

Steps to Reproduce

In the following program, type Term : Nat -> Type's first case boxed gets the index indirectly from the argument's field Box.value. Definitions f₁, f₂, f₃ attempting to pattern match on two values of the same type Term n fail (using wild card, inaccessible patterns, and just the constant literals, respectively).

structure Box where
  value : Nat

inductive Term : Nat → Type u where
| boxed : (b : Box) → Term b.value
| base : Term 0

def f₁ : Term n → Term n → Unit
| .boxed ⟨_⟩, .boxed ⟨_⟩ => ()
| .base, .base => ()
| .boxed ⟨_⟩, .base => ()
| .base, .boxed ⟨_⟩ => ()
/-
dependent elimination failed, failed to solve equation
  0 = b✝.1
at case Term.boxed after processing
  _, Term.base, _
-/

def f₂ : Term n → Term n → Unit
| .boxed ⟨k⟩, .boxed ⟨.(k)⟩ => ()
| .base, .base => ()
| .boxed ⟨.(0)⟩, .base => ()
| .base, .boxed ⟨.(0)⟩ => ()
/-
dependent elimination failed, failed to solve equation
  0 = b✝.1
at case Term.boxed after processing
  _, Term.base, _
-/

def f₃ : Term n → Term n → Unit
| .boxed ⟨k⟩, .boxed ⟨.(k)⟩ => ()
| .base, .base => ()
| .boxed ⟨0⟩, .base => ()
| .base, .boxed ⟨0⟩ => ()
/-
dependent elimination failed, failed to solve equation
  0 = b✝.1
at case Term.boxed after processing
  _, (Term.boxed (Box.mk 0)), _
-/

Robin Arnez also points out on Zulip that a cases on Term 0 will also fail with the same error:

example (x : Term 0) : Unit := by
  cases x
/-
dependent elimination failed, failed to solve equation
  0 = b✝.1
-/

Kyle Miller points out a workaround on Zulip:

def fAux : Term m → Term n → m = n → Unit
| .boxed ⟨k⟩, .boxed _, rfl => ()
| .boxed ⟨.(0)⟩, .base, rfl => ()
| .base, .boxed ⟨.(0)⟩, rfl => ()
| .base, .base, rfl => ()

def f (t t' : Term n) : Unit := fAux t t' rfl

Expected behavior:
Pattern matching succeeds, with either the wild card or the explicit inaccessible patterns.

Actual behavior:
Errors that equation 0 = b.value cannot be solved.

Versions

Lean 4.21.0
Target: arm64-apple-darwin23.6.0 macOS

Also Lean nightly on live.lean-lang.org

Impact

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

Start with the minimal Box, Term, f₁, f₂, and f₃ reproducer, then compare its pattern matching and cases behavior with the fAux workaround. Confirm the failure on Lean 4.21.0 or nightly. Done means the wildcard or inaccessible patterns compile without the dependent-elimination error, with regression coverage for the shown cases.