feat: have autoparams report parameter/field on failure (#5474)

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

Examples:
```text
could not synthesize default value for parameter 'h' using tactics

could not synthesize default value for field 'inv' of 'S' using tactics
```

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. This is justified on the grounds that
autoparams are not interactive.
* Autoparams for applications now cleanup the autoParam annotation,
bringing it in line with autoparams for structure fields.
* This preserves the old behavior that autoparams leave terminfo, but we
will revisit this after some imminent improvements to the unused
variable linter.

Closes #2950

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,12 @@ 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)
+          -- 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
           elabAndAddNewArg argName argNew
           main

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")

src/Lean/Elab/StructInst.lean

@@ -682,7 +682,12 @@ 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 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
           | _ =>
             if bi == .instImplicit then
               let val ← withRef field.ref <| mkFreshExprMVar d .synthetic

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 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
+    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
           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

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

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 (argName : Name)
+  /-- Tactic metavariable arising from an autoparam for a structure field. -/
+  | fieldAutoParam (fieldName structName : 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`.

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

@@ -2,6 +2,16 @@
  "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' of 'B' 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 +21,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":

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' of 'Foo' using tactics
+---
+error: tactic 'decide' proved that the proposition
+  "abc".length = 5
+is false
+-/
+#guard_msgs in
+def test2 : Foo := {
+  val := "abc"
+  len := 5
+}

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