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.

Important typeclasses #

Coe α β is the most basic class, and the usual one you will want to use when implementing a coercion for your own types.
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. This is automatically turned into CoeFun.coe f x.
CoeSort α β is a coercion to a sort. β must be a universe, and if a : α appears in a place where a type is expected, like (x : a) or a → a, then it will be turned into (x : CoeSort.coe a).
CoeHead is like Coe, but while Coe can be transitively chained in the CoeT class, CoeHead can only appear once and only at the start of such a chain. This is useful when the transitive instances are not well behaved.
CoeTail is similar: it can only appear at the end of a chain of coercions.
CoeT α (x : α) β itself is the combination of all the aforementioned classes (except CoeSort and CoeFun which have different triggers). You can implement CoeT if you do not want this coercion to be transitively composed with any other coercions.

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

Coercion #

Important typeclasses #

Basic instances #

Coe bridge #