fix: ensure autoparam errors have correct positions (#4926)

Autoparam tactic scripts have no source positions, which until recently
made it so that any errors or messages would be logged at the current
ref, which was the application or structure instance being elaborated.
However, with the new incrementality features the ref is now carefully
managed to avoid leakage of outside data. This inhibits the elaborator's
ref from being used for the tactic's ref, causing messages to be placed
at the beginning of the file rather than on the syntax that triggered
the autoparam.

To fix this, now the elaborators insert the ref's source position
everywhere into the autoparam tactic script.

If in the future messages for synthetic tactics appear at the tops of
files in other contexts, we should consider an approach where
`Lean.Elab.Term.withReuseContext` uses something like `replaceRef` to
set the ref while disabling incrementality when the tactic does not
contain source position information.

Closes #4880

src/Lean/Elab/App.lean

@@ -541,7 +541,7 @@ mutual
   /--
     Process a `fType` of the form `(x : A) → B x`.
     This method assume `fType` is a function type -/
-  private partial def processExplictArg (argName : Name) : M Expr := do
+  private partial def processExplicitArg (argName : Name) : M Expr := do
     match (← get).args with
     | arg::args =>
       if (← anyNamedArgDependsOnCurrent) then
@@ -586,6 +586,16 @@ mutual
         | Except.ok tacticSyntax =>
           -- TODO(Leo): does this work correctly for tactic sequences?
           let tacticBlock ← `(by $(⟨tacticSyntax⟩))
+          /-
+          We insert position information from the current ref into `stx` everywhere, simulating this being
+          a tactic script inserted by the user, which ensures error messages and logging will always be attributed
+          to this application rather than sometimes being placed at position (1,0) in the file.
+          Placing position information on `by` syntax alone is not sufficient since incrementality
+          (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 tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
           let argNew := Arg.stx tacticBlock
           propagateExpectedType argNew
           elabAndAddNewArg argName argNew
@@ -615,7 +625,7 @@ mutual
     This method assume `fType` is a function type -/
   private partial def processImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      processExplictArg argName
+      processExplicitArg argName
     else
       addImplicitArg argName
 
@@ -624,7 +634,7 @@ mutual
     This method assume `fType` is a function type -/
   private partial def processStrictImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      processExplictArg argName
+      processExplicitArg argName
     else if (← hasArgsToProcess) then
       addImplicitArg argName
     else
@@ -643,7 +653,7 @@ mutual
         addNewArg argName arg
         main
       else
-        processExplictArg argName
+        processExplicitArg argName
     else
       let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
       addInstMVar arg.mvarId!
@@ -668,7 +678,7 @@ mutual
         | .implicit       => processImplicitArg binderName
         | .instImplicit   => processInstImplicitArg binderName
         | .strictImplicit => processStrictImplicitArg binderName
-        | _               => processExplictArg binderName
+        | _               => processExplicitArg binderName
     else if (← hasArgsToProcess) then
       synthesizePendingAndNormalizeFunType
       main

src/Lean/Elab/StructInst.lean

@@ -677,6 +677,10 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
             | .error err       => throwError err
             | .ok tacticSyntax =>
               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 stx := stx.raw.rewriteBottomUp (·.setInfo info)
               cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field
           | _ =>
             if bi == .instImplicit then

tests/lean/interactive/4880.lean

@@ -0,0 +1,36 @@
+/-!
+# Ensure autoparam errors are placed at elaboration position
+
+Before, errors were placed at the beginning of the file.
+-/
+
+
+/-!
+Testing `infer_instance`, which defers a typeclass problem beyond the tactic script execution.
+-/
+class A
+
+-- For structure instance elaboration ...
+structure B where
+  h1 : A := by infer_instance
+
+example : B where
+          --^ collectDiagnostics
+
+-- ... and for app elaboration.
+def baz (_h1 : A := by infer_instance) : Nat := 1
+
+example : Nat := baz
+               --^ collectDiagnostics
+
+
+/-!
+Testing a tactic that immediately throws an error, but incrementality resets the ref
+from the syntax for the tactic (which would be a `.missing` position for autoparams).
+-/
+
+structure B' where
+  h1 : A := by done
+
+example : B' where
+           --^ collectDiagnostics

tests/lean/interactive/4880.lean.expected.out

@@ -0,0 +1,32 @@
+{"version": 1,
+ "uri": "file:///4880.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 16, "character": 12},
+    "end": {"line": 16, "character": 17}},
+   "message":
+   "failed to synthesize\n  A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "fullRange":
+   {"start": {"line": 16, "character": 12},
+    "end": {"line": 16, "character": 17}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 22, "character": 17},
+    "end": {"line": 22, "character": 20}},
+   "message":
+   "failed to synthesize\n  A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "fullRange":
+   {"start": {"line": 22, "character": 17},
+    "end": {"line": 22, "character": 20}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 34, "character": 13},
+    "end": {"line": 34, "character": 18}},
+   "message": "unsolved goals\n⊢ A",
+   "fullRange":
+   {"start": {"line": 34, "character": 13},
+    "end": {"line": 34, "character": 18}}}]}