deriving DecidableEq fails with implicit argument

Stream: lean4

[Bhavik Mehta]

Here's my example:

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

This 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✝ })

Is this already known? The equivalent works in Lean 3, and is mentioned in (at least) one porting note in mathlib.

[Kyle Miller]

I don't see anything in the issue tracker -- want to create an issue?

It seems it's just the implicit argument. This works:

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

[Bhavik Mehta]

Will do.

[Bhavik Mehta]

Reported here: https://github.com/leanprover/lean4/issues/2914

[Scott Morrison]

@Arthur Adjedj or others who've played with these derive handlers --- any ideas what's happening here? I'd be happy to merge a fix.

[Kyle Miller]

lean4#2918

[Scott Morrison]

Looks great. I'll merge once the test is moved.