This is not the Kernel type checker, but an auxiliary method for checking whether terms produced by tactics and isDefEq are type correct.

def Lean.Meta.addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr)

Given two expressions a and b, this method tries to annotate terms with pp.explicit := true and other pp options to expose "implicit" differences. For example, suppose a and b are of the form

@HashMap Nat Nat eqInst hasInst1
@HashMap Nat Nat eqInst hasInst2

By default, the pretty printer formats both of them as HashMap Nat Nat. So, counterintuitive error messages such as

error: application type mismatch
  HashMap.insert m
argument
  m
has type
  HashMap Nat Nat
but is expected to have type
  HashMap Nat Nat

would be produced. By adding pp.explicit := true, we can generate the more informative error

error: application type mismatch
  HashMap.insert m
argument
  m
has type
  @HashMap Nat Nat eqInst hasInst1
but is expected to have type
  @HashMap Nat Nat eqInst hasInst2

Remark: this method implements simple heuristics; we should extend it as we find other counterintuitive error messages.

def Lean.Meta.throwLetTypeMismatchMessage {α : Type} (fvarId : FVarId) : MetaM α

def Lean.Meta.mkUnfoldAxiomsNote (givenType expectedType : Expr) : MetaM MessageData

Adds note about definitions not unfolded because of the module system, if any.

def Lean.Meta.mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) (trailing? : Option MessageData := none) (trailingExprs : Array Expr := #[]) : MetaM MessageData

Return error message "has type{givenType}\nbut is expected to have type{expectedType}" Adds the type’s types unless they are defeq.

If trailing? is non-none, it is appended to the end of the message. This requires modifying the produced message, so prefer specifying trailing? over appending a message to the result of this function. Any expressions appearing in the trailing message should be included in trailingExprs.

def Lean.Meta.throwAppTypeMismatch {α : Type} (f a : Expr) : MetaM α

def Lean.Meta.checkApp (f a : Expr) : MetaM Unit

def Lean.Meta.checkProj (structName : Name) (idx : Nat) (e : Expr) : MetaM Unit

def Lean.Meta.check (e : Expr) : MetaM Unit

Throw an exception if e is not type correct.

def Lean.Meta.isTypeCorrect (e : Expr) : MetaM Bool

Return true if e is type correct.

def Lean.Meta.checkWithKernel (e : Expr) : MetaM Unit

Throw an exception if e cannot be type checked using the kernel. This function is used for debugging purposes only.