Coercion for nat literal

Stream: lean4

[Param Reddy]

While reading Coercion in Functional Programming in Lean, I am confused about one of the examples with cascading Option type.

-- 392 is Nat
#check 392

-- This gives error
def pppN : Option (Option (Option Nat)) := 392

-- This does not
def pppN1 : Option (Option (Option Nat)) := (392 : Nat)

check says that 392's type is nat. If lean already knows that 392's type is Nat, why does it again need explicit : Nat to initiate search for coercion chain to get from 392 to Option (Option (Option Nat))?

From text surrounding the example:

"Coercions are only activated automatically when Lean encounters a mismatch between an inferred type and a type that is imposed from the rest of the program. In cases with other errors, coercions are not activated. For example, if the error is that an instance is missing, coercions will not be used:"

But i could not fully comprehend what it means in this context.

[Timo Carlin-Burns]

The nat literal syntax uses a typeclass OfNat to take values in arbitrary types. For example, you can write (392 : Nat) or (392 : Int) and they are both literals using instances of OfNat Nat 392 and OfNat Int 392 respectively. When you write 392 without specifying a type, Lean cannot unambiguously determine what type of literal you're looking for, but there is a special fallback for this syntax to default to type Nat. When you write (392 : Option Nat), it's unambiguous that you want your literal to be of type Option Nat. Lean looks for an instance of OfNat (Option Nat) 392 and errors when it fails to find one

[Param Reddy]

Timo Carlin-Burns Thanks Timo. I think I was missing that unlike other languages 392 as literal does not have predefined type and #check was using "special fallback" to default to Nat.

[Kyle Miller]

Here's the implementation of that defaulting to Nat: https://github.com/leanprover/lean4/blob/019922878491315bcdc3bba67ecfd5e337333703/src/Init/Prelude.lean#L1095-L1097

Just pointing it out so you don't think it's hard coded. These default_instances are considered at certain points when typeclass inference can't make further progress on its own.

[Kyle Miller]

If you want to obstruct the expected type from propagating to 392, rather than specifying Nat, you can get it to follow the defaulting behavior by using ( ... :) syntax:

def pppN : Option (Option (Option Nat)) := (392 :)

That means "elaborate the expression without an expected type".

[Param Reddy]

Kyle Miller said:

Here's the implementation of that defaulting to Nat: https://github.com/leanprover/lean4/blob/019922878491315bcdc3bba67ecfd5e337333703/src/Init/Prelude.lean#L1095-L1097

Just pointing it out so you don't think it's hard coded. These default_instances are considered at certain points when typeclass inference can't make further progress on its own.

This now confused me more.

@[default_instance 100] /- low prio -/
instance (n : Nat) : OfNat Nat n where
  ofNat := n

My read of this is if n is Nat then you can apply this OfNat instance to Nat n. This seems a bit circular to me as it assumes n is nat before being triggered. So would mean 392 is already of type Nat. What am i missing?

[Kyle Miller]

It's that 392 is syntax for OfNat.ofNat 392, with 392 an actual Nat. Then Lean figures out which OfNat instance to used based on the expected type of this expression.

[Kyle Miller]

There's nat_lit 392 syntax if you want to get a raw Nat literal, without going through all this. I guess it's better to say that 392 is syntax for OfNat.ofNat (nat_lit 392).

[Eric Wieser]

Is there a reason not to enable pp.natLit by default?

[Kyle Miller]

I wasn't sure if there was a reason not to, and I decided not to investigate too deeply to see if there are any unintended consequences, so in the RFC (lean4#3021) I just specified that it's false by default. Well, I did know that pp.all is more verbose if that's the default:

#check 1
-- with pp.natLit false:
-- @OfNat.ofNat.{0} Nat 1 (instOfNatNat 1) : Nat
-- with pp.natLit true:
-- @OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)) : Nat

So, there would be the question of whether pp.all should turn off pp.natLit, or leave it on.

One thing that came up is the follow-up question of whether Nat.zero.succ.succ.....succ should pretty print as a nat_lit too, and if it does, then when pp.natLit is false, whether it should pretty print as a numeral for consistency.

I think changing this would take some real cases where someone got confused because of a raw nat_lit, and going through the process of filing an issue and getting :+1:'s.