format: uncaught backtrack exception

Stream: lean4

[Eric Wieser]

Minimized from mathlib:

import Lean

open Lean

def AddMonoidAlgebra (R A : Type) : Type := Unit

notation:9000 R:max "[" A "]" => AddMonoidAlgebra R A

-- format: uncaught backtrack exception
#eval do PrettyPrinter.ppTerm <| ← `(term| ∀ (f : R[A]), true)

[Eric Wieser]

This only seems to happen when the custom notation is used in a binder

[Eric Wieser]

It looks like this is interfering with array indexing notation?

[Mario Carneiro]

the syntax quotation is producing a choice node

[Mario Carneiro]

if you make the notation high or low priority then it will not do this

[Mario Carneiro]

@Sebastian Ullrich It appears this is an unusual interaction of formatter combinators and ungrouped optional nodes.

import Lean

open Lean

syntax:9000 (name := foo) term:max "  [" term "-]" : term
syntax:9000 (name := foo2) term:max " [" term "-]" : term

run_meta
  -- let stx ← `(Parser.Term.bracketedBinderF| (f : R[A]))
  let stx ← `(Parser.Term.bracketedBinderF| (f : R[A-]))
  _ ← PrettyPrinter.format Parser.Term.explicitBinder.formatter stx

Here's my test after inlining things to add logging

import Lean

open Lean

syntax:9000 (name := foo) term:max "  [" term "-]" : term
syntax:9000 (name := foo2) term:max " [" term "-]" : term

open PrettyPrinter Formatter Syntax.MonadTraverser

def tag (s : String) (p : Formatter) : Formatter := do
  let stx ← getCur
  let t ← (inferInstance : Syntax.MonadTraverser FormatterM).st.get
  logInfo f!"{s} [{t.parents}]: {stx}"
  try
    p
    let stx ← getCur
    logInfo f!"after {s}: {stx}"
  catch e =>
    logInfo m!"{s} failed"
    let stx ← getCur
    logInfo f!"after {s}: {stx}"
    throw e

def Lean.Parser.Term.binderType.formatter' : Formatter := do
  let p := andthen.formatter (Parser.symbol.formatter " : ") Parser.termParser.formatter
  let kind := `optional
  let suffix := Parser.symbol.formatter "?"
  optionalNoAntiquot.formatter (
    tag "withAntiquot" <|
    orelse.formatter
      (tag "t1" <| Parser.mkAntiquotSplice.formatter kind (withoutInfo.formatter p) suffix)
      (tag "t2" <| withAntiquotSuffixSplice.formatter kind p suffix))

def Lean.Parser.Term.explicitBinder.formatter' : Formatter :=
  Parser.ppGroup.formatter
    (Parser.leadingNode.formatter `Lean.Parser.Term.explicitBinder 1024
      (andthen.formatter (Parser.symbol.formatter "(")
        (andthen.formatter
          (Parser.withoutPosition.formatter
            (andthen.formatter (Parser.many1.formatter Parser.Term.binderIdent.formatter)
              (andthen.formatter Parser.Term.binderType.formatter'
                (Parser.optional.formatter
                  (orelse.formatter Parser.Term.binderTactic.formatter Parser.Term.binderDefault.formatter)))))
          (Parser.symbol.formatter ")"))))

run_meta
  let stx ← `(Parser.Term.bracketedBinderF| (f : R[A-]))
  _ ← PrettyPrinter.format Parser.Term.explicitBinder.formatter' stx

When testing with the non-overloaded syntax R[A], the optional node in binderType is of the form [":" (term_[_] ...)], and optionalNoAntiquot.formatter zooms in on the first subterm (term_[_] ...), which is consumed by term (which moves the cursor to ":") and then ":" as intended.

With the overloaded syntax R[A-], the optional node is instead [":" (choice (foo ...) (foo2 ...))], and again optionalNoAntiquot.formatter zooms in on (choice (foo ...) (foo2 ...)). But then we use orelse.formatter (actually withAntiquot.formatter) in order to try a possible antiquot at this position, and orelse.formatter strips choice nodes, so it zooms in further to (foo2 ...); applying term here succeeds and moves to the left to (foo ...) and applying ":" here fails.

[Mario Carneiro]

I think the issue is that orelse.formatter has an implementation which doesn't make sense if the provided formatters p1 and p2 have arity > 1, which is the case here because p2 is ":" >> term

[Eric Wieser]

(src#orelse.formatter)