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 : α → β

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

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.

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

• coe : α → β

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

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

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

Equations

• instCoeTC = { coe := fun a => Coe.coe (CoeTC.coe a) }

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

Equations

• instCoeTC_1 = { coe := fun a => Coe.coe a }

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

Equations

• instCoeTC_2 = { coe := fun a => a }

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

• coe : α → β

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

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

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

• coe : α → β

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

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

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

Equations

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

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

Equations

• instCoeOTC_1 = { coe := fun a => CoeTC.coe a }

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

Equations

• instCoeOTC_2 = { coe := fun a => a }

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

• coe : α → β

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

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

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

• coe : α → β

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

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

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

Equations

• instCoeHTC = { coe := fun a => CoeOTC.coe (CoeHead.coe a) }

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

Equations

• instCoeHTC_1 = { coe := fun a => CoeOTC.coe a }

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

Equations

• instCoeHTC_2 = { coe := fun a => a }

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

• coe : α → β

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

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.

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

• coe : α → β

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

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

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

Equations

• instCoeHTCT = { coe := fun a => CoeTail.coe (CoeHTC.coe a) }

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

Equations

• instCoeHTCT_1 = { coe := fun a => CoeHTC.coe a }

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

Equations

• instCoeHTCT_2 = { coe := fun a => a }

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

• 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.

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.

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

• 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.

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.

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

Equations

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

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

Equations

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

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

Equations

• instCoeT_2 = { coe := a }

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

• 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.

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.

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

Equations

• instCoeOut = { coe := fun a => CoeFun.coe a }

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

• coe : α → β

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

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.

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

Equations

• instCoeOut_1 = { 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).

Equations

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

Basic instances

instance boolToProp : Coe Bool Prop

Equations

• boolToProp = { coe := fun b => b = true }

instance boolToSort : CoeSort Bool Prop

Equations

• boolToSort = { coe := fun b => b = true }

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

Equations

• decPropToBool p = { coe := decide p }

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

Equations

• optionCoe = { coe := some }

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

Equations

• subtypeCoe = { coe := fun v => v.val }

Coe bridge

@[inline]

def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α : Type u} {β : 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.

Equations

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

@[inline]

def Lean.Internal.coeM {m : Type u → Type v} {α : Type u} {β : 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)