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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.check (e : Expr) (transparency : TransparencyMode := TransparencyMode.all) : MetaM Unit

Throw an exception if e is not type correct at the given transparency.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.withInstancesTypeCheckNote {m : Type → Type u_1} {α : Type} [MonadControlT MetaM m] [Monad m] (e : Expr) (x : m α) : m α

Runs x and, on any error, lazily checks whether e is type-correct at instances transparency. If not, appends an explanatory note to the error message.

This is useful for tactics like rw and simp whose failure modes can be caused by prior tactics (such as unfold) leaving the goal in a state that's type-correct only at .default transparency, preventing unification etc at .instances.

Equations

• One or more equations did not get rendered due to their size.

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

Return true if e is type correct.

Equations

• Lean.Meta.isTypeCorrect e = tryCatch (do Lean.Meta.check e pure true) fun (x : Lean.Exception) => pure false

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. Be sure to share common expressions in e before calling this function for good performance.

Equations

• One or more equations did not get rendered due to their size.