CoeTC typeclass

Stream: mathlib4

[Oliver Nash]

I am still building up my understanding of coercions in Lean 4. Looking at the source in core here I note that the guidance is not to use CoeTC directly. However if I search Mathlib4 for instances I find lots. Even this basic search shows we have many.

[Oliver Nash]

Can someone who understands this properly comment on this? In particular is it correct that we have these instances. See also this comment for my motivation.

[Anne Baanen]

I suspect it's caused by #align has_coe_t CoeTC here. docs#has_coe_t and docs4#CoeTC do behave the same in terms of composition of docs#has_coe / docs4#Coe so it makes some level of sense that the automated port matches them.

[Anne Baanen]

As for manual porting, I believe it's best to replace new instances of CoeTC with docs4#CoeTail, which should have the same semantics as the Lean 3 usages of has_coe_t.

[Oliver Nash]

I see, so these CoeTC instances in Mathlib4 are generated by mathport when it sees has_coe_t instances in Mathlib3. (Indeed looking here I confirmed this is the case for the one that I encountered.) But you're saying that it might be better if instead mathport generated instances of CoeTail?

[Anne Baanen]

I'm not sure if that is possible because we don't want to have instances like docs#coe_trans returning a CoeTail. Although the exceptions to aligning has_coe_t to CoeTail should be easily enumerable, and in fact probably consist of the set { docs#coe_base, docs#coe_trans }

[Oliver Nash]

OK thanks. Perhaps there is some small improvement to be made but it doesn't seem like a priority.

[Oliver Nash]

I'm grateful for the explanations.