chore: add missing diff-exposing in type/value mismatch errors

This PR addresses a few error messages where diffs aren't being exposed.

src/Lean/Elab/Calc.lean

@@ -131,14 +131,18 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
     if ← isDefEqGuarded r er then
       let mut failed := false
       unless ← isDefEqGuarded lhs elhs do
+        let (lhs, elhs) ← addPPExplicitToExposeDiff lhs elhs
+        let (lhsTy, elhsTy) ← addPPExplicitToExposeDiff (← inferType lhs) (← inferType elhs)
         logErrorAt steps[0]!.term m!"\
-          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
-          but is expected to be{indentD m!"{elhs} : {← inferType elhs}"}"
+          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {lhsTy}"}\n\
+          but is expected to be{indentD m!"{elhs} : {elhsTy}"}"
         failed := true
       unless ← isDefEqGuarded rhs erhs do
+        let (rhs, erhs) ← addPPExplicitToExposeDiff rhs erhs
+        let (rhsTy, erhsTy) ← addPPExplicitToExposeDiff (← inferType rhs) (← inferType erhs)
         logErrorAt steps.back!.term m!"\
-          invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {← inferType rhs}"}\n\
-          but is expected to be{indentD m!"{erhs} : {← inferType erhs}"}"
+          invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {rhsTy}"}\n\
+          but is expected to be{indentD m!"{erhs} : {erhsTy}"}"
         failed := true
       if failed then
         throwAbortTerm

src/Lean/Elab/CheckTactic.lean

@@ -38,6 +38,7 @@ def elabCheckTactic : CommandElab := fun stx => do
       | [next] => do
         let (val, _, _) ← matchCheckGoalType stx (←next.getType)
         if !(← Meta.withReducible <| isDefEq val expTerm) then
+          let (val, expTerm) ← addPPExplicitToExposeDiff val expTerm
           throwErrorAt stx
             m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
       | _ => do

src/Lean/Meta/Check.lean

@@ -17,14 +17,6 @@ namespace Lean.Meta
 private def ensureType (e : Expr) : MetaM Unit := do
   discard <| getLevel e
 
-def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
-  let lctx ← getLCtx
-  match lctx.find? fvarId with
-  | some (LocalDecl.ldecl _ _ _ t v _ _) => do
-    let vType ← inferType v
-    throwError "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
-  | _ => unreachable!
-
 private def checkConstant (constName : Name) (us : List Level) : MetaM Unit := do
   let cinfo ← getConstInfo constName
   unless us.length == cinfo.levelParams.length do
@@ -177,6 +169,15 @@ where
     catch _ =>
       return (a, b)
 
+def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
+  let lctx ← getLCtx
+  match lctx.find? fvarId with
+  | some (LocalDecl.ldecl _ _ _ t v _ _) => do
+    let vType ← inferType v
+    let (vType, t) ← addPPExplicitToExposeDiff vType t
+    throwError "invalid let declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
+  | _ => unreachable!
+
 /--
   Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 -/