From b0db7deeef520203bfc68b4bed05d2226d469c18 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 12 Aug 2022 19:32:55 -0400 Subject: [PATCH] doc: documentation for Init.Coe --- src/Init/Coe.lean | 197 +++++++++++++++++++++++++++++-- src/Lean/Elab/Term.lean | 2 +- src/Lean/Parser/Term.lean | 2 +- tests/lean/621.lean.expected.out | 2 +- 4 files changed, 188 insertions(+), 15 deletions(-) diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean index 19599db9c7..3689d5a248 100644 --- a/src/Init/Coe.lean +++ b/src/Init/Coe.lean @@ -1,45 +1,207 @@ /- Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Mario Carneiro -/ prelude import Init.Prelude +set_option linter.missingDocs true -- keep it documented + +/-! +# 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 +``` +-/ universe u v w w' +/-- +`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. +-/ class Coe (α : Sort u) (β : Sort v) where + /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`, + or by double type ascription `((x : α) : β)`. -/ coe : α → β -/-- Auxiliary class that contains the transitive closure of `Coe`. -/ +/-- +Auxiliary class that contains the transitive closure of `Coe`. +Users should generally not implement this directly. +-/ class CoeTC (α : Sort u) (β : Sort v) where + /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`, + or by double type ascription `((x : α) : β)`. -/ coe : α → β -/-- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/ +/-- +`CoeHead α β` is for coercions that can only appear at the beginning of a +sequence of coercions. That is, `β` can be further coerced via `Coe β γ` and +`CoeTail γ δ` instances but `α` will only be the inferred type of the input. +-/ class CoeHead (α : Sort u) (β : Sort v) where + /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`, + or by double type ascription `((x : α) : β)`. -/ coe : α → β -/-- Expensive coercion that can only appear at the end of a sequence of coercions. -/ +/-- +`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. +-/ class CoeTail (α : Sort u) (β : Sort v) where + /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`, + or by double type ascription `((x : α) : β)`. -/ coe : α → β -/-- Auxiliary class that contains `CoeHead` + `CoeTC` + `CoeTail`. -/ +/-- +Auxiliary class that contains `CoeHead` + `CoeTC` + `CoeTail`. + +A `CoeHTCT` chain has the "grammar" `(CoeHead)? (Coe)* (CoeTail)?`, except that +the empty sequence is not allowed. +-/ class CoeHTCT (α : Sort u) (β : Sort v) where + /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`, + or by double type ascription `((x : α) : β)`. -/ coe : α → β +/-- +`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. +-/ class CoeDep (α : Sort u) (_ : α) (β : Sort v) where + /-- 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`. -/ coe : β -/-- Combines CoeHead, CoeTC, CoeTail, CoeDep -/ +/-- +`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)? (Coe)* (CoeTail)? | CoeDep`, +except that the empty sequence is not allowed (identity coercions don't need +the coercion system at all). +-/ class CoeT (α : Sort u) (_ : α) (β : Sort v) where + /-- 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`. -/ coe : β -class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where - coe : (a : α) → γ a +/-- +`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`. +-/ +class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where + /-- 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`. -/ + coe : (f : α) → γ f + +/-- +`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)`. +-/ class CoeSort (α : Sort u) (β : outParam (Sort v)) where + /-- Coerces a value of type `α` to `β`, which must be a universe. -/ coe : α → β +/-- +`↑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)`. +-/ syntax:1024 (name := coeNotation) "↑" term:1024 : term instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe β δ] [CoeTC α β] : CoeTC α δ where @@ -100,13 +262,24 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead (Subtype p) α whe /-! # Coe bridge -/ --- Helper definition used by the elaborator. It is not meant to be used directly by users -@[inline] def 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 β := do +/-- +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. +-/ +@[inline] def 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 β := do let a ← liftM x pure (CoeT.coe a) --- Helper definition used by the elaborator. It is not meant to be used directly by users -@[inline] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do +/-- +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. +-/ +@[inline] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u} + [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do let a ← x pure (CoeT.coe a) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 0ef1daeaa4..3e2120893d 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1425,7 +1425,7 @@ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do if (← synthesizeCoeInstMVarCore mvarId) then let result ← expandCoe <| mkAppN (Lean.mkConst ``CoeSort.coe [u, v]) #[α, β, mvar, a] unless (← isType result) do - throwError "failed to coerse{indentExpr a}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr result}\nthis is often due to incorrect `CoeSort` instances, the synthesized value for{indentExpr coeSortInstType}\nwas{indentExpr mvar}" + throwError "failed to coerce{indentExpr a}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr result}\nthis is often due to incorrect `CoeSort` instances, the synthesized value for{indentExpr coeSortInstType}\nwas{indentExpr mvar}" return result else throwError "type expected" diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 1a9e1e954d..38f925b603 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -264,7 +264,7 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls @[builtinTermParser] def noindex := leading_parser "no_index " >> termParser maxPrec @[builtinTermParser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec -/-- Similar to `binrel`, but coerse `Prop` arguments into `Bool`. -/ +/-- Similar to `binrel`, but coerce `Prop` arguments into `Bool`. -/ @[builtinTermParser] def binrel_no_prop := leading_parser "binrel_no_prop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec @[builtinTermParser] def binop := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec @[builtinTermParser] def binop_lazy := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec diff --git a/tests/lean/621.lean.expected.out b/tests/lean/621.lean.expected.out index 36c635a258..20e6928aaf 100644 --- a/tests/lean/621.lean.expected.out +++ b/tests/lean/621.lean.expected.out @@ -1,5 +1,5 @@ 621.lean:4:45-4:47: error: type expected -failed to coerse +failed to coerce xs to a type, after applying `CoeSort.coe`, result is still not a type xs.val