fix: ghost goals in autoparam tactic block (#6408)

This PR fixes a regression where goals that don't exist were being
displayed. The regression was triggered by #5835 and originally caused
by #4926.

Bug originally reported at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/tactic.20doesn't.20change.20primary.20goal.20state/near/488957772.

The cause of this issue was that #5835 made certain `SourceInfo`s
canonical, which was directly transferred to several `TacticInfo`s by
#4926. The goal state selection mechanism would then pick up these extra
`TacticInfo`s.

The approach taken by this PR is to ensure that the `SourceInfo` that is
being transferred by #4926 is noncanonical.

src/Lean/Elab/App.lean

@@ -628,7 +628,7 @@ mutual
           (in particular, `Lean.Elab.Term.withReuseContext`) controls the ref to avoid leakage of outside data.
           Note that `tacticSyntax` contains no position information itself, since it is erased by `Lean.Elab.Term.quoteAutoTactic`.
           -/
-          let info := (← getRef).getHeadInfo
+          let info := (← getRef).getHeadInfo.nonCanonicalSynthetic
           let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
           let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName)
           -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.

src/Lean/Elab/StructInst.lean

@@ -853,7 +853,7 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
               let stx ← `(by $tacticSyntax)
               -- See comment in `Lean.Elab.Term.ElabAppArgs.processExplicitArg` about `tacticSyntax`.
               -- We add info to get reliable positions for messages from evaluating the tactic script.
-              let info := field.ref.getHeadInfo
+              let info := field.ref.getHeadInfo.nonCanonicalSynthetic
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
               let type := (d.getArg! 0).consumeTypeAnnotations
               let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)

src/Lean/Syntax.lean

@@ -33,6 +33,16 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
 def SourceInfo.getRange? (canonicalOnly := false) (info : SourceInfo) : Option String.Range :=
   return ⟨(← info.getPos? canonicalOnly), (← info.getTailPos? canonicalOnly)⟩
 
+/--
+Converts an `original` or `synthetic (canonical := true)` `SourceInfo` to a
+`synthetic (canonical := false)` `SourceInfo`.
+This is sometimes useful when `SourceInfo` is being moved around between `Syntax`es.
+-/
+def SourceInfo.nonCanonicalSynthetic : SourceInfo → SourceInfo
+  | SourceInfo.original _ pos _ endPos => SourceInfo.synthetic pos endPos false
+  | SourceInfo.synthetic pos endPos _  => SourceInfo.synthetic pos endPos false
+  | SourceInfo.none                    => SourceInfo.none
+
 deriving instance BEq for SourceInfo
 
 /-! # Syntax AST -/

tests/lean/interactive/ghostGoals.lean

@@ -0,0 +1,19 @@
+-- Issue originally reported at
+-- https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/tactic.20doesn't.20change.20primary.20goal.20state/near/488957772
+class Preorder (α : Type) extends LE α, LT α where
+  le_refl : ∀ a : α, a ≤ a
+  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+  lt := fun a b => a ≤ b ∧ ¬b ≤ a
+  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+
+class PartialOrder (α : Type) extends Preorder α where
+  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
+
+instance : PartialOrder Nat where
+  le := (· ≤ ·)
+  le_refl := Nat.le_refl
+  le_trans a b c := Nat.le_trans
+  le_antisymm := by
+    intro x
+      -- One goal: x : Nat ⊢ ∀ (b : Nat), x ≤ b → b ≤ x → x = b
+  --^ $/lean/plainGoal

tests/lean/interactive/ghostGoals.lean.expected.out

@@ -0,0 +1,4 @@
+{"textDocument": {"uri": "file:///ghostGoals.lean"},
+ "position": {"line": 17, "character": 4}}
+{"rendered": "```lean\nx : Nat\n⊢ ∀ (b : Nat), x ≤ b → b ≤ x → x = b\n```",
+ "goals": ["x : Nat\n⊢ ∀ (b : Nat), x ≤ b → b ≤ x → x = b"]}