Typeclass inference failing

Stream: lean4

[Jesse Vogel]

Consider the typeclasses as in the example below. Why is the typeclass system not able to infer an instance of ZeroOne α from instances Zero α and One α? And, is there a way to get this to work without explicitly defining these trivial instances? I guess such cases appear a lot in mathlib as well?

namespace Test

variable (α : Type u)

class Zero where zero : α
class One where one : α
class ZeroOne extends Zero α, One α

variable [Zero α] [One α]

#check (inferInstance : ZeroOne α) -- fails to find instance

instance : ZeroOne α where -- quite an obvious instance
  toZero := inferInstance
  toOne := inferInstance

#check (inferInstance : ZeroOne α) -- now it does find an instance

-- Conversely, it works just fine
variable (β : Type u) [ZeroOne β]
#check (inferInstance : Zero β)
#check (inferInstance : One β)

end Test

[Tomas Skrivan]

In Lean 3 this would imply type class loop which were bad. In Lean 4, loops are not bad anymore. My guess is that the reason is partially historical, people learned to live without it. Also do you have a use case where you can immediately provide instance of ZeroOne? The last reason is probably performance, not providing this instance can shorten class synthesis primarily in case of failure as all possibilities need to be exhausted.

To save on typing with

instance : ZeroOne a := ZeroOne.mk

[Sebastian Ullrich]

Lean 4 has a specific macro for that use case:

class abbrev ZeroOne := Zero α, One α