Coercions

Stream: mathlib4

[Kevin Buzzard]

I have never understood Lean 4 coercions. There are the myriad typeclasses (Coe, CoeTC, CoeOut, CoeOTC, CoeHead, CoeHTC, CoeTail, CoeHTCT, CoeDep, CoeT, many of which are I think implementation details) as well as CoeFun and CoeSort (which I think I do understand) and then also the attribute @[coe] which I think is just for up-arrow notation. I just reviewed a PR on profinite groups and noticed this:

import Mathlib

variable (P : ProfiniteGrp.{0}) -- an object in the category of profinite groups.

#check (P : Type) -- ↑P.toProfinite.toTop : Type

Is that what we want to happen here? It looks a bit ridiculous to me, but I'm not sure that with the current set-up we can just make ↑P : Type be a thing because

instance : CoeSort ProfiniteGrp (Type u) where
  coe G := G.toProfinite

really means coe G := G.toProfinite.toTop.α and in particular there doesn't seem to be a bare function which we can tag with @[coe]. Are we just doomed to have this silly-looking ↑P.toProfinite.toTop in our goals?

[Eric Wieser]

It's always possible to write a custom delaborator that prints that specific term as a coercion

[Eric Wieser]

@[coe] is nothing more than a mechanism to reuse an existing delaborator in the simple cases

[Kevin Buzzard]

Eric Wieser said:

It's always possible to write a custom delaborator that prints that specific term as a coercion

If this delaborator were written for the example above (profinite groups to Type) then it would merely be a syntactic change, thus tidying up printed output, whilst having no affect on mathlib?

[Kyle Miller]

Eric Wieser said:

@[coe] is nothing more than a mechanism to reuse an existing delaborator in the simple cases

It's also the mechanism to configure the norm_cast tactics, which @Jireh Loreaux pointed out to me.

[Kyle Miller]

If you want a bare function to tag with @[coe], you can make one:

@[coe]
def ProfiniteGrp.toType (G : ProfiniteGrp) : Type u := G

instance : CoeSort ProfiniteGrp (Type u) where
  coe := ProfiniteGrp.toType

I think it's generally better to define coercions using an auxiliary function like this for this reason.

Presumably you'd have a simp lemma to rewrite ↑P.toProfinite.toTop to ↑P.

[Jireh Loreaux]

Agreed, I think auxiliary functions are likely the way to go here.

[Eric Wieser]

You probably want an abbrev not a def, otherwise you have to copy over all the instances again

[Mario Carneiro]

Do we have a linter that all Coe instances are tagged with @[coe]? Should we?

[Eric Wieser]

I don't think we should, I think there are cases where you want automatic insertion but you'd prefer to always see the full name in the goal view

[Eric Wieser]

But I guess there could be a @[no_coe_pp] attribute, and a linter that ensures either that or @[coe] is present

[Mario Carneiro]

I was thinking you would just use @[nolint] when you don't want to use @[coe]