fix: disable "error to sorry" and "error recovery" at failIfSuccess

closes #1375

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -166,10 +166,11 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 @[builtinTactic unknown] def evalUnknown : Tactic := fun stx => do
   addCompletionInfo <| CompletionInfo.tactic stx (← getGoals)
 
-@[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do
-  let tactic := stx[1]
-  if (← try evalTactic tactic; pure true catch _ => pure false) then
-    throwError "tactic succeeded"
+@[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx =>
+  Term.withoutErrToSorry <| withoutRecover do
+    let tactic := stx[1]
+    if (← try evalTactic tactic; pure true catch _ => pure false) then
+      throwError "tactic succeeded"
 
 @[builtinTactic traceState] def evalTraceState : Tactic := fun _ => do
   let gs ← getUnsolvedGoals

src/Lean/Elab/Term.lean

@@ -425,12 +425,15 @@ def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr
     withReader (fun ctx => { ctx with auxDeclToFullName := ctx.auxDeclToFullName.insert x.fvarId! declName }) do
       k x
 
+def withoutErrToSorryImp (x : TermElabM α) : TermElabM α :=
+  withReader (fun ctx => { ctx with errToSorry := false }) x
+
 /--
   Execute `x` without converting errors (i.e., exceptions) to `sorry` applications.
   Recall that when `errToSorry = true`, the method `elabTerm` catches exceptions and convert them into `sorry` applications.
 -/
-def withoutErrToSorry (x : TermElabM α) : TermElabM α :=
-  withReader (fun ctx => { ctx with errToSorry := false }) x
+def withoutErrToSorry [MonadFunctorT TermElabM m] : m α → m α :=
+  monadMap (m := TermElabM) withoutErrToSorryImp
 
 /-- For testing `TermElabM` methods. The #eval command will sign the error. -/
 def throwErrorIfErrors : TermElabM Unit := do

tests/lean/run/1375.lean

@@ -0,0 +1,9 @@
+example : True := by
+  fail_if_success (have : False := by assumption)
+  trivial
+
+example : True := by
+  have : False := by
+    fail_if_success assumption
+    sorry
+  trivial