Only ordinary coercion insertion uses chaining. Inserting coercions to a sort or a function uses ordinary instance synthesis. Similarly, dependent coercions are not chained.
The coercion insertion mechanism unfolds applications of coercions, which allows them to control the specific shape of the resulting term.
This is important both to ensure readable proof goals and to control evaluation of the coerced term in compiled code.
Unfolding coercions is controlled by the coe_decl attribute, which is applied to each coercion method (e.g. Coe.coe).
This attribute should be considered part of the internals of the coercion mechanism, rather than part of the public coercion API.
Coercion chaining is implemented through a collection of auxiliary type classes.
Users should not write instances of these classes directly, but knowledge of their structure can be useful when diagnosing the reason why a coercion was not inserted as expected.
The specific rules governing the ordering of instances in the chain (namely, that it should match CoeHead?CoeOut*Coe*CoeTail?) are implemented by the following type classes:
CoeOTC is the middle of the chain, consisting of the transitive closure of CoeOut instances followed by CoeTC.
CoeHTC is the start of the chain, consisting of at most one CoeHead instance followed by CoeOTC.
CoeHTCT is the whole chain, consisting of CoeHTC followed by at most one CoeTail instance. Alternatively, it might be a NatCast instance.
CoeT represents the entire chain: it is either a CoeHTCT chain or a single CoeDep instance.
CoeHTCT.{u, v} (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
Auxiliary class implementing CoeHead* Coe* CoeTail?.
Users should generally not implement this directly.
CoeHTCT.mk.{u, v}
coe : α → β
Coerces a value of type α to type β. Accessible by the notation ↑x,
or by double type ascription ((x : α) : β).
CoeHTC.{u, v} (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
Auxiliary class implementing CoeHead CoeOut* Coe*.
Users should generally not implement this directly.
CoeHTC.mk.{u, v}
coe : α → β
Coerces a value of type α to type β. Accessible by the notation ↑x,
or by double type ascription ((x : α) : β).
CoeOTC.{u, v} (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
Auxiliary class implementing CoeOut* Coe*.
Users should generally not implement this directly.
CoeOTC.mk.{u, v}
coe : α → β
Coerces a value of type α to type β. Accessible by the notation ↑x,
or by double type ascription ((x : α) : β).
CoeTC.{u, v} (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
Auxiliary class implementing Coe*.
Users should generally not implement this directly.
CoeTC.mk.{u, v}
coe : α → β
Coerces a value of type α to type β. Accessible by the notation ↑x,
or by double type ascription ((x : α) : β).