Option coercion

Stream: lean4

[Paul Chisholm]

The following is accepted by Lean:

def g (n : Nat) : Option Nat := some n

def f (n : Nat) : Option Nat :=
  match g n with
  | none => none
  | some x => x

#check f 4
#eval f 4

I assume in the some clause of the match the x of type Nat is being coerced to Option Nat.

However, the following throws an error:

def f (n : Nat) : Option Nat :=
  match g n with
  | none => none
  | some x => 4

failed to synthesize instance
  OfNat (Option Nat) 4

The 4 is not coerced to Option Nat though the documentation states in the absence of other information, a numeric literal is considered to be Nat. I can get it to pass type checking by changing it to (4:Nat).

[Leonardo de Moura]

The 4 is not coerced to Option Nat though the documentation states in the absence of other information, a numeric literal is considered to be Nat

The documentation is correct. The expected type is available, it is Option Nat.

I can get it to pass type checking by changing it to (4:Nat).

You can also write some 4 and avoid the need for a coercion.

[Paul Chisholm]

Yes, personally I always include the some for clarity, but why is x coerced to Option Nat by 4 throw an error?

[Leonardo de Moura]

It is because Lean knows that x is a Nat, but doesn't know what 4 is. The numeric literals are polymorphic in Lean. Given a context where the expected type is A, Lean will accept the numeric literal 4, if it can synthesize the instance OfNat A 4. Polymorphism and coercions often create the problem you described above.

[Paul Chisholm]

Ok, got it thanks.