parenthesizer backtrack errors?

Stream: lean4

[Daniel Selsam]

I see a bunch of "HACK" warnings in https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Parenthesizer.lean Are errors @ https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Parenthesizer.lean#L539 expected? Here is a short example that triggers it:

import Lean
open Lean Lean.PrettyPrinter.Delaborator

axiom Nat.mul2plus (n : Nat) : 2 * n = n + n

theorem foo (n : Nat) (h : 2 * n = n + n) : n + n = n + n := by
  simp only [Nat.mul2plus] at h
  exact h

@[delab app.Eq.mp]
def delabSimpHyp : Delab := do
  let arg := (← getExpr).appArg!
  let h := mkIdent (← Meta.getFVarLocalDecl arg).userName
  let lemmas := #[`Nat.mul2plus].map mkIdent
  `(by simp only [$[$lemmas:term],*] at $h)

#print foo -- parenthesizer backtracking exception

[Sebastian Ullrich]

Yes, these are expected/unavoidable if the syntax tree is malformed. In this case, it should be $h:ident.

[Daniel Selsam]

@Sebastian Ullrich Thanks, indeed $h:ident fixes it. Any suggestions for how I might have diagnosed/debugged that on my own?

[Sebastian Ullrich]

My line of reasoning basically was "I hope it's not a bug in the parenthesizer... so let's assume the syntax tree is malformed. $lemmas:term looks good, it is actually fed a term. So maybe $h is underspecified? Oh yeah, at also takes other arguments like *, so let's try :ident."

[Sebastian Ullrich]

But using quotations correctly in non-trivial syntax is simply tough right now. Ideally the original code should fail to typecheck because mkIdent should return some TSyntax `ident while $h would expect some TSyntax `location (or maybe the former even automatically coerces into the latter in the right way), but that would be a pretty fundamental and extensive change.