Using forall binders as function binders

Stream: metaprogramming / tactics

[Jonathan Chan]

What's the best way to reuse forall binders as function binders in a macro? I'd like to implement a function like this:

-- this is `(binderIdent <|> bracketedBinder)`
def binderKinds : SyntaxNodeKinds :=
  [`ident, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder]

-- create a pair of type `Σ' (A : Sort _), A` with a hole `⟨(∀ binders, sig), (λ binders ↦ ?name)⟩`
def mkPair
  (name : TSyntax `ident)
  (binders : TSyntaxArray binderKinds)
  (sig : TSyntax `term) : MacroM (TSyntax `term) := do
  `(PSigma.mk (∀ $binders*, $sig) (λ $binders* ↦ ?$name))

The parser for functions asks for `Lean.Parser.Term.funBinder, which I see includes all of the bracketed forms including implicit and instance arguments, so it should be possible to map my binders to funBinders. Is there some way to coerce this, or should I manually match on the binder syntax and reconstruct them as funBinders?

[Jonathan Chan]

For reference, I used a coercion:

instance : Coe (TSyntax binderKinds) (TSyntax `Lean.Parser.Term.funBinder) where
  coe stx := ⟨stx.raw⟩

which feels like cheating, but I haven't encountered an unexpected parse error yet...