From e78fc220b02a5f77665f4938b2fcaf0012849029 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 25 Sep 2024 13:03:54 -0700
Subject: [PATCH 1/5] feat: have autoparams report parameter/field on failure

Adds mechanism where when a autoparam tactic fails to synthesize a parameter, the associated parameter or field name for the autoparam is reported in an error.

Notes:
* Autoparams now run their tactics without any error recovery or error-to-sorry enabled. This enables catching the error and reporting the contextual information.
* Autoparams for applications now cleanup the autoParam annotation, brining it in line with autoparams for structure fields.

Closes #2950
---
 src/Lean/Elab/App.lean                        |  4 +--
 src/Lean/Elab/BuiltinTerm.lean                | 18 +---------
 src/Lean/Elab/StructInst.lean                 |  4 ++-
 src/Lean/Elab/SyntheticMVars.lean             | 27 +++++++++++----
 src/Lean/Elab/Tactic/Simp.lean                |  2 +-
 src/Lean/Elab/Term.lean                       | 31 ++++++++++++++++-
 tests/lean/interactive/4880.lean.expected.out | 19 +++++++++++
 tests/lean/run/autoparam.lean                 | 33 +++++++++++++++++++
 tests/lean/run/mergeSort.lean                 |  4 +++
 9 files changed, 114 insertions(+), 28 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 373e029f9876..b9a3f5ae42ac 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -584,7 +584,6 @@ mutual
         match evalSyntaxConstant env opts tacticDecl with
         | Except.error err       => throwError err
         | 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
@@ -596,7 +595,8 @@ mutual
           -/
           let info := (← getRef).getHeadInfo
           let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
-          let argNew := Arg.stx tacticBlock
+          let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName)
+          let argNew := Arg.expr mvar
           propagateExpectedType argNew
           elabAndAddNewArg argName argNew
           main
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index d33a54bb40c6..38fd868b00a7 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -150,26 +150,10 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
     elabTerm b expectedType?
   | _ => throwUnsupportedSyntax
 
-private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
-  let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
-  let mvarId := mvar.mvarId!
-  let ref ← getRef
-  registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
-  return mvar
-
-register_builtin_option debug.byAsSorry : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
-}
-
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
   | some expectedType =>
-    if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
-      mkSorry expectedType false
-    else
-      mkTacticMVar expectedType stx
+    mkTacticMVar expectedType stx .term
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 220d7b8e910b..10bcf28ac36a 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -682,7 +682,9 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
               -- 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
+              let type := (d.getArg! 0).consumeTypeAnnotations
+              let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName)
+              cont mvar field
           | _ =>
             if bi == .instImplicit then
               let val ← withRef field.ref <| mkFreshExprMVar d .synthetic
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index a5378133af97..239c8074e335 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -316,6 +316,18 @@ def PostponeBehavior.ofBool : Bool → PostponeBehavior
   | true  => .yes
   | false => .no
 
