Fragmented Explanation for Coercion of `Nat to Option (Option (Option Nat))` Example

[JadAbouHawili]

The following at the end of 3.6.3 introduces 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:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize
  OfNat (Option (Option (Option Nat))) 392
numerals are polymorphic in Lean, but the numeral `392` cannot be used in a context 
where the expected type is
  Option (Option (Option Nat))
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

This can be worked around by manually indicating the desired type to be used for OfNat:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  (392 : Nat)

Additionally, coercions can be manually inserted using an up arrow:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  ↑(392 : Nat)

In some cases, this can be used to ensure that Lean finds the right instances.
 It can also make the programmer's intentions more clear.

and then 3.6.7 provides more explanation

Natural number literals are overloaded with the OfNat type class. Because coercions fire 
in cases where types don't match, rather than in cases of missing instances, 
a missing OfNat instance for a type does not cause a coercion from Nat to be applied:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  392

failed to synthesize
  OfNat (Option (Option (Option Nat))) 392
numerals are polymorphic in Lean, but the numeral `392` cannot be used in a context where the expected type is
  Option (Option (Option Nat))
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

3.6.3 left me confused and 3.6.7 clarified this confusion, which is why I'm suggesting merging both.

---

This section from 3.6.3 has 'the spirit' of 3.6.7 but wasn't fully understandable until I read 3.6.7 and went back to 3.6.3

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:

Moreover , this section from 3.6.3 made me correctly guess what was explicitly stated in 3.6.7 which reinforces the case of merging

This can be worked around by manually indicating the desired type to be used for OfNat:
def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  (392 : Nat)

I am willing to propose changes and prepare a pull request that would merge 3.6.7 into 3.6.3 and remove section 3.6.7 if such changes would be accepted.