Weird errors in quotation match

Stream: lean4

[Patrick Massot]

Does anyone understands

import Lean

open Lean Meta

def foo (t : Term) : MetaM Name := do
  match t with
  | `($x:ident > 0) => return .mkSimple <| x.getId.toString ++ "_pos"
  | `($x:ident > $y:ident) => return .mkSimple <| x.getId.toString ++ "_gt_" ++ y.getId.toString
  | `($x:ident > $_) => return x.getId
  | _ => return `Bar -- typeclass instance problem is stuck

def foo' (t : Term) : MetaM Name := do
  let n : Name ← match t with -- Failed to infer binder type
    | `($x:ident > 0) => pure <| .mkSimple <| x.getId.toString ++ "_pos"
    | `($x:ident > $y:ident) => pure <| .mkSimple <| x.getId.toString ++ "_gt_" ++ y.getId.toString
    | `($x:ident > $_) => pure x.getId
    | _ => pure `Bar
  return n

[Patrick Massot]

Note: this is minimized from an example actually using MetaM but the following already fails:

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
  | _ => `Bar

[Patrick Massot]

Note this is very unstable: removing any of the three non-trivial cases gets rid of the error.

[Sebastian Ullrich]

I don't know what is happening there, surprised this hasn't come up before