unfortunate error messages

Stream: lean4

[Jason Gross]

This is unfortunate:

instance OfNat_1 : OfNat Type 1 := { ofNat := Unit }
#check (1 : Type)
/-
2:9: failed to synthesize instance
  OfNat Type 1
-/

[Jason Gross]

(I do see what's going on here, but it took me a couple minutes and set_option pp.all true to puzzle it out)

[Leonardo de Moura]

We have some documentation here https://leanprover.github.io/lean4/doc/typeclass.html (Numerals section)
You are not the first person confused by this issue, we should probably just let people write these instances without the natLit!.