SourceInfo in quoted but not parsed syntax

Stream: lean4

[Thomas Murrills]

It seems that when forming syntax via syntax quotation, synthetic source info can get inserted even in positions that parsing usually does not insert source info. This can change where messages are logged.

The following is a minimized issue that occurs in the new tactic analysis framework which causes messages to be logged at the current ref instead of on the tactic sequence:

import Lean

open Lean

elab "#show_parsed " t:tacticSeq : command => do
  logInfoAt t (repr t)

elab "#show_quoted " ts:tactic* : command => do
  let t ← `(tacticSeq|$ts:tactic*)
  logInfoAt t (repr t)

#show_parsed
  intro a -- info logged on this line
  intro b

#show_quoted -- info logged on this line
  intro a
  intro b

One can see that the syntax created in #show_quoted retains its original source info, but also has synthetic source info near the top of the tree, whereas the parsed tacticSeq has no such info.

I'm not sure if this is an issue or not. I can imagine that sometimes we want to eagerly add source info from the ref when constructing synthetic syntax (so that we're more likely to have position info than not at the end of the day), but it's a bit unusual to me that it's added despite having perfectly good source info in the syntax we're using to construct it (and that it's being added in a place it isn't "naturally" added), so I thought I'd bring it up here.

(Note: it's not too hard to work around this to get correct logging with e.g. withRef (mkNullNode ts) `(tacticSeq|$ts:tactic*), or even MonadRef.withRef .missing `(tacticSeq|$ts:tactic*).)