`formatCommand` throws `uncaught backtrack exception` when a binder's type uses a doubly-declared notation

Prerequisites

• 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.

Description

When a notation token is declared twice, Lean.PrettyPrinter.formatCommand throws
format: uncaught backtrack exception on any command having a binder whose whole type is an application of that
notation. The command parses and elaborates fine; only formatting fails.

Only binder position fails, and the token kind does not matter — infixl, prefix, and notation all trigger it:

With only one of the two declarations, formatting succeeds.

Context

Mathlib declares infixl:51 " ⊨ " twice — Sentence.Realize at Mathlib/ModelTheory/Semantics.lean:634 and
Theory.Model at :736 — so any command with a binder (hM : M ⊨ T) is unformattable. This breaks tooling built on
formatCommand.

Steps to Reproduce

Toolchain only, no Mathlib. Save as Repro.lean and run lean Repro.lean:

import Lean
open Lean Parser PrettyPrinter

structure Th where
structure Md where

def realizeOne : Md → Th → Prop := fun _ _ => True
def realizeTwo : Md → Unit → Prop := fun _ _ => True

infixl:51 " ⊨ " => realizeOne
infixl:51 " ⊨ " => realizeTwo

def tryFmt (label s : String) : CoreM Unit := do
  match runParserCategory (← getEnv) `command s with
  | .error e => IO.println s!"{label}: parse error: {e}"
  | .ok stx =>
    try
      let fmt ← formatCommand stx
      IO.println s!"{label}: formatted: {fmt.pretty 100}"
    catch e => IO.println s!"{label}: THREW: {← e.toMessageData.toString}"

#eval show CoreM _ from do
  tryFmt "binder     " "theorem a (M : Md) (T : Th) (hM : M ⊨ T) : True := trivial"
  tryFmt "conclusion " "theorem b (M : Md) (T : Th) : M ⊨ T := trivial"
  tryFmt "body       " "def c (M : Md) (T : Th) : Prop := M ⊨ T"
  tryFmt "unambiguous" "theorem d (M : Md) (T : Th) (hM : realizeOne M T) : True := trivial"

Expected behavior: all four format.

Actual behavior:

binder     : THREW: format: uncaught backtrack exception
conclusion : formatted: theorem b (M : Md) (T : Th) : M ⊨ T :=
  trivial
body       : formatted: def c (M : Md) (T : Th) : Prop :=
  M ⊨ T
unambiguous: formatted: theorem d (M : Md) (T : Th) (hM : realizeOne M T) : True :=
  trivial

Replacing both infixl lines with two prefix:max "◇" declarations, or with two notation:max "⟦" x "⟧" declarations,
throws identically in binder position.

Additional Information

The orelse.formatter / categoryFormatterCore "format only last choice" path in
src/Lean/PrettyPrinter/Formatter.lean appears to pick an alternative whose formatter cannot accept the node, and the
backtrack escapes uncaught. That code's own TODO notes it wants the elaborator's choice, which is what would
disambiguate here.

Versions

Reproduced identically on Lean 4.33.0-rc1 (62eed1db4d67327ec8120be05f1a1b0847d74561) and nightly-2026-07-31
(5b8d06c1764fa367a1e27b3e89f64667eac425af), arm64-apple-darwin.

Impact

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

Start with src/Lean/PrettyPrinter/Formatter.lean, especially the orelse.formatter and categoryFormatterCore paths mentioned in the report. Run the self-contained Repro.lean case first, then trace why the binder formatter backtracks with duplicate notation declarations. Done means all four examples format without an uncaught backtrack exception and the relevant formatter tests pass.