`pp.all` output does not round-trip when a local's type has `optParam`/`autoParam` binders

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

pp.all prints constants with @, but prints local variables bare. When a local's type has an optParam (or autoParam) binder and the local is passed unapplied, re-elaborating the printed text eta-expands the local and fills in the default, producing a type mismatch. Writing @f for the local makes the printed form re-elaborate.

This came out of a mechanical round-trip check over every declaration in Init and Std (delaborate the type with pp.all, re-parse, re-elaborate, compare): 74,535 of 76,100 round-trip syntactically and 1,333 up to defeq; this is one of the few genuine failures. In core it affects Std.Async.MonadAsync.{casesOn, rec, recOn, mk.noConfusion} (an optParam field) and the Nat.dfoldRev_* lemmas (autoParam in the type of a binder).

Steps to Reproduce

universe u

structure S where
  f : Nat → optParam Nat 0 → Nat

set_option pp.all true in
#check @S.casesOn
-- {motive : (t : S) → Sort u_1} → (t : S) →
--   (mk : (f : Nat → optParam.{1} Nat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) → Nat) → motive (S.mk f)) →
--   motive t

-- Re-elaborating that (defaults abbreviated) fails:
#check ({motive : S → Sort u} → (t : S) → (mk : (f : Nat → optParam.{1} Nat 0 → Nat) → motive (S.mk f)) → motive t)
-- error: Application type mismatch: The argument
--   fun a => f a 0
-- has type
--   Nat → Nat
-- but is expected to have type
--   Nat → optParam Nat 0 → Nat
-- in the application
--   { f := fun a => f a 0 }

-- With `@f` it elaborates:
#check ({motive : S → Sort u} → (t : S) → (mk : (f : Nat → optParam.{1} Nat 0 → Nat) → motive (S.mk @f)) → motive t)

The same happens for a plain hypothesis, not just a structure field:

example (h : Nat → optParam Nat 0 → Nat) : (Nat → optParam Nat 0 → Nat) := h    -- fails
example (h : Nat → optParam Nat 0 → Nat) : (Nat → optParam Nat 0 → Nat) := @h   -- ok

Expected behavior: the pp.all output re-elaborates to the original term — e.g. by printing @f for a local whose type has optParam/autoParam binders when it appears as an unapplied argument, the way constants already get @.

Actual behavior: the printed text fails to elaborate.

Versions

• Lean 4.35.0-nightly-2026-09-04, arm64-apple-darwin24.6.0 macOS
• Lean 4.33.1 (stable) — same
• Lean 4.20.0 — same (long-standing, not a regression)

Additional Information

The elaborator behaviour itself (eta-expanding a bare local with default-valued binders) may be intended; this report is about the delaborator not producing text that survives it. The same sweep found two other non-round-tripping classes that look like limitations rather than bugs — public casesOn/rec declarations whose types mention private constructors print unparseable _private.…0.… names, and inferInstance's [i : α] binder fails the binder-annotation check — mentioned only for completeness.

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 with the minimal reproductions using set_option pp.all true and the optParam/autoParam examples, then trace the pp.all delaborator path for unapplied locals. Done means the printed output re-elaborates to the original term, including the Std.Async.MonadAsync and Nat.dfoldRev_* cases.