+private def TacticMVarKind.logError (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Unit := do
+  match kind with
+  | term => pure ()
+  | autoParam arg => logErrorAt tacticCode m!"could not synthesize default value for parameter '{arg}' using tactics"
+  | fieldAutoParam field => logErrorAt tacticCode m!"could not synthesize default value for field '{field}' using tactics"
+
+private def TacticMVarKind.maybeWithoutRecovery (kind : TacticMVarKind) (m : TacticM α) : TacticM α := do
+  if kind matches .autoParam _ | .fieldAutoParam _ then
+    withoutErrToSorry <| Tactic.withoutRecover <| m
+  else
+    m
+
 mutual
 
   /--
@@ -325,7 +337,7 @@ mutual
 
   If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
   -/
-  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
+  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
     instantiateMVarDeclMVars mvarId
     /-
     TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type.
@@ -342,7 +354,7 @@ mutual
     in more complicated scenarios.
     -/
     tryCatchRuntimeEx
-      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
+      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId <| kind.maybeWithoutRecovery do
             withTacticInfoContext tacticCode do
               -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
               -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
@@ -354,10 +366,13 @@ mutual
               synthesizeSyntheticMVars (postpone := .no)
           unless remainingGoals.isEmpty do
             if report then
+              kind.logError tacticCode
               reportUnsolvedGoals remainingGoals
             else
               throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
       fun ex => do
+        if report then
+          kind.logError tacticCode
         if report && (← read).errToSorry then
           for mvarId in (← getMVars (mkMVar mvarId)) do
             mvarId.admit
@@ -385,10 +400,10 @@ mutual
       return false
     -- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
     | .postponed savedContext => resumePostponed savedContext mvarSyntheticDecl.stx mvarId postponeOnError
-    | .tactic tacticCode savedContext =>
+    | .tactic tacticCode savedContext kind =>
       withSavedContext savedContext do
         if runTactics then
-          runTactic mvarId tacticCode
+          runTactic mvarId tacticCode (kind := kind)
           return true
         else
           return false
@@ -529,9 +544,9 @@ the result of a tactic block.
 def runPendingTacticsAt (e : Expr) : TermElabM Unit := do
   for mvarId in (← getMVars e) do
     let mvarId ← getDelayedMVarRoot mvarId
-    if let some { kind := .tactic tacticCode savedContext, .. } ← getSyntheticMVarDecl? mvarId then
+    if let some { kind := .tactic tacticCode savedContext kind, .. } ← getSyntheticMVarDecl? mvarId then
       withSavedContext savedContext do
-        runTactic mvarId tacticCode
+        runTactic mvarId tacticCode kind
         markAsResolved mvarId
 
 builtin_initialize
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 2ac90f893557..eca414db661b 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -47,7 +47,7 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp
         -/
         withoutModifyingStateWithInfoAndMessages do
           Term.withSynthesize (postpone := .no) do
-            Term.runTactic (report := false) mvar.mvarId! tacticCode
+            Term.runTactic (report := false) mvar.mvarId! tacticCode .term
           let result ← instantiateMVars mvar
           if result.hasExprMVar then
             return none
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index d04bab834284..4d47c997eab0 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -29,6 +29,15 @@ structure SavedContext where
   errToSorry : Bool
   levelNames : List Name
 
+/-- The kind of a tactic metavariable, used for additional error reporting. -/
+inductive TacticMVarKind
+  /-- Standard tactic metavariable, arising from `by ...` syntax. -/
+  | term
+  /-- Tactic metavariable arising from an autoparam for a function application. -/
+  | autoParam (arg : Name)
+  /-- Tactic metavariable arising from an autoparam for a structure field. -/
+  | fieldAutoParam (field : Name)
+
 /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
 inductive SyntheticMVarKind where
   /--
@@ -43,7 +52,7 @@ inductive SyntheticMVarKind where
   Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/
   | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
   /-- Use tactic to synthesize value for metavariable. -/
-  | tactic (tacticCode : Syntax) (ctx : SavedContext)
+  | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
   /-- Metavariable represents a hole whose elaboration has been postponed. -/
   | postponed (ctx : SavedContext)
   deriving Inhabited
@@ -1191,6 +1200,26 @@ private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) :
 def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
   return (← get).syntheticMVars.find? mvarId
 
+register_builtin_option debug.byAsSorry : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
+}
+
+/--
+Creates a new metavariable of type `type` that will be synthesized using the tactic code.
+The `tacticCode` syntax is the full `by ..` syntax.
+-/
+def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Expr := do
+  if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then
+    mkSorry type false
+  else
+    let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
+    let mvarId := mvar.mvarId!
+    let ref ← getRef
+    registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext) kind
+    return mvar
+
 /--
   Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable.
   See `mkTermInfo`.
diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out
index bea102118361..d7d617d9f0fe 100644
--- a/tests/lean/interactive/4880.lean.expected.out
+++ b/tests/lean/interactive/4880.lean.expected.out
@@ -2,6 +2,15 @@
  "uri": "file:///4880.lean",
  "diagnostics":
  [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 16, "character": 12},
