ppSpace in elab/macro is ignored before constructor dot notation

[eric-wieser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

Using ppSpace in a parser does not always result in a space. As a result, syntax does not roundtrip.

Context

Zulip

Steps to Reproduce

1. Run the following:

import Lean.Elab.Command

macro (name := useSyntax) "use" ppSpace arg:term : tactic => `(tactic| sorry)

run_cmd do
  Lean.logInfo <| ← `(tactic| use .succ 0)

Expected behavior: Outputs use .succ✝ 0

Actual behavior: Outputs use.succ✝ 0, which is invalid syntax due to the missing space

Versions

4.10.0-nightly-2024-06-25

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

[kmill]

It looks like the issue is that when ppSpace is used as a macroArg without a variable name, it gets wrapped in a group, which inhibits inserting the space.

Is this a bug in whitespace insertion? Or should Lean.Elab.Command.expandMacroArg special case ppSpace?

import Lean

open Lean Lean.Parser.Command Lean.Elab.Command

elab "test_macroArg " args:macroArg* : command => do
    let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
    logInfo m!"{stxParts}"

test_macroArg ppSpace term,+
-- [group✝(ppSpace), sepBy1(term, ",", ", ")]
test_macroArg x:ppSpace term,+
-- [ppSpace, sepBy1(term, ",", ", ")]

elab "use1" ppSpace term,+ : tactic => failure
elab "use2" x:ppSpace term,+ : tactic => failure

run_cmd Lean.Elab.Command.liftTermElabM do
  Lean.logInfo <| ← `(tactic| use1 .succ 0) -- use1.succ✝ 0
  Lean.logInfo <| ← `(tactic| use2 .succ 0) -- use2 .succ✝ 0