From 1f2e92ea04d1035dee7a52e1300ade3d602635da Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Oct 2021 13:30:27 -0700
Subject: [PATCH] feat: make sure `#check` produces some result even when there
 are pending TC problems

Lean 3 uses the same approach.

closes #714
---
 src/Lean/Elab/BuiltinCommand.lean | 2 +-
 src/Lean/Elab/SyntheticMVars.lean | 4 ++--
 tests/lean/714.lean               | 3 +++
 tests/lean/714.lean.expected.out  | 1 +
 4 files changed, 7 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/714.lean
 create mode 100644 tests/lean/714.lean.expected.out

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index f97dde6992..677d362bbf 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -212,7 +212,7 @@ open Meta
 @[builtinCommandElab Lean.Parser.Command.check] def elabCheck : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv $ runTermElabM (some `_check) fun _ => do
     let e ← Term.elabTerm term none
-    Term.synthesizeSyntheticMVarsNoPostponing
+    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
     let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
     let type ← inferType e
     unless e.isSyntheticSorry do
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 95a5f24e54..6c37c15bd5 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -296,8 +296,8 @@ mutual
     loop ()
 end
 
-def synthesizeSyntheticMVarsNoPostponing : TermElabM Unit :=
-  synthesizeSyntheticMVars (mayPostpone := false)
+def synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := false) : TermElabM Unit :=
+  synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := ignoreStuckTC)
 
 /- Keep invoking `synthesizeUsingDefault` until it returns false. -/
 private partial def synthesizeUsingDefaultLoop : TermElabM Unit := do
diff --git a/tests/lean/714.lean b/tests/lean/714.lean
new file mode 100644
index 0000000000..51d035b5d0
--- /dev/null
+++ b/tests/lean/714.lean
@@ -0,0 +1,3 @@
+def test {α : Type} [LT α] := List α
+
+#check test
diff --git a/tests/lean/714.lean.expected.out b/tests/lean/714.lean.expected.out
new file mode 100644
index 0000000000..1010ce36fc
--- /dev/null
+++ b/tests/lean/714.lean.expected.out
@@ -0,0 +1 @@
+test : Type