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 outparams of type class parameters), becauseCoe
is chained righttoleft. 
CoeOut α β
is likeCoe α β
but chained lefttoright. Use this if the variables in the typeα
are a superset of the variables inβ
. 
CoeTail α β
is likeCoe α β
, but only applied once. Use this for coercions that would cause loops, like[Ring R] → CoeTail Nat R
. 
CoeHead α β
is similar toCoeOut α β
, 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 valuex : α
itself. This is useful when the coercion function is dependent. An example of a dependent coercion is the instance forProp → Bool
, because it only holds forDecidable
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 (coercionto)function type, and this is triggered whenever an elementf : α
appears in an application likef x
which would not make sense sincef
does not have a function type.CoeFun
instances apply toCoeOut
as well. 
CoeSort α β
is a coercion to a sort.β
must be a universe, and this is triggered whena : α
appears in a place where a type is expected, like(x : a)
ora → a
.CoeSort
instances apply toCoeOut
as well.
On top of these instances this file defines several auxiliary type classes:
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 : α) : β)
.
Instances
Equations
 instCoeOTCOfCoeOut = { coe := fun (a : α) => CoeOTC.coe (CoeOut.coe a) }
Equations
 instCoeOTC = { coe := fun (a : α) => a }
CoeHead α β
is for coercions that are applied from lefttoright 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 : α) : β)
.
Instances
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 : α) : β)
.
Instances
Equations
 instCoeHTCOfCoeHeadOfCoeOTC = { coe := fun (a : α) => CoeOTC.coe (CoeHead.coe a) }
Equations
 instCoeHTCOfCoeOTC = { coe := fun (a : α) => CoeOTC.coe a }
Equations
 instCoeHTC = { coe := fun (a : α) => a }
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 : α) : β)
.
Instances
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 : α) : β)
.
Instances
Equations
 instCoeHTCTOfCoeTailOfCoeHTC = { coe := fun (a : α) => CoeTail.coe (CoeHTC.coe a) }
Equations
 instCoeHTCTOfCoeHTC = { coe := fun (a : α) => CoeHTC.coe a }
Equations
 instCoeHTCT = { coe := fun (a : α) => a }
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 inputx : α
is a parameter to the type class, so the value of typeβ
may possibly depend on additional typeclasses onx
.
Instances
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 inputx : α
is a parameter to the type class, so the value of typeβ
may possibly depend on additional typeclasses onx
.
Instances
Equations
 instCoeTOfCoeHTCT = { coe := CoeHTCT.coe a }
Equations
 instCoeTOfCoeDep = { coe := CoeDep.coe a }
CoeFun α (γ : α → Sort v)
is a coercion to a function. γ a
should be a
(coercionto)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 anotherCoeFun
type, in order to resolve a mistyped applicationf x
.
Instances
Equations
 instCoeOutOfCoeFun = { coe := fun (a : α) => CoeFun.coe a }
Equations
 instCoeOutOfCoeSort = { coe := fun (a : α) => CoeSort.coe a }
↑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))
Instances For
⇑ 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))
Instances For
↥ t
coerces t
to a type.
Equations
 coeSortNotation = Lean.ParserDescr.node `coeSortNotation 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↥") (Lean.ParserDescr.cat `term 1024))
Instances For
Basic instances #
Equations
 boolToSort = { coe := fun (b : Bool) => b = true }
Equations
 decPropToBool p = { coe := decide p }
Coe bridge #
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)
Instances For
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)