why does ofNat require this form?

Stream: new members

[Alok Singh]

inductive TrivialWrapper where
| wrap (n: Nat)

/- fails with 'unknown identifier n'. But removing `n` gives `type expected, got
  (OfNat TrivialWrapper : Nat → Type)` -/
instance : OfNat TrivialWrapper n where
  ofNat := .wrap n


-- works
instance (n : Nat) : OfNat TrivialWrapper n where
  ofNat := .wrap n

-- from https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html
structure Rational where
  num : Int
  den : Nat
  inv : den ≠ 0

-- fails with 'unknown identifier n'
instance : OfNat Rational n where
  ofNat := { num := n, den := 1, inv := by decide }

Why doesn't the first form work? The definition of OfNat looks to me like it should allow naming n.

class OfNat (α : Type u) (_ : Nat) where
  ofNat : α

Even the link to https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html is apparently wrong.

[Vlad Tsyrklevich]

All of your examples seem to work in the Lean playground?

[Edward van de Meent]

the issue here is with the autoImplicit setting which is on at the playground

[Edward van de Meent]

i.e. your instance assumes you have some natural number n a priori, so you need to declare the assumption. When autoImplicit is on, lean will do that automatically (and try to resolve the type through elaboration). Otherwise, lean complains that suddenly you're mentioning some constant named n which lean knows nothing about.

[Edward van de Meent]

that means that fixed instances might look like this:

instance {n : Nat} : OfNat TrivialWrapper n where
  ofNat := .wrap n

instance {n : Nat} : OfNat Rational n where
  ofNat := { num := n, den := 1, inv := by decide }