fix: withMainContext in type_check tactic (#15533)

Fixing a problem about `type_check` tactic: If you don't use `withMainContext`, you can't use local hypotheses and definitions produced by tactics before the `type_check` tactic, only can use hypotheses written on `theorem` header.

Mathlib/Tactic/TypeCheck.lean

@@ -4,17 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
 import Lean.Elab.Tactic.Basic
+import Lean.Elab.SyntheticMVars
 
 /-!
 # The `type_check` tactic
 Define the `type_check` tactic: it type checks a given expression, and traces its type.
 -/
 
-open Lean Meta
+open Lean Elab Meta
 
 /-- Type check the given expression, and trace its type. -/
 elab tk:"type_check " e:term : tactic => do
-  let e ← Lean.Elab.Term.elabTerm e none
-  check e
-  let type ← inferType e
-  Lean.logInfoAt tk f!"{← Lean.instantiateMVars type}"
+  Tactic.withMainContext do
+    let e ← Term.elabTermAndSynthesize e none
+    check e
+    let type ← inferType e
+    Lean.logInfoAt tk m!"{← Lean.instantiateMVars type}"

test/TypeCheck.lean

@@ -17,7 +17,9 @@ info: Prop
 ---
 info: Prop
 ---
-info: Nat -> Nat
+info: Nat → Nat
+---
+info: List Nat
 -/
 #guard_msgs in
 example : True := by
@@ -28,5 +30,6 @@ example : True := by
   type_check (True : _) -- Prop
   type_check ∀ x y : Nat, x = y -- Prop
   type_check fun x : Nat => 2 * x + 1 -- Nat -> Nat
+  type_check [1]
   fail_if_success type_check wrong
   trivial