Bug? Local instances not populated during delaboration

Stream: lean4

[Thomas Murrills]

I was testing #30266, which delaborates an algebra equivalence into Galois notation if a Field instance can be synthesized for some of its arguments, when I noticed that the local instances are not populated in DelabM. This leads to synthInstance? for Field A failing despite there being a variable [Field A] present (and present in the local context during delaboration).

MWE

import Lean
import Qq

open Lean Meta Elab PrettyPrinter Delaborator Qq Syntax

def Foo : Type := Unit

class Bar (α : Type) where

/-- Dummy declaration to attach our `app_delab` to, to mimic circumstances in #30266 -/
def baz (_ : Nat) : True := True.intro

/-- Syntax to embed our debugging logs in. -/
syntax "⟪" ppLine
-- Whether `Bar Foo` is synthesized
 &"synthBar" " := " term "," ppLine
 -- Types of terms in the local context
 &"lctx" " := " "[" term,* "]" "," ppLine
 -- List of local instance names
 &"localInstanceNames" " := " "[" ident,* "]" ppLine
 "⟫" : term

@[app_delab baz]
partial def delabBaz : Delab := whenPPOption getPPNotation do
  let synthBar := quote (← synthInstance? q(Bar Foo)).isSome
  let lctx : TSepArray `term "," ← (← getLocalHyps).mapM fun e =>
    withOptions (fun opts => opts.setBool `Lean.pp.notation false) do
      PrettyPrinter.delab <|← inferType e
  let localInstanceNames : TSepArray `ident "," :=
    (← getLocalInstances).map (mkIdent ·.className)
  `(⟪ synthBar := $synthBar,
    lctx := [$lctx,*],
    localInstanceNames := [$localInstanceNames,*]⟫)

variable [Bar Foo]

-- the `[Bar Foo]` instance is present in the local context, but not in the local instances
/--
info: ⟪
  synthBar := Bool.false✝,
  lctx := [Bar Foo],
  localInstanceNames := []
  ⟫ : True
-/
#guard_msgs in
#check baz 0

-- local instances are, as expected, correctly populated during elaboration
elab "test_elab%" : term => do
  logInfo m!"local instance names: {(← getLocalInstances).map (·.className)}"
  return q(true)

/--
info: local instance names: [Bar]
---
info: true : Bool
-/
#guard_msgs in
#check test_elab%

Is this a bug, or is this deliberate to avoid overhead during delaboration? (Should #30266 crawl the local context/populate the local instances manually?)

[Andrew Yang]

Here's some thing related:
The infoview seems to have different behaviour when pretty printing Tactic state and Expected type?

import Lean.PrettyPrinter.Delaborator.Basic

open Lean Meta PrettyPrinter Delaborator

class Bar where

def NoBar : Type := Unit

macro "YesBar":term => `(NoBar)

/-- Delaborates `NoBar` to `YesBar` if `Bar` instance is present. -/
@[app_delab NoBar]
partial def delabNoBar : Delab := whenPPOption getPPNotation do
  let some _ ← synthInstance? (mkConst ``Bar) | failure
  `(YesBar)

example [Bar] : NoBar := by
  /-
  Infoview when you place your cursor here:
  ▼ Tactic state
  1 goal
    inst✝ : Bar
    ⊢ YesBar
  -/
  exact .unit
  /-
  Infoview when you place your cursor on the end of the previous line:
  ▼ Tactic state
    No goals
  ▼ Expected type
    inst✝ : Bar
    ⊢ NoBar
  -/

[Aaron Liu]

we have docs#Mathlib.Meta.delabInf and docs#Mathlib.Meta.delabSup what do they do

[Andrew Yang]

They add the local instances back manually (i.e. withLocalInstances (← getLCtx).decls.toList.reduceOption do)

[Thomas Murrills]

Nice find! :) For visibility, #23558 is the PR in which that approach was introduced, and on which this issue was encountered was discussed.

@Kyle Miller mentioned on that PR that this was a 4.19 limitation; Kyle, do you happen to know if there's an issue associated with it and/or still plans to address it?

[Jovan Gerbscheid]

Yes, I made a PR to Lean that tried to fix this issue (and this is the fix that @Kyle Miller was referring to), but it turns out that the PR didn't fix it (or at least not in all situations)

[Thomas Murrills]

Ah, okay! Did that end up with a planned fix, a wontfix, or just a general postponement? I'm trying to figure out if this should be filed as an issue.

[Jovan Gerbscheid]

I think nobody else cared about it at that time, and I didn't make an issue, so feel free to make an issue about it now.

[Jovan Gerbscheid]

(My attempted fix was in lean#8022)

[Thomas Murrills]

I see, thanks! :) Issue: lean4#10830

[Thomas Murrills]

Aha, I think I've gotten to the bottom of this.

Pretty-printing works by starting with a PPContext, which looks like this:

structure PPContext where
  env           : Environment
  mctx          : MetavarContext := {}
  lctx          : LocalContext := {}
  opts          : Options := {}
  currNamespace : Name := Name.anonymous
  openDecls     : List OpenDecl := []

(Note the lack of localInstances....)

To pretty-print viaLean.ppExprWithInfos (ctx : PPContext) (e : Expr) : BaseIO FormatWithInfos using some such ctx, we look in the ppExt extension's state in ctx.env, which in turn is set by looking in the pretty-printing ref ppFnsRef. In there, you find an instance of a structure PPFns, which looks like this:

structure PPFns where
  ppExprWithInfos : PPContext → Expr → IO FormatWithInfos
  ppConstNameWithInfos : PPContext → Name → IO FormatWithInfos
  ppTerm : PPContext → Term → IO Format
  ppLevel : PPContext → Level → BaseIO Format
  ppGoal : PPContext → MVarId → IO Format

What do we set this field ppExprWithInfos to?

builtin_initialize
  ppFnsRef.set {
    ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e
    ppConstNameWithInfos := fun ctx n => ctx.runMetaM <| withoutContext <| ppConstNameWithInfos n
    ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx
    ppLevel := fun ctx l => return l.format (mvars := getPPMVarsLevels ctx.opts)
    ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId
  }

Note: that's Lean.Meta.ppExprWithInfos in the body, not to be confused with Lean.ppExprWithInfos above or the name of the field itself!

That ctx is a PPContext, and PPContext.runMetaM (Lean.Meta.Basic) looks like this:

def runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
  ppCtx.runCoreM <| x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }

It's there that localInstances acquires the value #[] by a default field value, I believe.

[Thomas Murrills]

So, we can either

1. give PPContext a field localInstances--this would mean constructing those at the different points we construct a PPContext
2. add the local instances to the context in PPContext.runMetaM
3. provide better documentation around DelabM if both of these are too burdensome performance-wise

[Thomas Murrills]

I'm experimenting with option 2 in lean4#10832. If it's not too bad when benched (fingers crossed! But my hopes aren't too high...), I'll clean it up and propose it... :)

[Thomas Murrills]

Here are the bench results (comparing the commit incorporating lean4#10832 to the one just before it, via benching PRs #30642 and #30643), though I'm not 100% sure how they should be interpreted. There's a good bit of orange, but not much shows up in the stddev column...

I'm also not sure if benching like this actually stress-tests pretty printing sufficiently well, especially if it's focused on building. If it doesn't, how would we tell if this change was making things more sluggish in the infoview?

[Jovan Gerbscheid]

I would think that

• this change doesn't affect performance much
• if it did affect performance, it would not be visible in the benchmarking since very little of the benchmarking time is spent on pretty printing.