weirdness with `ofNat`

Stream: mathlib4

[Scott Morrison]

Guess which currently fail in mathlib4 (e.g. if you put these at the bottom of Algebra/Ring/Basic.lean):

example {α : Type _} [Ring α] : α := 0
example {α : Type _} [Ring α] : α := 1
example {α : Type _} [Ring α] : α := 2
example {α : Type _} [Ring α] : α := 37
example {α : Type _} [Ring α] : OfNat α 0 := inferInstance
example {α : Type _} [Ring α] : OfNat α 1 := inferInstance
example {α : Type _} [Ring α] : OfNat α 2 := inferInstance
example {α : Type _} [Ring α] : OfNat α 37 := inferInstance

[Scott Morrison]

example {α : Type _} [Ring α] : OfNat α 0 := inferInstance -- failed to synthesize instance OfNat α 0
example {α : Type _} [Ring α] : OfNat α 1 := inferInstance -- failed to synthesize instance OfNat α 1

I don't pretend to understand how that is internally consistent...

[Mario Carneiro]

remember that OfNat instances require their argument to be a raw nat literal. These all succeed:

example {α : Type _} [Ring α] : OfNat α (nat_lit 0) := inferInstance
example {α : Type _} [Ring α] : OfNat α (nat_lit 1) := inferInstance
example {α : Type _} [Ring α] : OfNat α (nat_lit 2) := inferInstance
example {α : Type _} [Ring α] : OfNat α (nat_lit 37) := inferInstance

I believe Leo added a hack to make OfNat instances without nat_lit to work anyway, but it's possible that if there is some inconsistency in how they are being declared you will see different things for 0, 1 and 2 or more (yes, there is a docs4#Nat.AtLeastTwo typeclass for this)