Profiler reports incorrect time of type checking

Description

It seems that Lean does not correctly report type checking times. I'm not a 100% sure about this, so I'm making this issue partly to confirm. What I think happens:

1. "type checking" is measured with a time_task here. It's a RAII-style thing that prints out its measured timespan in the destructor. The variable is not passed anywhere, so the destruction happens right after return.
2. This means that the only measured statement is ::lean::check, defined here.
3. The immediately argument to check is always false (see type_checker.h and all uses of check), so the call to check_definition, which is what actually checks the type is deferred to happen in an asynchronous task-closure. The closure runs sometime after lean::check, which returns immediately.
4. Hence, the time measured by the time_task is merely the time to build the closure, potentially orders of magnitude less than type checking really takes.

Reproducing

1. Create profile.lean with contents:

import tactic.interactive tactic.ring tactic.ring2

constants (α : Type) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 : α)

theorem profile_me [comm_ring α]
  : ((((((((x15*x0)*x3)+x2)+x6)*(15: α))*x5)+x5)*(0: α))
  = ((0: α)*(1*((x5*1)+(x5*(1*((0+(15: α))*((x6*1)+(0+(x2+(1*(x3*((0+x0)*(x15*1)))))))))))))
:= by ring

2. Run lean -j1 --profile profile.lean in a debugger and inspect the control flow. Or put a print statement in the checked_proof closure and see that it prints long after "type checking of profile_me took ..".

Versions

Any recent one.

Start in src/frontends/lean/definition_cmds.cpp at the time_task around type checking, then trace check in src/kernel/type_checker.cpp and its declarations and uses in type_checker.h. Reproduce with profile.lean using lean -j1 --profile and compare the reported time with the checked_proof closure's execution. Done means the profiler's type-checking duration covers the actual deferred checking work.