field Notation prints unprovable goal as `bla = bla`

Prerequisites

• [ X] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [ X] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [ X] 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

As Aaron Liu puts it:
if you have a : A and a function B.foo and A extends B then B.foo a.toB will pretty print as a.foo

This is very overeager by the pretty printer and will lead to a very undesirable output if a.foo already exists (it may have a completely unrelated definition!).

opaque Calculus : Type u

opaque P : Calculus -> Prop

axiom c1 : Calculus
axiom c2 : Calculus

structure BaseSpecification where
  param : Nat

structure ExtendedSpecification extends BaseSpecification where
  extra : Nat


noncomputable def ExtendedSpecification.toCalc (e : ExtendedSpecification) : Calculus := c1

def BaseSpecification.toExtendSpecification (e : BaseSpecification) : ExtendedSpecification where
  toBaseSpecification := e
  extra := 0

noncomputable def BaseSpecification.toCalc (e : BaseSpecification) : Calculus := c2

/--
trace: e : ExtendedSpecification
⊢ P e.toCalc ↔ P e.toCalc
---
warning: declaration uses `sorry`
-/
#guard_msgs in
theorem the_problem (e : ExtendedSpecification) :
    P (ExtendedSpecification.toCalc e)
    ↔ P (BaseSpecification.toCalc e.toBaseSpecification) := by
  trace_state
  sorry -- this is unprovable!


-- removing field notation shows that the fieldnotation was the problem
set_option pp.fieldNotation false

/--
trace: e : ExtendedSpecification
⊢ P (ExtendedSpecification.toCalc e) ↔ P (BaseSpecification.toCalc (ExtendedSpecification.toBaseSpecification e))
---
warning: declaration uses `sorry`
-/
#guard_msgs in
theorem the_problem2 (e : ExtendedSpecification) :
    P (ExtendedSpecification.toCalc e)
    ↔ P (BaseSpecification.toCalc e.toBaseSpecification) := by
  trace_state
  sorry -- this is still unprovable, but now it doesn't act like it's trivially provable!

Context

Zulip Thread from the issue discovery:

In my current project formalizing Saturation Calculi completeness i have multiple of these kinds of definitions and the goals are extremely confusing because of this bug.

To be able to trust an interactive theorem prover, one also needs to be able to trust its output machinery so that we can be sure we are proving what we think we are proving.
In this sense, this is a pretty serious bug.

Versions

"4.30.0-nightly-2026-03-18"

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 minimal Lean reproducer and compare trace_state with pp.fieldNotation false, focusing on the field-notation pretty-printing path and #guard_msgs output. Done means the two distinct toCalc expressions are no longer printed as the same goal, with the reproducer's messages updated accordingly.