Elaborated term size issue with syntax coercions

[gebner]

Most syntax coercions are declared like this:

instance : Coe Ident (TSyntax `Lean.Parser.Command.declId) where
  coe id := mkNode _ #[id, mkNullNode #[]]

Since we're inlining coercions during elaboration, this can blow up the term size a bit. In practice, it is probably eclipsed by the size of syntax quotations though.

Possible fixes:

1. Double where.

   instance : Coe Ident (TSyntax `Lean.Parser.Command.declId) where
   coe := coe where coe id := mkNode _ #[id, mkNullNode #[]]

2. Add an abstract macro (which creates an auxiliary declaration).

   instance : Coe Ident (TSyntax `Lean.Parser.Command.declId) where
   coe id := abstract mkNode _ #[id, mkNullNode #[]]

3. Add a macro to create these syntax coercions.

   tsyntax_coercion ident declId

4. Add macros that correctly setup coercion functions (and register them in the environment so that they can be found by tactics, delaborators, etc.). Note that we're going to do something like this in mathlib anyhow.

   @[coe]
   def Syntax.Ident.toDeclId (id : Ident) : TSyntax ``declId :=
   Unhygienic.run `(declId| $id:ident)

[Kha]

In practice, it is probably eclipsed by the size of syntax quotations though.

Right, given that we would get the same code inline anyway if we wrote either $x:ident or an actual ident, do we expect this to yield significant savings?

A question related to this issue is: should quotations instead use a custom, monadic coe typeclass so that we don't have to use Unygienic.run with the wrong getRef?

[gebner]

Right, given that we would get the same code inline anyway if we wrote either $x:ident or an actual ident, do we expect this to yield significant savings?

It seems like an easy win, anything that makes the syntax quotation code smaller is a positive change in my eyes. The really humongous instances are in mathport, so it would be great to have a good solution that doesn't entice users to shoot themselves in the foot like the following:

instance : Coe (TSyntax ``Parser.Term.structInst) Term where
  coe s := Unhygienic.run `($s:structInst)

A question related to this issue is: should quotations instead use a custom, monadic coe typeclass so that we don't have to use Unygienic.run with the wrong getRef?

I think this is a great idea. If we have a QuotM that is a reader with the source info, module name, and macro scope, then we can even use it for all of Quote, the syntax coercion class, and syntax quotations. That is, have dot-notation like `(this).unhygienic.

custom, monadic coe typeclass

Another reason why I like that change is because it decouples type-class search from coercions once again. There's always the plan lingering around that we might want to refactor coercions and no longer use type-classes for them.