Local instances not populated during delaboration

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Local instances are not populated during delaboration, meaning that delaborators which synthesize instances to guide delaboration behave unexpectedly (and must populate the local instances themselves manually to behave correctly).

Context

This was noticed first in mathlib4#23558 (on Lean 4.19), and again in mathlib4#30266 (on Lean 4.24.0). Both add delaborators which attempt to synthesize an instance for the expressions involved to determine whether to continue delaboration.

This was discussed on Zulip here as well as on mathlib4#23558.

An attempted fix was made (and merged) in #8022, but this didn't fully address the issue.

Steps to Reproduce

1. Create a delaborator which attempts to synthesize an instance using synthInstance?.
2. Include that instance (only) in the local context, e.g. as a variable.
3. Use the delaborator in this local context.

Expected behavior: synthInstance? finds the instance, and delaboration proceeds accordingly.

Actual behavior: synthInstance? fails to find the instance.

Versions

4.19 through 4.25.0-nightly-2025-10-13

Additional Information

The following shows directly that synthInstance? fails because the local instances are not populated:

import Lean

open Lean Meta Elab PrettyPrinter Delaborator Syntax

class Bar where

syntax boolLit := &"true" <|> &"false"

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

/-- Syntax embedding debugging info for synthesizing `Bar`. -/
 def synthBarStxLog : MetaM Term := do
  let synthBar ← if (← synthInstance? (mkConst ``Bar)).isSome then `(boolLit|true) else `(boolLit|false)
  let lctx : TSepArray `term "," ← (← getLocalHyps).mapM fun e =>
    withOptions (·.setBool ``Lean.pp.notation false) do
      PrettyPrinter.delab <|← inferType e
  let localInstanceNames : TSepArray `ident "," :=
    (← getLocalInstances).map (mkIdent ·.className)
  `(⟪ synthBar := $synthBar,
    lctx := [$lctx,*],
    localInstanceNames := [$localInstanceNames,*]⟫)

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

@[app_delab foo]
partial def delabFoo : Delab := whenPPOption getPPNotation synthBarStxLog

variable [Bar]

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

-- As a control for the above code, local instances are, as expected, correctly populated during term elaboration.
elab "test_elab%" : term => do
  logInfo m!"{← synthBarStxLog}"
  return mkConst ``Unit.unit

/--
info: ⟪
  synthBar := true,
  lctx := [Bar],
  localInstanceNames := [Bar]
  ⟫
---
info: () : Unit
-/
#guard_msgs in
#check test_elab%

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the self-contained reproduction with the listed nightly versions and inspect the delaborator using synthInstance?, getLocalInstances, and synthBarStxLog. Compare its context with the test_elab% control case, then verify that the local [Bar] instance is visible during delaboration and that the #guard_msgs output shows synthBar := true.