12. Coercions🔗

When the Lean elaborator is expecting one type but produces a term with a different type, it attempts to automatically insert a coercion, which is a specially designated function from the term's type to the expected type. Coercions make it possible to use specific types to represent data while interacting with APIs that expect less-informative types. They also allow mathematical developments to follow the usual practice of “punning”, where the same symbol is used to stand for both an algebraic structure and its carrier set, with the precise meaning determined by context.

Lean's standard library and metaprogramming APIs define many coercions. Some examples include:

A Nat may be used where an Int is expected.
A Fin may be used where a Nat is expected.
An α may be used where an Option α is expected. The coercion wraps the value in some.
An α may be used where a Thunk α is expected. The coercion wraps the term in a function to delay its evaluation.
When one syntax category c1 embeds into another category c2, a coercion from TSyntax c1 to TSyntax c2 performs any necessary wrapping to construct a valid syntax tree.

Coercions are found using type class synthesis. The set of coercions can be extended by adding further instances of the appropriate type classes.

Coercions

All of the following examples rely on coercions:

example (n : Nat) : Int := n
example (n : Fin k) : Nat := n
example (x : α) : Option α := x

def th (f : Int → String) (x : Nat) : Thunk String := f x

open Lean in
example (n : Ident) : Term := n

In the case of th, using Lean.Parser.Command.print : command#print demonstrates that evaluation of the function application is delayed until the thunk's value is requested:

def th : (Int → String) → Nat → Thunk String :=
fun f x => { fn := fun x_1 => f ↑x }#print th

def th : (Int → String) → Nat → Thunk String :=
fun f x => { fn := fun x_1 => f ↑x }

Coercions are not used to resolve generalized field notation: only the inferred type of the term is considered. However, a type ascription can be used to trigger a coercion to the type that has the desired generalized field. Coercions are also not used to resolve OfNat instances: even though there is a default instance for OfNat Nat, a coercion from Nat to α does not allow natural number literals to be used for α.

Coercions and Generalized Field Notation

The name Nat.bdiv is not defined, but Int.bdiv exists. The coercion from Nat to Int is not considered when looking up the field bdiv:

example (n : Nat) := Invalid field `bdiv`: The environment does not contain `Nat.bdiv`
  n
has type
  Natn.bdiv 2

Invalid field `bdiv`: The environment does not contain `Nat.bdiv`
  n
has type
  Nat

This is because coercions are only inserted when there is an expected type that differs from an inferred type, and generalized fields are resolved based on the inferred type of the term before the dot. Coercions can be triggered by adding a type ascription, which additionally causes the inferred type of the entire ascription term to be Int, allowing the function Int.bdiv to be found.

example (n : Nat) := (n : Int).bdiv 2

Coercions and OfNat

Bin is an inductive type that represents binary numbers.

inductive Bin where
  | done
  | zero : Bin → Bin
  | one : Bin → Bin

def Bin.toString : Bin → String
  | .done => ""
  | .one b => b.toString ++ "1"
  | .zero b => b.toString ++ "0"

instance : ToString Bin where
  toString
    | .done => "0"
    | b => Bin.toString b

Binary numbers can be converted to natural numbers by repeatedly applying Bin.succ:

def Bin.succ (b : Bin) : Bin :=
  match b with
  | .done => Bin.done.one
  | .zero b => .one b
  | .one b => .zero b.succ

def Bin.ofNat (n : Nat) : Bin :=
  match n with
  | 0 => .done
  | n + 1 => (Bin.ofNat n).succ

Even if Bin.ofNat is registered as a coercion, natural number literals cannot be used for Bin:

attribute [coe] Bin.ofNat

instance : Coe Nat Bin where
  coe := Bin.ofNat

#eval (failed to synthesize
  OfNat Bin 9
numerals are polymorphic in Lean, but the numeral `9` cannot be used in a context where the expected type is
  Bin
due to the absence of the instance above

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

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

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

This is because coercions are inserted in response to mismatched types, but a failure to synthesize an OfNat instance is not a type mismatch.

The coercion can be used in the definition of the OfNat Bin instance:

instance : OfNat Bin n where
  ofNat := n

1010#eval (10 : Bin)

Most new coercions can be defined by declaring an instance of the Coe type class and applying the coe attribute to the function that performs the coercion. To enable more control over coercions or to enable them in more contexts, Lean provides further classes that can be implemented, described in the rest of this chapter.

Defining Coercions: Decimal Numbers

Decimal numbers can be defined as arrays of digits.

structure Decimal where
  digits : Array (Fin 10)

Adding a coercion allows them to be used in contexts that expect Nat, but also contexts that expect any type that Nat can be coerced to.

@[coe]
def Decimal.toNat (d : Decimal) : Nat :=
  d.digits.foldl (init := 0) fun n d => n * 10 + d.val

instance : Coe Decimal Nat where
  coe := Decimal.toNat

This can be demonstrated by treating a Decimal as an Int as well as a Nat:

def twoHundredThirteen : Decimal where
  digits := #[2, 1, 3]

def one : Decimal where
  digits := #[1]

-212#eval (one : Int) - (twoHundredThirteen : Nat)

-212

type class

Coe.{u, v} (α : semiOutParam (Sort u)) (β : Sort v) :
  Sort (max (max 1 u) v)
Coe.{u, v} (α : semiOutParam (Sort u))
  (β : Sort v) : Sort (max (max 1 u) v)

Coe α β is the typeclass for coercions from α to β. It can be transitively chained with other Coe instances, and coercion is automatically used when x has type α but it is used in a context where β is expected. You can use the ↑x operator to explicitly trigger coercion.

Instance Constructor

Coe.mk.{u, v}

Methods

coe : α → β

Coerces a value of type α to type β. Accessible by the notation ↑x, or by double type ascription ((x : α) : β).