Documentation

Init.Coe

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 NatNatInt. 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 : NatInt :=
-- 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:

On top of these instances this file defines several auxiliary type classes:

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.

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

    Instances
      instance instCoeTC {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} [Coe β γ] [CoeTC α β] :
      CoeTC α γ
      Equations
      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.

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

        Instances
          instance instCoeOTC {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [CoeOut α β] [CoeOTC β γ] :
          CoeOTC α γ
          Equations
          instance instCoeOTC_1 {α : Sort u_1} {β : Sort u_2} [CoeTC α β] :
          CoeOTC α β
          Equations
          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.

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

            Instances
              instance instCoeHTC {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [CoeHead α β] [CoeOTC β γ] :
              CoeHTC α γ
              Equations
              instance instCoeHTC_1 {α : Sort u_1} {β : Sort u_2} [CoeOTC α β] :
              CoeHTC α β
              Equations
              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.

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

                Instances
                  instance instCoeHTCT {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} [CoeTail β γ] [CoeHTC α β] :
                  CoeHTCT α γ
                  Equations
                  instance instCoeHTCT_1 {α : Sort u_1} {β : Sort u_2} [CoeHTC α β] :
                  CoeHTCT α β
                  Equations
                  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.

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

                    Instances
                      instance instCoeT {α : Sort u_1} {β : Sort u_2} {a : α} [CoeHTCT α β] :
                      CoeT α a β
                      Equations
                      instance instCoeT_1 {α : Sort u_1} {a : α} {β : Sort u_2} [CoeDep α a β] :
                      CoeT α a β
                      Equations
                      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.

                      Instances
                        instance instCoeOut {α : Sort u_1} {β : Sort u_2} [CoeFun α fun x => β] :
                        CoeOut α β
                        Equations
                        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.

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

                          ↑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
                          Instances For

                            Basic instances #

                            Equations
                            Equations
                            instance decPropToBool (p : Prop) [Decidable p] :
                            Equations
                            instance optionCoe {α : Type u} :
                            Coe α (Option α)
                            Equations
                            • optionCoe = { coe := some }
                            instance subtypeCoe {α : Sort u} {p : αProp} :
                            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
                            Instances For
                              @[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
                              Instances For