Coercion

Lean uses a somewhat elaborate system of typeclasses to drive the coercion system. Here a coercion means an invisible function that is automatically inserted to fix what would otherwise be a type error. For example, if we have:

def f (x : Nat) : Int := x

then this is clearly not type correct as is, because x has type Nat but type Int is expected, and normally you will get an error message saying exactly that. But before it shows that message, it will attempt to synthesize an instance of CoeT Nat x Int, which will end up going through all the other typeclasses defined below, to discover that there is an instance of Coe Nat Int defined.

This instance is defined as:

instance : Coe Nat Int := ⟨Int.ofNat⟩

so Lean will elaborate the original function f as if it said:

def f (x : Nat) : Int := Int.ofNat x

which is not a type error anymore.

You can also use the ↑ operator to explicitly indicate a coercion. Using ↑x instead of x in the example will result in the same output.

Because there are many polymorphic functions in Lean, it is often ambiguous where the coercion can go. For example:

def f (x y : Nat) : Int := x + y

This could be either ↑x + ↑y where + is the addition on Int, or ↑(x + y) where + is addition on Nat, or even x + y using a heterogeneous addition with the type Nat → Nat → Int. You can use the ↑ operator to disambiguate between these possibilities, but generally Lean will elaborate working from the "outside in", meaning that it will first look at the expression _ + _ : Int and assign the + to be the one for Int, and then need to insert coercions for the subterms ↑x : Int and ↑y : Int, resulting in the ↑x + ↑y version.

Note that unlike most operators like +, ↑ is always eagerly unfolded at parse time into its definition. So if we look at the definition of f from before, we see no trace of the CoeT.coe function:

def f (x : Nat) : Int := x
#print f
-- def f : Nat → Int :=
-- fun (x : Nat) => Int.ofNat x

Important typeclasses

Lean resolves a coercion by either inserting a CoeDep instance or chaining CoeHead? CoeOut* Coe* CoeTail? instances. (That is, zero or one CoeHead instances, an arbitrary number of CoeOut instances, etc.)

The CoeHead? CoeOut* instances are chained from the "left" side. So if Lean looks for a coercion from Nat to Int, it starts by trying coerce Nat using CoeHead by looking for a CoeHead Nat ?α instance, and then continuing with CoeOut. Similarly Coe* CoeTail? are chained from the "right".

These classes should be implemented for coercions:

• Coe α β is the most basic class, and the usual one you will want to use when implementing a coercion for your own types. The variables in the type α must be a subset of the variables in β (or out-params of type class parameters), because Coe is chained right-to-left.

• CoeOut α β is like Coe α β but chained left-to-right. Use this if the variables in the type α are a superset of the variables in β.

• CoeTail α β is like Coe α β, but only applied once. Use this for coercions that would cause loops, like [Ring R] → CoeTail Nat R.

• CoeHead α β is similar to CoeOut α β, but only applied once. Use this for coercions that would cause loops, like [SetLike S α] → CoeHead S (Set α).

• CoeDep α (x : α) β allows β to depend not only on α but on the value x : α itself. This is useful when the coercion function is dependent. An example of a dependent coercion is the instance for Prop → Bool, because it only holds for Decidable propositions. It is defined as:

  instance (p : Prop) [Decidable p] : CoeDep Prop p Bool := ...
  

• CoeFun α (γ : α → Sort v) is a coercion to a function. γ a should be a (coercion-to-)function type, and this is triggered whenever an element f : α appears in an application like f x which would not make sense since f does not have a function type. CoeFun instances apply to CoeOut as well.

• CoeSort α β is a coercion to a sort. β must be a universe, and this is triggered when a : α appears in a place where a type is expected, like (x : a) or a → a. CoeSort instances apply to CoeOut as well.

On top of these instances this file defines several auxiliary type classes:

• CoeTC := Coe*
• CoeOTC := CoeOut* Coe*
• CoeHTC := CoeHead? CoeOut* Coe*
• CoeHTCT := CoeHead? CoeOut* Coe* CoeTail?
• CoeDep := CoeHead? CoeOut* Coe* CoeTail? | CoeDep

