Num lit in OfNat instance fails with poor error message

[ammkrn]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The following code fails; even with pp.all true, the error message isn't terribly helpful since it doesn't do anything with the literal 1 :

set_option pp.all true
structure Title where
  val : String

instance : OfNat Title 1 where
  ofNat := ⟨""⟩

-- failed to synthesize instance OfNat.{0} Title 1
example : Title := 1

Looking at the lean4 repo, the workaround seems to be instance : OfNat Title (nat_lit 1) := ..., which does work, but this seems like something that would frustrate new users.

Versions

Lean (version 4.0.0-nightly-2021-12-13, commit 3a6cc77, Release)
MacOS 11.4

[leodemoura]

It is documented here:
https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#numerals
https://leanprover.github.io/lean4/doc/typeclass.html?highlight=ofNat#numerals