Zulip Chat Archive

Stream: new members

Topic: Weird “failed to synthesize instance” error

Sabrina Jewson (Aug 18 2023 at 20:41):

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

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 (Aug 18 2023 at 20:43):

(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 (Aug 18 2023 at 20:47):

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 (Aug 20 2023 at 22:37):

Did this work in lean 3?

Last updated: Dec 20 2023 at 11:08 UTC