Syntax pattern $foo:with_type fails unhelpfully

This papercut in error reporting has been causing me mild frustration and prevented me from figuring out syntax by trying, maybe it can be improved:

import Lean

def bar := leading_parser "a_bar"
def foo := leading_parser bar

namespace Works
def test (stx : Lean.Syntax) : Bool := 
  match stx with
  | `(foo| $bar:bar) => true
  | _ => false
end Works

namespace FailsUnhelpfully
def test (stx : Lean.Syntax) : Bool := 
  match stx with
  | `(foo| $bar:barr) => true
  | _ => false

end FailsUnhelpfully

If I want to use a “parser annotation”(?) in a syntax pattern, but mistype the parser (or don’t have it in scope), I get

unexpected token '$'; expected 'a_bar', 'bar' or 'foo'

What I’d like to see is something telling me that barr isn't in scope.

My guess is that somewhere this name lookup fails, but the parser’s backtracking backtracks that error, when instead it (maybe?) should be a non-backtrackable error?

Versions

4.3.0-rc2

Impact

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

Begin by running the supplied Lean.Syntax pattern reproducer, comparing the working bar annotation with the misspelled barr case. Trace parser-annotation name lookup and error backtracking; done means an out-of-scope or unknown parser name produces a direct diagnostic instead of the generic unexpected-token message.