throw better error messages when typecheck fails at elaboration

[FrederickPu]

In lean lsp when you try #check (1 + 1 : True) you get the following error message:

Type mismatch
  1 + 1
has type
  Nat
of sort `outParam Type` but is expected to have type
  True
of sort `Prop`

However, when running kernel check you 1 + 1 get elaborated into a metavariable. And you don't get a meaningful error message.

This is not a soundness issue, but would be helpful for users understanding why the kernel check failed.