# 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`

source
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 : α) : β)`.

Instances

source
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 : α) : β)`.

Instances

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

- instCoeTCOfCoe = { coe := fun (a : α) => Coe.coe (CoeTC.coe a) }

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

- instCoeTCOfCoe_1 = { coe := fun (a : α) => Coe.coe a }

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

- instCoeTC = { coe := fun (a : α) => a }

source
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 : α) : β)`.

Instances

source
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 : α) : β)`.

Instances

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

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

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

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

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

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

source
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 : α) : β)`.

Instances

source
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 : α) : β)`.

Instances

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

- instCoeHTCOfCoeHeadOfCoeOTC = { coe := fun (a : α) => CoeOTC.coe (CoeHead.coe a) }

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

- instCoeHTCOfCoeOTC = { coe := fun (a : α) => CoeOTC.coe a }

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

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

source
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 : α) : β)`.

Instances

source
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 : α) : β)`.

Instances

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

- instCoeHTCTOfCoeTailOfCoeHTC = { coe := fun (a : α) => CoeTail.coe (CoeHTC.coe a) }

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

- instCoeHTCTOfCoeHTC = { coe := fun (a : α) => CoeHTC.coe a }

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

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

source
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`.

Instances

source
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`.

Instances

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

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

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

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

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

- instCoeT = { coe := a }

source
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`.

Instances

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

- instCoeOutOfCoeFun = { coe := fun (a : α) => CoeFun.coe a }

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

Instances

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

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

source
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))

Instances For

source
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))

Instances For

source
def coeSortNotation :
Lean.ParserDescr

`↥ 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 #

source
instance boolToProp :
Coe Bool Prop
Equations

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

source
instance boolToSort :
CoeSort Bool Prop
Equations

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

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

- decPropToBool p = { coe := decide p }

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

- subtypeCoe = { coe := fun (v : Subtype p) => v.val }

# Coe bridge #

source
@[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.

Equations

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

Instances For

source
@[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)

Instances For