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

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

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

tests/lean/714.lean

@@ -0,0 +1,3 @@
+def test {α : Type} [LT α] := List α
+
+#check test

tests/lean/714.lean.expected.out

@@ -0,0 +1 @@
+test : Type