Delaborator omits an instance binder's name when it is used only in a later binder's type

Prerequisites

• Check that your issue is not already filed
• 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

Description

When printing a fun, the delaborator drops the name of an instance-implicit binder if the name does not occur in the innermost body — but it still prints the name in the types of the binders that follow. The result references a variable it never bound, so pp.all output cannot be re-elaborated.

Steps to Reproduce

universe u
class E (α : Type u) [BEq α] : Prop where
  h : True

def g : {α : Type u} → [BEq α] → (x : E α → Nat) → Nat :=
  fun {α} [BEq α] (x : E α → Nat) => 0

set_option pp.all true in
#print g
-- def g.{u} : {α : Type u} → [inst : BEq.{u} α] → (x : @E.{u} α inst → Nat) → Nat :=
-- fun {α : Type u} [BEq.{u} α] (x : @E.{u} α inst → Nat) => @OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))
--                  ^^^^^^^^^^^^ no name              ^^^^ but used here

Re-elaborating the printed value gives Unknown identifier 'inst'. The signature line (a ∀) is printed correctly; only the fun is affected.

Expected behavior: fun {α : Type u} [inst : BEq.{u} α] (x : @E.{u} α inst → Nat) => … — as v4.20.0 prints it.

Actual behavior: the binder is printed anonymously while a later binder type refers to inst.

Versions

• Lean 4.35.0-nightly-2026-09-04, arm64-apple-darwin24.6.0 macOS — wrong
• Lean 4.33.1 (stable) — wrong
• Lean 4.20.0 — correct

Additional Information

Cause. In Lean/PrettyPrinter/Delaborator/Builtins.lean, the instance-implicit case of the fun binder delaborator decides whether to keep the name with

-- Approximation: if the name does not appear in the pretty printed body
-- then don't use the name, even if it is dependent.
if dep && curNames.any (fun n => stxBody.raw.hasIdent n.getId) then

but a few lines earlier the nested fun has already been peeled apart — match stxBody with | \(fun $binderGroups* => $stxBody) => (binderGroups, stxBody)— sostxBodyis only the innermost body and the peeledbinderGroups, whose types may mention the name, are never searched. The ∀ path (delabForallBinders) keeps the name whenever dependent, which is why signatures are fine. Checking binderGroupsas well asstxBody(or simply trustingdep`) would fix it.

Scope. On the current nightly this affects every casesOn of a Prop-valued class with instance parameters, because those are now constructed as mk t.1 — the body no longer mentions the instance, only the motive binder's type does. A mechanical pp.all round-trip over all 19,868 definition values in Init and Std finds 276 values that fail with Unknown identifier 'inst' (or inst_1, inst_2) for this reason, e.g. EquivBEq.casesOn, PartialEquivBEq.casesOn, LawfulMonadLift.casesOn, Std.PRange.LawfulUpwardEnumerableLE.casesOn. On 4.33.1 those particular values print correctly because the older casesOn body (@E.rec α inst …) happens to mention inst; the underlying check is wrong on both.

Related round-trip reports from the same sweep: #15035, #15036.

Investigation assisted by Claude; repros run and checked manually.

Impact

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

Start in Lean/PrettyPrinter/Delaborator/Builtins.lean at the instance-implicit fun binder logic and compare the peeled binderGroups with stxBody when deciding whether to retain a dependent binder name. Run the minimal reproduction with pp.all enabled, then verify the printed definition can be re-elaborated without an Unknown identifier error.