Strange linter behaviour

Stream: lean4

[IntGrah]

I get a discrepancy with linter behaviour after adding seemingly innocuous parentheses.

import Mathlib.Tactic.Linter.UnusedTactic

def foo (n : Nat) : Option (Fin (0 + n + 1)) := some ⟨n, by omega⟩

/-- warning:
'simpa only [Nat.zero_add] using ← foo n' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
-/
#guard_msgs in
def bad (n : Nat) : Option (Fin (n + 1)) := do
  return by simpa only [Nat.zero_add] using ← foo n

def good (n : Nat) : Option (Fin (n + 1)) := do
  return by simpa only [Nat.zero_add] using (← foo n)

The cause seems to be that the "← foo n" is getting lifted out

  let __foo_n ← foo n
  return by simpa only [Nat.zero_add] using __foo_n

and the simpa tactic source span isn't taking ownership of the synthetic __foo_n, causing the linter to see a broken simpa. Whereas with the parentheses, there is still some original syntax, and everything works.
I looked at the linter and it seems to rely on source spans. Is the bug in the linter, or in the elaborator?

[IntGrah]

I'm able to silence the error by editing
src/Lean/Elab/Do/Legacy.lean,
replacing line 1340

      let id ← mkIdentFromRef (.num baseId (← get).length)

with

      let id := mkIdentFrom term (.num baseId (← get).length) (canonical := true)

[IntGrah]

issue is still open, as the above message is only my guess of a solution hack