feat: make "type mismatch" error add numeric type ascriptions (#5919)

Example:
```lean
example : 0 = (0 : Nat) := by
  exact Eq.refl (0 : Int)
/-
error: type mismatch
  Eq.refl 0
has type
  (0 : Int) = 0 : Prop
but is expected to have type
  (0 : Nat) = 0 : Prop
-/
```

src/Lean/Expr.lean

@@ -1836,6 +1836,13 @@ The delaborator uses `pp` options.
 def setPPUniverses (e : Expr) (flag : Bool) :=
   e.setOption `pp.universes flag
 
+/--
+Annotate `e` with `pp.explicit := flag`
+The delaborator uses `pp` options.
+-/
+def setPPNumericTypes (e : Expr) (flag : Bool) :=
+  e.setOption `pp.numericTypes flag
+
 /--
 If `e` is an application `f a_1 ... a_n` annotate `f`, `a_1` ... `a_n` with `pp.explicit := false`,
 and annotate `e` with `pp.explicit := true`.

src/Lean/Meta/Check.lean

@@ -123,6 +123,15 @@ where
                 firstExplicitDiff? := firstExplicitDiff? <|> some i
               else
                 firstImplicitDiff? := firstImplicitDiff? <|> some i
+          -- Some special cases
+          let fn? : Option Name :=
+            match a.getAppFn, b.getAppFn with
+            | .const ca .., .const cb .. => if ca == cb then ca else none
+            | _, _ => none
+          if fn? == ``OfNat.ofNat && as.size ≥ 3 && firstImplicitDiff? == some 0 then
+            -- Even if there is an explicit diff, it is better to see that the type is different.
+            return (a.setPPNumericTypes true, b.setPPNumericTypes true)
+          -- General case
           if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
             let (ai, bi) ← visit as[i]! bs[i]!
             as := as.set! i ai

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1021,8 +1021,10 @@ Delaborates an `OfNat.ofNat` literal.
 `@OfNat.ofNat _ n _` ~> `n`.
 -/
 @[builtin_delab app.OfNat.ofNat]
-def delabOfNat : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 3 do
-  delabOfNatCore (showType := (← getPPOption getPPNumericTypes))
+def delabOfNat : Delab := do
+  let showType ← getPPOption getPPNumericTypes
+  whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 3 do
+    delabOfNatCore (showType := ← pure showType <||> getPPOption getPPNumericTypes)
 
 /--
 Delaborates the negative of an `OfNat.ofNat` literal.

tests/lean/issue3232.lean.expected.out

@@ -5,9 +5,9 @@ with
 h : foo
 ⊢ foo
 issue3232.lean:8:2-8:29: error: tactic 'apply' failed, failed to unify
-  @OfNat.ofNat Int 1 instOfNat = 1
+  (1 : Int) = 1
 with
-  @OfNat.ofNat Nat 1 (instOfNatNat 1) = 1
+  (1 : Nat) = 1
 ⊢ 1 = 1
 issue3232.lean:11:2-11:25: error: tactic 'apply' failed, failed to unify
   PUnit = PUnit

tests/lean/run/addPPExplicitToExposeDiff.lean

@@ -63,3 +63,45 @@ but is expected to have type
 #guard_msgs in
 example : @f 1 2 := by
   exact (sorry : @f 0 _)
+
+/-!
+Add type ascriptions for numerals if they have different types.
+-/
+/--
+error: type mismatch
+  Eq.refl 0
+has type
+  (0 : Int) = 0 : Prop
+but is expected to have type
+  (0 : Nat) = 0 : Prop
+-/
+#guard_msgs in example : 0 = (0 : Nat) := by
+  exact Eq.refl (0 : Int)
+
+-- Even if the numerals are different.
+/--
+error: type mismatch
+  Eq.refl 1
+has type
+  (1 : Int) = 1 : Prop
+but is expected to have type
+  (0 : Nat) = 0 : Prop
+-/
+#guard_msgs in example : 0 = (0 : Nat) := by
+  exact Eq.refl (1 : Int)
+
+-- Even for numerals that are functions
+section
+local instance {α : Type _} [OfNat β n] : OfNat (α → β) n where
+  ofNat := fun _ => OfNat.ofNat n
+/--
+error: type mismatch
+  Eq.refl (0 1)
+has type
+  (0 : Nat → Int) 1 = 0 1 : Prop
+but is expected to have type
+  (0 : Nat → Nat) 1 = 0 1 : Prop
+-/
+#guard_msgs in example : (0 : Nat → Nat) 1 = (0 : Nat → Nat) 1 := by
+  exact Eq.refl ((0 : Nat → Int) 1)
+end