12.3. Coercing to Sorts🔗

The Lean elaborator expects types in certain positions without necessarily being able to determine the type's universe ahead of time. For example, the term following the colon in a definition header might be a proposition or a type. The ordinary coercion mechanism is not applicable because it requires a specific expected type, and there's no way to express that the expected type could be any universe in the Coe class.

When a term is elaborated in a position where a proposition or type is expected, but the inferred type of the elaborated term is not a proposition or type, Lean attempts to recover from the error by synthesizing an instance of CoeSort. If the instance is found, and the resulting type is itself a type, then it the coercion is inserted and unfolded.

Not every situation in which the elaborator expects a universe requires CoeSort. In some cases, a particular universe is available as an expected type. In these situations, ordinary coercion insertion using CoeT is used. Instances of CoeSort can be used to synthesize instances of CoeOut, so no separate instance is needed to support this use case. In general, coercions to types should be implemented as CoeSort.

type class

CoeSort.{u, v} (α : 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.

Instance Constructor

CoeSort.mk.{u, v}

Methods

coe : α → β

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

syntaxExplicit Coercion to Sorts

term ::= ...
    | `↥ t` coerces `t` to a type. ↥ term

Coercions to sorts can be explicitly triggered using the ↥ prefix operator.

Sort Coercions

A monoid is a type equipped with an associative binary operation and an identity element. While monoid structure can be defined as a type class, it can also be defined as a structure that “bundles up” the structure with the type:

structure Monoid where
  Carrier : Type u
  op : Carrier → Carrier → Carrier
  id : Carrier
  op_assoc :
    ∀ (x y z : Carrier), op x (op y z) = op (op x y) z
  id_op_identity : ∀ (x : Carrier), op id x = x
  op_id_identity : ∀ (x : Carrier), op x id = x

The type Monoid does not indicate the carrier:

def StringMonoid : Monoid where
  Carrier := String
  op := (· ++ ·)
  id := ""
  op_assoc := by⊢ ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z introsx✝:Stringy✝:Stringz✝:String⊢ x✝ ++ (y✝ ++ z✝) = x✝ ++ y✝ ++ z✝; simp [String.append_assoc]All goals completed! 🐙
  id_op_identity := by⊢ ∀ (x : String), "" ++ x = x introsx✝:String⊢ "" ++ x✝ = x✝; simpAll goals completed! 🐙
  op_id_identity := by⊢ ∀ (x : String), x ++ "" = x introsx✝:String⊢ x✝ ++ "" = x✝; simpAll goals completed! 🐙

However, a CoeSort instance can be implemented that applies the Monoid.Carrier projection when a monoid is used in a position where Lean would expect a type:

instance : CoeSort Monoid (Type u) where
  coe m := m.Carrier

example : StringMonoid := "hello"

Sort Coercions as Ordinary Coercions

The inductive type NatOrBool represents the types Nat and Bool. The can be coerced to the actual types Nat and Bool:

inductive NatOrBool where
  | nat | bool

@[coe]
abbrev NatOrBool.asType : NatOrBool → Type
  | .nat => Nat
  | .bool => Bool

instance : CoeSort NatOrBool Type where
  coe := NatOrBool.asType

open NatOrBool

The CoeSort instance is used when nat occurs to the right of a colon:

def x : nat := 5

When an expected type is available, ordinary coercion insertion is used. In this case, the CoeSort instance is used to synthesize a CoeOut NatOrBool Type instance, which chains with the Coe Type (Option Type) instance to recover from the type error.

def y : Option Type := bool