Syntax match strange error

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

Pattern matching on syntax can lead to unexpected errors as in:

import Lean

open Lean Meta

def foo (t : Term) : Name :=
  match t with -- Failed to infer binder type
  | `($x:ident > 0) =>  .mkSimple <| x.getId.toString ++ "_pos"
  | `($x:ident > $y:ident) => .mkSimple <| x.getId.toString ++ "_gt_" ++ y.getId.toString
  | `($x:ident > $_) =>  x.getId
  | _ => `Bas

Context

See variations on https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Weird.20errors.20in.20quotation.20match

Steps to Reproduce

The above code is enough.

Expected behavior:

This definition should work

Actual behavior:

There is a “Failed to infer binder type” error on the match line.

Versions

4.27.0-rc1

Impact

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

Start with the self-contained foo definition in the issue and reproduce the error against Lean 4.27.0-rc1 and the latest nightly. Compare the quotation patterns in the match arms, then verify that the definition elaborates without “Failed to infer binder type” while preserving the expected Name results.