+    "end": {"line": 16, "character": 17}},
+   "message": "could not synthesize default value for field 'h1' using tactics",
+   "fullRange":
+   {"start": {"line": 16, "character": 12},
+    "end": {"line": 16, "character": 17}}},
+  {"source": "Lean 4",
    "severity": 1,
    "range":
    {"start": {"line": 16, "character": 12},
@@ -11,6 +20,16 @@
    "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":
+   "could not synthesize default value for parameter '_h1' using tactics",
+   "fullRange":
+   {"start": {"line": 22, "character": 17},
+    "end": {"line": 22, "character": 20}}},
   {"source": "Lean 4",
    "severity": 1,
    "range":
diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean
index 31fda18ba31c..34156eaf56ca 100644
--- a/tests/lean/run/autoparam.lean
+++ b/tests/lean/run/autoparam.lean
@@ -1,3 +1,6 @@
+/-!
+# Testing the autoparam feature
+-/
 
 def f (x y : Nat) (h : x = y := by assumption) : Nat :=
 x + x
@@ -13,3 +16,33 @@ x + x
 
 #check fun x => f2 x x
 #check fun x => f3 x x
+
+/--
+error: could not synthesize default value for parameter 'h' using tactics
+---
+error: tactic 'assumption' failed
+⊢ 1 = 2
+-/
+#guard_msgs in example := f 1 2
+
+/-!
+From #2950, field autoparam should mention which field failed.
+-/
+
+structure Foo where
+  val : String
+  len : Nat := val.length
+  inv : val.length = len := by next => decide
+
+/--
+error: could not synthesize default value for field 'inv' using tactics
+---
+error: tactic 'decide' proved that the proposition
+  "abc".length = 5
+is false
+-/
+#guard_msgs in
+def test2 : Foo := {
+  val := "abc"
+  len := 5
+}
diff --git a/tests/lean/run/mergeSort.lean b/tests/lean/run/mergeSort.lean
index 954bfa156ae1..2215f56327cc 100644
--- a/tests/lean/run/mergeSort.lean
+++ b/tests/lean/run/mergeSort.lean
@@ -37,6 +37,8 @@ inductive NoLE
 | mk : NoLE
 
 /--
+error: could not synthesize default value for parameter 'le' using tactics
+---
 error: failed to synthesize
   LE NoLE
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
@@ -51,6 +53,8 @@ instance : LE UndecidableLE where
   le := fun _ _ => true
 
 /--
+error: could not synthesize default value for parameter 'le' using tactics
+---
 error: type mismatch
   a ≤ b
 has type

From 01fe6c9c249d7673201b8a1b1f1b5dadb631ba06 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 25 Sep 2024 13:07:11 -0700
Subject: [PATCH 2/5] named arg -> arg

---
 src/Lean/Elab/SyntheticMVars.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 239c8074e335..b238a0290896 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -403,7 +403,7 @@ mutual
     | .tactic tacticCode savedContext kind =>
       withSavedContext savedContext do
         if runTactics then
-          runTactic mvarId tacticCode (kind := kind)
+          runTactic mvarId tacticCode kind
           return true
         else
           return false

From 0920e6ff3693d91132e89dcfcf5968551ad462ea Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 25 Sep 2024 13:13:55 -0700
Subject: [PATCH 3/5] mention structure name in error

---
 src/Lean/Elab/StructInst.lean                 | 2 +-
 src/Lean/Elab/SyntheticMVars.lean             | 6 +++---
 src/Lean/Elab/Term.lean                       | 4 ++--
 tests/lean/interactive/4880.lean.expected.out | 3 ++-
 tests/lean/run/autoparam.lean                 | 2 +-
 5 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 10bcf28ac36a..bb5ba522d8fb 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -683,7 +683,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
               let info := field.ref.getHeadInfo
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
               let type := (d.getArg! 0).consumeTypeAnnotations
-              let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName)
+              let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)
               cont mvar field
           | _ =>
             if bi == .instImplicit then
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index b238a0290896..3e5e25223c75 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -319,11 +319,11 @@ def PostponeBehavior.ofBool : Bool → PostponeBehavior
 private def TacticMVarKind.logError (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Unit := do
   match kind with
   | term => pure ()
-  | autoParam arg => logErrorAt tacticCode m!"could not synthesize default value for parameter '{arg}' using tactics"
-  | fieldAutoParam field => logErrorAt tacticCode m!"could not synthesize default value for field '{field}' using tactics"
+  | autoParam argName => logErrorAt tacticCode m!"could not synthesize default value for parameter '{argName}' using tactics"
+  | fieldAutoParam fieldName structName => logErrorAt tacticCode m!"could not synthesize default value for field '{fieldName}' of '{structName}' using tactics"
 
 private def TacticMVarKind.maybeWithoutRecovery (kind : TacticMVarKind) (m : TacticM α) : TacticM α := do
-  if kind matches .autoParam _ | .fieldAutoParam _ then
+  if kind matches .autoParam .. | .fieldAutoParam .. then
     withoutErrToSorry <| Tactic.withoutRecover <| m
   else
     m
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 4d47c997eab0..78593be5d0c6 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -34,9 +34,9 @@ inductive TacticMVarKind
   /-- Standard tactic metavariable, arising from `by ...` syntax. -/
   | term
   /-- Tactic metavariable arising from an autoparam for a function application. -/
-  | autoParam (arg : Name)
+  | autoParam (argName : Name)
   /-- Tactic metavariable arising from an autoparam for a structure field. -/
-  | fieldAutoParam (field : Name)
+  | fieldAutoParam (fieldName structName : Name)
 
 /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
 inductive SyntheticMVarKind where
diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out
index d7d617d9f0fe..88d320c447ec 100644
--- a/tests/lean/interactive/4880.lean.expected.out
+++ b/tests/lean/interactive/4880.lean.expected.out
@@ -6,7 +6,8 @@
    "range":
    {"start": {"line": 16, "character": 12},
     "end": {"line": 16, "character": 17}},
-   "message": "could not synthesize default value for field 'h1' using tactics",
+   "message":
+   "could not synthesize default value for field 'h1' of 'B' using tactics",
    "fullRange":
    {"start": {"line": 16, "character": 12},
     "end": {"line": 16, "character": 17}}},
diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean
index 34156eaf56ca..7dd13506a9af 100644
--- a/tests/lean/run/autoparam.lean
+++ b/tests/lean/run/autoparam.lean
@@ -35,7 +35,7 @@ structure Foo where
   inv : val.length = len := by next => decide
 
 /--
-error: could not synthesize default value for field 'inv' using tactics
+error: could not synthesize default value for field 'inv' of 'Foo' using tactics
 ---
 error: tactic 'decide' proved that the proposition
   "abc".length = 5

From 6bae2e6ef9c5b0edd72ab930206f84135e410d29 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 25 Sep 2024 15:39:53 -0700
Subject: [PATCH 4/5] terminfo

---
 src/Lean/Elab/App.lean        | 1 +
 src/Lean/Elab/StructInst.lean | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index b9a3f5ae42ac..907daf7041e0 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -596,6 +596,7 @@ mutual
           let info := (← getRef).getHeadInfo
           let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
           let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName)
+          addTermInfo' tacticBlock mvar
           let argNew := Arg.expr mvar
           propagateExpectedType argNew
           elabAndAddNewArg argName argNew
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index bb5ba522d8fb..328032bbc6cd 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -684,6 +684,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
               let type := (d.getArg! 0).consumeTypeAnnotations
               let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)
+              addTermInfo' stx mvar
               cont mvar field
           | _ =>
             if bi == .instImplicit then

From 7fa852e335a2db7f6faa4e66f8d67a77dcc8e448 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 27 Sep 2024 11:38:56 -0700
Subject: [PATCH 5/5] comments

---
 src/Lean/Elab/App.lean        | 3 +++
 src/Lean/Elab/StructInst.lean | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 907daf7041e0..d7caaa78c365 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -596,6 +596,9 @@ mutual
           let info := (← getRef).getHeadInfo
           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`.
+          -- We should look into removing this since terminfo for synthetic syntax is suspect,
+          -- but we noted it was necessary to preserve the behavior of the unused variable linter.
           addTermInfo' tacticBlock mvar
           let argNew := Arg.expr mvar
           propagateExpectedType argNew
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 328032bbc6cd..861d04dd08d5 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -684,6 +684,8 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
               let type := (d.getArg! 0).consumeTypeAnnotations
               let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName)
+              -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.
+              -- (See the aformentioned `processExplicitArg` for a comment about this.)
               addTermInfo' stx mvar
               cont mvar field
           | _ =>