Adding a `BEq` instance makes `Mem` not decidable?

Stream: lean4

[David Renshaw]

-- this works
example : 1 ∈ [1] := by decide


inductive Foo where
| A : Foo
| B : Foo
deriving DecidableEq

-- this also works
example : .A ∈ [Foo.A] := by decide


inductive Bar where
| C : Bar
| D : Bar
deriving DecidableEq, BEq

-- this does not work!
example : .C ∈ [Bar.C] := by decide
-- failed to synthesize Decidable (Bar.C ∈ [Bar.C])

[David Renshaw]

My hypothesis is that the BEq instance is sending typeclass synthesis down a dead end.

[David Renshaw]

But this seems surprising and bad.

[David Renshaw]

(simp works to close the proof in this particular case, but not in a larger example where I first encountered the problem)

[Kyle Miller]

According to set_option trace.Meta.synthInstance true, the first one works because of docs#List.instDecidableMemOfLawfulBEq

That suggests that the reason the second one fails to work is that the additional BEq instance is overriding the one coming from DecidableEq, so it fails to derive a LawfulBEq instance. (There's a LawfulBEq instance coming from DecidableEq, but it's in terms of DecidableEq's BEq and not the derived BEq.)

Three ways to fix this: (1) make sure you don't have conflicting Decidable and BEq instances (2) create a version of List.instDecidableMemOfLawfulBEq for Decidable instances or (3) somehow get the derive handlers to work together so that the BEq from the Decidable instance is defeq to the BEq one.

I guess there's also (4) get the BEq handler to try to derive LawfulBEq as well (or have a LawfulBEq derive handler)

[David Renshaw]

I think I'm going to (5) remove the deriving BEq from my types.

[Kyle Miller]

Ah, that's what I meant by (1), you can either remove DerivableEq and then add your own LawfulBEq instance, or remove the BEq