Deriving DecidableEq fails in implicit argument

[b-mehta]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Can't derive DecidableEq when implicit argument is used in structure

Context

structure Foo where
  a : List Nat
  ha : ∀ {i}, i ∈ a → 0 < i
deriving DecidableEq

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deriving.20DecidableEq.20fails.20with.20implicit.20argument. The equivalent in Lean 3 succeeds. This was observed in a porting note in mathlib from February 2023 but seemingly never reported.

Steps to Reproduce

Code as above.

Expected behavior: A DecidableEq instance is generated for Foo.

Actual behavior: Fails with error:

tactic 'subst' failed, invalid equality proof, it is not of the form (x = t) or (t = x)
  _ = _
x✝¹x✝: Foo
a✝¹: List Nat
a✝b✝: ∀ {i : Nat}, i ∈ a✝¹ → 0 < i
h✝: _ = _
⊢ Decidable ({ a := a✝¹, ha := a✝ } = { a := a✝¹, ha := b✝ })

Versions

Lean (version 4.3.0-rc2)
MacOS

Additional Information

None

Impact

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

[kmill]

It's worth mentioning that when the type of ha is ∀ i, i ∈ a → 0 < i then the deriving handler succeeds.