Different notation for coercion

Stream: general

[Peiran Wu]

MWE:

import Mathlib.GroupTheory.GroupAction.Defs

open MulAction

variable (G α : Type*) [Group G] [MulAction G α] (a : α)

#check (stabilizer G a : Type _) -- ↥(stabilizer G a) : Type u_1
#check (orbit G a : Type _) -- ↑(orbit G a) : Type u_2
#check (fixedPoints G α : Type _) -- ↑(fixedPoints G α) : Type u_2

Why is ↥ used in the first coercion, while the normal up arrow is used for the other two?

[Peiran Wu]

There is not much documentation for ↥ docs#coeSortNotation. I could deduce from the name that it is perhaps intended for CoeSort. But for example orbit G a is a set, and the coercion from a set to a type is docs#Set.instCoeSortType, yet ↑ is used.

[Robin Arnez]

Well, the way coercions are shown is defined by Lean.Meta.coeExt, registerable using Lean.Meta.registerCoercion. This process is completely disconnected from the coercions themselves, that is, defining a CoeSort instances still makes it display without the coercion arrow. To make sure the coercions are shown as such, usually the attribute @[coe] is used; however, this variant always registers them as ↑. To register them as ↥ notation, one needs to write

run_meta
  Lean.Meta.registerCoercion ``Set.Elem (some { numArgs := 2, coercee := 1, type := .coeSort })

This effort was apparently not done for Set.Elem. For Subgroup a completely different approach is used, using a custom delaborator:

@[app_delab Subtype]
def delabSubtypeSetLike : Delab := whenPPOption getPPNotation do
  -- ...
  `(↥$S)

[Peiran Wu]

Aha, thanks! This confirms my suspicion that it's an inconsistency in implementation, although the mechanism sounds a bit more complicated that I would have imagined.

Could we make it easier to maintain consistency? Would an alternative attribute @[coe_sort] make sense?

What's the mechanism behind the notation for CoeFun? It seems very consistent.

[Robin Arnez]

Same thing:

run_cmd Lean.Elab.Command.liftTermElabM do
  Lean.Meta.registerCoercion ``DFunLike.coe
    (some { numArgs := 5, coercee := 4, type := .coeFun })

(see Mathlib.Data.FunLike.Basic). The only difference I think is that DFunLike and FunLike are used more consistently.