Weird “failed to synthesize instance” error

Stream: new members

[Sabrina Jewson]

So I’m messing around with some typeclasses and I encountered this extremely weird error, with a minimal reproducer below:

class AddGroup (α : Type u) extends Add α, OfNat α 0, Neg α
class Ring (α : Type u) extends Add α, AddGroup α
class AddOrder (α : Type u) [Add α] [LE α]
theorem neg_is_nonneg [AddGroup α] [LE α] [AddOrder α] {a : α} : 0 ≤ -a ↔ a ≤ 0 := sorry

class TotalOrderedRing (α : Type u) extends Ring α, LE α, AddOrder α
example [TotalOrderedRing α] {a : α} (ha : a ≤ 0) : True := by
  have : _ := (@neg_is_nonneg α).mpr ha -- Works
  have : _ := neg_is_nonneg.mpr ha -- failed to synthesize instance AddOrder ?m.448
  trivial

This is really confusing to me — I thought that Lean would be able to infer that α is the desired type here. Am I doïng something silly or is this a bug? I’m using the latest Nightly of Lean 4.

[Sabrina Jewson]

(note, the typeclasses have been simplified, e.g. Ring extending from Add, a necessary precondition for this error to occur, is representative of it extending from Semiring which extends from Add)

[Sabrina Jewson]

Looks maybe the same as <https://github.com/leanprover/lean4/issues/2183>?
I’m not experiënced enough in Lean to tell :sweat_smile:

[Eric Wieser]

Did this work in lean 3?