Roundtripping delaboration involving coercions

Stream: metaprogramming / tactics

[Jannis Limperg]

The term 0 ≤ (↑n : Int) delaborates as 0 ≤ ↑n, which then re-elaborates as 0 ≤ n, so the coercion is lost (even with pp.analyze):

import Lean

open Lean Lean.Meta Lean.Elab.Term Lean.PrettyPrinter in
#eval show TermElabM Unit from do
  withLocalDeclD `n (.const ``Nat []) λ _ => do
    let type ← elabTerm (← `(0 ≤ (↑$(mkIdent `n) : Int))) none
    synthesizeSyntheticMVarsNoPostponing
    let delabed ← withOptions (pp.analyze.set · true) $ delab type
    logInfo m!"delaborated: {delabed}"
    let type' ← elabTerm delabed none
    synthesizeSyntheticMVarsNoPostponing
    logInfo m!"re-elaborated: {type'}"
    logInfo m!"defeq: {← isDefEq type type'}"

/-
delaborated: 0 ≤ ↑n

re-elaborated: 0 ≤ n

defeq: false
-/

Is this considered a bug? And is there anything I can do to make the delaborator print the type ascription? cc @Kyle Miller

Context: I use the delaborator to generate tactic scripts in aesop? and this behaviour came up in one of my tests.

[Kyle Miller]

I think that could be considered to be a bug in pp.analyze.

There should probably also be a pp option to print type ascriptions for coercions as well. (pp.analyze would then interact with this option.)

[Jannis Limperg]

lean4#4315. Thanks!

[Tony Beta Lambda]

I think I can help with this issue. Here are my thoughts on possible solutions:

a) Modify analyze. Add a new option, pp.analyze.typedCoercions (name up to discussion) that, when enabled, will cause pp.analyze annotate all coercions with pp.analysis.needsType.

pros: better separation of concerns (analyze is responsible for type ascriptions)
cons: typedCoercions have no effect if typeAscriptions is not enabled; the user have no option to enable type ascriptions only for coercions (which might be desirable)

b) Modify coeDelaborator. Add a new option, pp.coercions.typeAscriptions, that takes effect within coeDelaborator to cause it to add ascriptions to delaborated term.
pros: better control over delab process.
cons: the user has no central control over whether/how type ascriptions are added.

I'm leaning towards the second option. Any comments/suggestions?

[Kyle Miller]

I invite you to implement pp.coercions.types, which is one of those things I've been meaning to get around to. There is a combinator that should make this easy -- make sure to see how other builtin delaborators add ascriptions.

[Kyle Miller]

Re pp.analyze, let's avoid touching it. I would rather make it intelligently add ascriptions when necessary, and if the option is "always add an ascription" we shouldn't be setting that option indirectly through pp.analyze.

[Tony Beta Lambda]

https://github.com/leanprover/lean4/pull/6119