Can't resolve OfNat instances defined with Nat literals

[david-christiansen]

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

When defining an OfNat instance for a small sum type, instance resolution only works when the Nat constructors are written out fully explicitly, rather than as Nat literals themselves.

Steps to Reproduce

Write the following:

inductive Bit where
  | zero
  | one

instance : OfNat Bit 0 where
  ofNat := Bit.zero

instance : OfNat Bit 1 where
  ofNat := Bit.one

example : Bit := 0

Expected behavior:

I expect the example to be defined to mean Bit.zero

Actual behavior:
This error:

failed to synthesize instance
   OfNat Bit 0

Reproduces how often:
100%

Versions

Lean (version 4.0.0-nightly-2022-07-30, commit 78927542b7f8, Release)

I'm running Fedora 36

Additional Information

I can work around the issue as follows:

inductive Bit where
  | zero
  | one

instance : OfNat Bit Nat.zero where
  ofNat := Bit.zero

instance : OfNat Bit (Nat.succ Nat.zero) where
  ofNat := Bit.one

example : Bit := 0

However, it quickly gets tiring and error-prone if the datatype has a few more constructors.

[Kha]

I think this can be considered a duplicate of #875.

A lint for this common issue would be nice though.

[leodemoura]

@Kha This issue has been raised so many times. I am considering writing code for converting the numeric literals occurring in OfNat instances to nat_lits.

[david-christiansen]

Thanks for the quick fix!

The docs linked to from #875 took me a long time to figure out, and I think it would have ended up with a fairly long explanation in the book. Much better to just make it easier :-)