class Coe (α : 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.

• coe : α → β

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

class CoeTC (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

Auxiliary class implementing Coe*. Users should generally not implement this directly.

• coe : α → β

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

instance instCoeTCOfCoe {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} [Coe β γ] [CoeTC α β] : CoeTC α γ

instance instCoeTCOfCoe_1 {α : Sort u_1} {β : Sort u_2} [Coe α β] : CoeTC α β

instance instCoeTC {α : Sort u_1} : CoeTC α α

class CoeOut (α : Sort u) (β : semiOutParam (Sort v)) : Sort (max (max 1 u) v)

CoeOut α β is for coercions that are applied from left-to-right.

• coe : α → β

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

class CoeOTC (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

Auxiliary class implementing CoeOut* Coe*. Users should generally not implement this directly.

• coe : α → β

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

instance instCoeOTCOfCoeOut {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [CoeOut α β] [CoeOTC β γ] : CoeOTC α γ

Equations

• instCoeOTCOfCoeOut = { coe := fun (a : α) => CoeOTC.coe (CoeOut.coe a) }

instance instCoeOTCOfCoeTC {α : Sort u_1} {β : Sort u_2} [CoeTC α β] : CoeOTC α β

Equations

• instCoeOTCOfCoeTC = { coe := fun (a : α) => CoeTC.coe a }

instance instCoeOTC {α : Sort u_1} : CoeOTC α α

Equations

• instCoeOTC = { coe := fun (a : α) => a }

class CoeHead (α : Sort u) (β : semiOutParam (Sort v)) : Sort (max (max 1 u) v)

CoeHead α β is for coercions that are applied from left-to-right at most once at beginning of the coercion chain.

• coe : α → β

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

class CoeHTC (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

Auxiliary class implementing CoeHead CoeOut* Coe*. Users should generally not implement this directly.

• coe : α → β

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

instance instCoeHTCOfCoeHeadOfCoeOTC {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [CoeHead α β] [CoeOTC β γ] : CoeHTC α γ

instance instCoeHTCOfCoeOTC {α : Sort u_1} {β : Sort u_2} [CoeOTC α β] : CoeHTC α β

instance instCoeHTC {α : Sort u_1} : CoeHTC α α

Equations

• instCoeHTC = { coe := fun (a : α) => a }

class CoeTail (α : semiOutParam (Sort u)) (β : Sort v) : Sort (max (max 1 u) v)

CoeTail α β is for coercions that can only appear at the end of a sequence of coercions. That is, α can be further coerced via Coe σ α and CoeHead τ σ instances but β will only be the expected type of the expression.

• coe : α → β

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

class CoeHTCT (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

Auxiliary class implementing CoeHead* Coe* CoeTail?. Users should generally not implement this directly.

• coe : α → β

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

instance instCoeHTCTOfCoeTailOfCoeHTC {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} [CoeTail β γ] [CoeHTC α β] : CoeHTCT α γ

instance instCoeHTCTOfCoeHTC {α : Sort u_1} {β : Sort u_2} [CoeHTC α β] : CoeHTCT α β

instance instCoeHTCT {α : Sort u_1} : CoeHTCT α α

Equations

• instCoeHTCT = { coe := fun (a : α) => a }

class CoeDep (α : Sort u) : α → (β : Sort v) → Sort (max 1 v)

CoeDep α (x : α) β is a typeclass for dependent coercions, that is, the type β can depend on x (or rather, the value of x is available to typeclass search so an instance that relates β to x is allowed).

Dependent coercions do not participate in the transitive chaining process of regular coercions: they must exactly match the type mismatch on both sides.

• coe : β

  The resulting value of type β. The input x : α is a parameter to the type class, so the value of type β may possibly depend on additional typeclasses on x.

class CoeT (α : Sort u) : α → (β : Sort v) → Sort (max 1 v)

CoeT is the core typeclass which is invoked by Lean to resolve a type error. It can also be triggered explicitly with the notation ↑x or by double type ascription ((x : α) : β).

A CoeT chain has the grammar CoeHead? CoeOut* Coe* CoeTail? | CoeDep.

• coe : β

  The resulting value of type β. The input x : α is a parameter to the type class, so the value of type β may possibly depend on additional typeclasses on x.

instance instCoeTOfCoeHTCT {α : Sort u_1} {β : Sort u_2} {a : α} [CoeHTCT α β] : CoeT α a β

Equations

• instCoeTOfCoeHTCT = { coe := CoeHTCT.coe a }

instance instCoeTOfCoeDep {α : Sort u_1} {a : α} {β : Sort u_2} [CoeDep α a β] : CoeT α a β

Equations

• instCoeTOfCoeDep = { coe := CoeDep.coe a }

instance instCoeT {α : Sort u_1} {a : α} : CoeT α a α

class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) : Sort (max (max 1 u) v)

CoeFun α (γ : α → Sort v) is a coercion to a function. γ a should be a (coercion-to-)function type, and this is triggered whenever an element f : α appears in an application like f x, which would not make sense since f does not have a function type. CoeFun instances apply to CoeOut as well.

• coe : (f : α) → γ f

  Coerces a value f : α to type γ f, which should be either be a function type or another CoeFun type, in order to resolve a mistyped application f x.

instance instCoeOutOfCoeFun {α : Sort u_1} {β : Sort u_2} [CoeFun α fun (x : α) => β] : CoeOut α β

class CoeSort (α : Sort u) (β : outParam (Sort v)) : Sort (max (max 1 u) v)

CoeSort α β is a coercion to a sort. β must be a universe, and this is triggered when a : α appears in a place where a type is expected, like (x : a) or a → a. CoeSort instances apply to CoeOut as well.

• coe : α → β

  Coerces a value of type α to β, which must be a universe.

instance instCoeOutOfCoeSort {α : Sort u_1} {β : Sort u_2} [CoeSort α β] : CoeOut α β

Equations

• instCoeOutOfCoeSort = { coe := fun (a : α) => CoeSort.coe a }

def coeNotation : Lean.ParserDescr

↑x represents a coercion, which converts x of type α to type β, using typeclasses to resolve a suitable conversion function. You can often leave the ↑ off entirely, since coercion is triggered implicitly whenever there is a type error, but in ambiguous cases it can be useful to use ↑ to disambiguate between e.g. ↑x + ↑y and ↑(x + y).

def coeFunNotation : Lean.ParserDescr

⇑ t coerces t to a function.

Equations

• coeFunNotation = Lean.ParserDescr.node `coeFunNotation 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⇑") (Lean.ParserDescr.cat `term 1024))

def coeSortNotation : Lean.ParserDescr

↥ t coerces t to a type.

Basic instances

instance boolToProp : Coe Bool Prop

Equations

• boolToProp = { coe := fun (b : Bool) => b = true }

instance boolToSort : CoeSort Bool Prop

Equations

• boolToSort = { coe := fun (b : Bool) => b = true }

instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool

instance optionCoe {α : Type u} : Coe α (Option α)

Equations

• optionCoe = { coe := some }

instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeOut (Subtype p) α

Coe bridge

@[reducible, inline]

abbrev Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [(a : α) → CoeT α a β] [Monad n] (x : m α) : n β

Helper definition used by the elaborator. It is not meant to be used directly by users.

This is used for coercions between monads, in the case where we want to apply a monad lift and a coercion on the result type at the same time.

@[reducible, inline]

abbrev Lean.Internal.coeM {m : Type u → Type v} {α β : Type u} [(a : α) → CoeT α a β] [Monad m] (x : m α) : m β

Helper definition used by the elaborator. It is not meant to be used directly by users.

This is used for coercing the result type under a monad.

Equations

• Lean.Internal.coeM x = do let a ← x pure (CoeT.coe a)