Gory details of `coe`

Stream: lean4

[Moritz Doll]

FPiL has a pretty good overview of coercion, but the part about the nasty details is a bit short. Is there any documentation/zulip threads that explain how coercion actually works in Lean 4 (or differences to Lean 3)? I am asking because I want to understand when one has to change stuff in the mathlib4 port.

[David Thrane Christiansen]

@Gabriel Ebner sent me a nice high-level description. I'll reproduce it here with his permission.

[Gabriel Ebner]

Please feel free to post it here.

[David Thrane Christiansen]

Thanks! Here it is:

We want all type-class query to terminate, quickly, and no matter whether they fail or succeed. This is a strict requirement since we try to apply coercions quite often in the elaborator. Instances like Coe α (Option α) can easily lead to nontermination (depending on the order they're chained in, which has changed in the past). The general coercion chain looks like this:

CoeHead? Coe* CoeTail?

And it is currently set up so that we first search for a CoeHead coercion, then for a CoeTail coercion, and then chain Coe from the right. An important invariant that we maintain is that in typeclass queries for Coe A B, the term B is always metavariable-free. This means that for:

Coe T S, CoeTail T S: the variables of T must be a subset of those of S
CoeHead T S: the variables of S must be a subset of those of T

Generally speaking, the property we want to have at the end is that there are only finitely many types A that transitively coerce into any metavariable-free type B. It is not clear to me what additional invariants we need to put on Coe A B instances to ensure that, where Coe α (Option α) becomes acceptable. It seems tempting to require that A is less than B in some term order, but that doesn't work because we have cyclic coercions where you can coerce both A into B as well as B into A.

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.204.20set_like/near/244530150

[Eric Wieser]

(note you can use the "quote and reply or forward" button in zulip to forward a message verbatim with the code blocks within the quote blocks)

[David Thrane Christiansen]

Thanks! But this was not sent in Zulip, so I had to try to figure out the formatting myself.