`do` lifting is not handled correctly in antiquotations

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

When building Syntax or Qq quotations involving a do $(← getArg) antiquotation, the parser rejects the ← even if there is a suitable enclosing do block. This is unexpected; the lifting behavior of antiquotations should be unaffected by the syntax that they are interpolated within.

Context

This issue also arises with if $(← getCond) then _ else _ quotations after #3820.

Steps to Reproduce

1. Run the following

import Lean
open Lean

def foo : MetaM (TSyntax ``Parser.Term.doSeq) := do `(Parser.Term.doSeq| pure 37)

#check do `(do $(← foo))

#check do
  let mkDo x := `(do $x)
  mkDo (← foo)

Expected behavior: Both #checks succeed

Actual behavior: The first one fails, with the error

invalid use of (<- ...), must be nested inside a 'do' expression

Versions

4.7.0-rc2

Impact

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

Start with the minimal Lean reproduction in the issue and inspect how Syntax or Qq quotations process antiquotations containing ← inside do expressions. Run both #check examples to confirm the current failure. Done means both checks succeed, including the mkDo example and the related quotation behavior described after #3820.