feat: expose Kernel.check for debugging purposes (#5412)

along `Kernel.isDefEq` and `Kernel.whnf`.

src/Lean/Environment.lean

@@ -1096,6 +1096,13 @@ def isDefEqGuarded (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool
 @[extern "lean_kernel_whnf"]
 opaque whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
 
+/--
+  Kernel typecheck function. We use it mainly for debugging purposes.
+  Recall that the Kernel type checker does not support metavariables.
+  When implementing automation, consider using the `MetaM` methods. -/
+@[extern "lean_kernel_check"]
+opaque check (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
+
 end Kernel
 
 class MonadEnv (m : Type → Type) where

src/kernel/type_checker.cpp

@@ -1203,6 +1203,12 @@ extern "C" LEAN_EXPORT lean_object * lean_kernel_whnf(lean_object * env, lean_ob
     });
 }
 
+extern "C" LEAN_EXPORT lean_object * lean_kernel_check(lean_object * env, lean_object * lctx, lean_object * a) {
+    return catch_kernel_exceptions<object*>([&]() {
+        return type_checker(environment(env), local_ctx(lctx)).check(expr(a)).steal();
+    });
+}
+
 inline static expr * new_persistent_expr_const(name const & n) {
     expr * e = new expr(mk_const(n));
     mark_persistent(e->raw());

tests/lean/run/kernel2.lean

@@ -15,6 +15,12 @@ def whnf (a : Name) : CoreM Unit := do
   let r ← ofExceptKernelException (Kernel.whnf env {} a)
   IO.println (toString a ++ " ==> " ++ toString r)
 
+def check (a : Name) : CoreM Unit := do
+  let env ← getEnv
+  let a := mkConst a
+  let r ← ofExceptKernelException (Kernel.check env {} a)
+  IO.println (toString a ++ " ==> " ++ toString r)
+
 partial def fact : Nat → Nat
 | 0     => 1
 | (n+1) => (n+1)*fact n
@@ -93,3 +99,7 @@ def c12 : Nat := 'a'.toNat
 /-- info: c12 ==> 97 -/
 #guard_msgs in
 #eval whnf `c12
+
+/-- info: c11 ==> Bool -/
+#guard_msgs in
+#eval check `c11