diff --git a/Mathlib/Tactic/TypeCheck.lean b/Mathlib/Tactic/TypeCheck.lean
index 63fbf103f96584..b72e3f2079b0fe 100644
--- a/Mathlib/Tactic/TypeCheck.lean
+++ b/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}"
diff --git a/test/TypeCheck.lean b/test/TypeCheck.lean
index a5498d874644f7..c707c493a6bd87 100644
--- a/test/TypeCheck.lean
+++ b/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