Simple Type Class Synthesis Failure

Stream: new members

[Zach]

I have a proof which is mysteriously (to me) failing to synthesize a type class instance. I've distilled the issue into a simple example:

section
variable {T : Type}
variable [BEq T]
variable [EquivBEq T]
-- failed to synthesize PartialEquivBEq (Option T)
#synth PartialEquivBEq (Option T)

Because EquivBEq T implies PartialEquivBEq T (right?), I'm surprised that we can't synthesize PartialEquivBEq (Option T). I've been able to synthesize PartialEquivBEq (Option ...) in other examples and even adding variable [PartialEquivBEq T] to the above doesn't correct the problem. Is there a good way to diagnose why a type class instance can't be synthesized or what steps Lean attempted to take to synthesize it?

[Robin Arnez]

Well, there is no EquivBEq instance for Option. In other cases it presumably went through LawfulBEq

[Zach]

I see; thanks! Is there a way for me to ask lean how it has synthesized a type class instance so I can see this line of reasoning?

[Robin Arnez]

Well, for one you can recursively hover over the output of #synth to see which instances it used. If you want to know how it got the answer you can also use set_option trace.Meta.synthInstance true in above the #synth

[Zach]

Thanks again! This is helpful. It hadn't occurred to me that the solution to my other tests was via LawfulBEq. I'm trying to write some proofs generally enough that == could over-equate things (e.g. two sets represented as lists could use == to canonicalize). Perhaps that's against the grain of how I'm expected to work.

I'm a little surprised that there's no PartialEquivBEq for Option, but I'm guessing that's just because not everything can be in the standard library. The upside is that I can declare my own instance if I want:

instance {T : Type} [BEq T] [PartialEquivBEq T]
    : PartialEquivBEq (Option T) where
  symm := by
    intro a b H
    cases a <;> cases b <;> try simp_all
    case some.some a' b' =>
      apply PartialEquivBEq.symm
      exact H
  trans := by
    intro a b c H1 H2
    cases a <;> cases b <;> cases c <;> try simp_all
    case some.some.some a' b' c' =>
      exact PartialEquivBEq.trans H1 H2

Thanks for the help!