Syntax match strange error

[PatrickMassot]

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.