From 4b2fa38cb8841fb9e50bfaa2402bddf40f49295e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 15 Nov 2021 16:56:55 -0800
Subject: [PATCH] fix: `#check_failure` command should succeed if there are
 stuck TC problems

---
 src/Lean/Elab/BuiltinCommand.lean | 8 +++++---
 tests/lean/run/check_failure.lean | 2 ++
 2 files changed, 7 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/check_failure.lean

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 8be3d5563d..455920be4c 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -209,16 +209,18 @@ private def replaceBinderAnnotation (binder : Syntax) : CommandElabM Bool := do
 
 open Meta
 
-@[builtinCommandElab Lean.Parser.Command.check] def elabCheck : CommandElab
+def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv $ runTermElabM (some `_check) fun _ => do
     let e ← Term.elabTerm term none
-    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
+    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := ignoreStuckTC)
     let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
     let type ← inferType e
     unless e.isSyntheticSorry do
       logInfoAt tk m!"{e} : {type}"
   | _ => throwUnsupportedSyntax
 
+@[builtinCommandElab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true)
+
 @[builtinCommandElab Lean.Parser.Command.reduce] def elabReduce : CommandElab
   | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM (some `_check) fun _ => do
     let e ← Term.elabTerm term none
@@ -256,7 +258,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
 
 @[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab
   | `(#check_failure $term) => do
-    failIfSucceeds <| elabCheck (← `(#check $term))
+    failIfSucceeds <| elabCheckCore (ignoreStuckTC := false) (← `(#check $term))
   | _ => throwUnsupportedSyntax
 
 private def mkEvalInstCore (evalClassName : Name) (e : Expr) : MetaM Expr := do
diff --git a/tests/lean/run/check_failure.lean b/tests/lean/run/check_failure.lean
new file mode 100644
index 0000000000..c71b78ec9b
--- /dev/null
+++ b/tests/lean/run/check_failure.lean
@@ -0,0 +1,2 @@
+-- #check_failure should not ignore stuck TC problems.
+#check_failure (inferInstance : Inhabited (Nat × _))