fix: simp fails when custom discharger makes no progress (leanprove…

…r#3317)

closes leanprover#2634

src/Lean/Elab/SyntheticMVars.lean

@@ -293,8 +293,10 @@ mutual
   Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`.
 
   The `tacticCode` syntax comprises the whole `by ...` expression.
+
+  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) : TermElabM Unit := withoutAutoBoundImplicit do
+  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
     let code := tacticCode[1]
     instantiateMVarDeclMVars mvarId
     /-
@@ -320,9 +322,12 @@ mutual
             evalTactic code
         synthesizeSyntheticMVars (mayPostpone := false)
       unless remainingGoals.isEmpty do
-        reportUnsolvedGoals remainingGoals
+        if report then
+          reportUnsolvedGoals remainingGoals
+        else
+          throwError "unsolved goals\n{goalsToMessageData remainingGoals}"
     catch ex =>
-      if (← read).errToSorry then
+      if report && (← read).errToSorry then
         for mvarId in (← getMVars (mkMVar mvarId)) do
           mvarId.admit
         logException ex

src/Lean/Elab/Tactic/Simp.lean

@@ -43,9 +43,11 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp
     let runTac? : TermElabM (Option Expr) :=
       try
         /- We must only save messages and info tree changes. Recall that `simp` uses temporary metavariables (`withNewMCtxDepth`).
-           So, we must not save references to them at `Term.State`. -/
+           So, we must not save references to them at `Term.State`.
+        -/
         withoutModifyingStateWithInfoAndMessages do
-          Term.withSynthesize (mayPostpone := false) <| Term.runTactic mvar.mvarId! tacticCode
+          Term.withSynthesize (mayPostpone := false) do
+            Term.runTactic (report := false) mvar.mvarId! tacticCode
           let result ← instantiateMVars mvar
           if result.hasExprMVar then
             return none

tests/lean/2634.lean

@@ -0,0 +1,17 @@
+example
+  {p: Prop}
+  (h: True → p)
+  : p := by
+  simp (discharger := skip) [h] -- simp made no progress
+
+example
+  {p: Prop}
+  (h: True → p)
+  : p := by
+  simp (discharger := simp) [h]
+
+example
+  {p: Prop}
+  (h: True → p)
+  : p := by
+  simp (discharger := trace "hello"; simp) [h]

tests/lean/2634.lean.expected.out

@@ -0,0 +1,2 @@
+2634.lean:5:2-5:31: error: simp made no progress
+hello