deriving `DecidableEq` fails with failure of dependent elimination

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

Consider:

inductive BVExpr : Nat → Type where
  | append (lhs : BVExpr l) (rhs : BVExpr r) : BVExpr (l + r)
  deriving DecidableEq

This errors out with:

tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  l✝¹.add r✝¹ = l✝.add r✝
at case BVExpr.append after processing
  _, (BVExpr.append _ _ _ _), _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

I would love this to work but also to at least throw a nice error message.

Context

Work on bv_decide.

Steps to Reproduce

1. Copy code
2. Boom

Expected behavior: The instance should be synthesized or at least a good error be thrown if it isn't possible.

Actual behavior: Incomprehensible error message to users that aren't aware of the internals.

Versions

Lean 4.19.0-nightly-2025-03-19
Target: x86_64-unknown-linux-gnu

Impact

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

Start by reproducing the minimal BVExpr example with deriving DecidableEq on the specified Lean nightly release, then inspect the dependent pattern-matching and deriving paths involved in the reported failure. Done means either the DecidableEq instance is synthesized for this case or the failure is replaced with an understandable diagnostic explaining the limitation.