feat: consider universes and projections in addPPExplicitToExposeDiff (#8271)

This PR changes `addPPExplicitToExposeDiff` to show universe differences
and to visit into projections, e.g.:
```
error: tactic 'rfl' failed, the left-hand side
  (Test.mk (∀ (x : PUnit.{1}), True)).1
is not definitionally equal to the right-hand side
  (Test.mk (∀ (x : PUnit.{2}), True)).1
```
for
```lean
inductive Test where
  | mk (x : Prop)

example : (Test.mk (∀ _ : PUnit.{1}, True)).1 = (Test.mk (∀ _ : PUnit.{2}, True)).1 := by
  rfl
```

src/Lean/Meta/Check.lean

@@ -84,6 +84,17 @@ where
       | _, .mdata _ b' =>
         let (a, b') ← visit a b'
         return (a, b.updateMData! b')
+      | .const nm _, .const nm' _ =>
+        if nm != nm' then
+          return (a, b)
+        else
+          return (a.setPPUniverses true, b.setPPUniverses true)
+      | .proj _ i a', .proj _ j b' =>
+        if i != j then
+          return (a, b)
+        else
+          let (a', b') ← visit a' b'
+          return (a.updateProj! a', b.updateProj! b')
       | .app .., .app .. =>
         if a.getAppNumArgs != b.getAppNumArgs then
           return (a, b)

tests/lean/issue3232.lean

@@ -8,4 +8,4 @@ example : (1 : Nat) = 1 := by
   apply (rfl : (1 : Int) = 1)
 
 example : PUnit.{0} = PUnit.{0} := by
-  apply Eq.refl PUnit.{1} -- TODO: addPPExplicitToExposeDiff is not handling this yet
+  apply Eq.refl PUnit.{1}

tests/lean/issue3232.lean.expected.out

@@ -10,7 +10,7 @@ with the goal
   (1 : Nat) = 1
 ⊢ 1 = 1
 issue3232.lean:11:2-11:25: error: tactic 'apply' failed, could not unify the type of `Eq.refl PUnit`
-  PUnit = PUnit
+  Eq.{2} PUnit PUnit
 with the goal
-  PUnit = PUnit
+  Eq.{1} PUnit PUnit
 ⊢ PUnit = PUnit

tests/lean/run/exposeDiff.lean

@@ -0,0 +1,48 @@
+/--
+error: tactic 'apply' failed, could not unify the type of `x`
+  PUnit.{1}
+with the goal
+  PUnit.{0}
+x : PUnit
+⊢ PUnit
+-/
+#guard_msgs in
+example (x : PUnit.{1}) : PUnit.{0} := by
+  apply x
+
+/--
+error: type mismatch
+  x
+has type
+  PUnit.{1} : Type
+but is expected to have type
+  PUnit.{0} : Prop
+-/
+#guard_msgs in
+example (x : PUnit.{1}) : PUnit.{0} :=
+  x
+
+/--
+error: tactic 'rfl' failed, the left-hand side
+  ∀ (x : PUnit.{1}), True
+is not definitionally equal to the right-hand side
+  ∀ (x : PUnit.{2}), True
+⊢ (∀ (x : PUnit), True) ↔ ∀ (x : PUnit), True
+-/
+#guard_msgs in
+example : (∀ _ : PUnit.{1}, True) ↔ ∀ _ : PUnit.{2}, True := by
+  rfl
+
+inductive Test where
+  | mk (x : Prop)
+
+/--
+error: tactic 'rfl' failed, the left-hand side
+  (Test.mk (∀ (x : PUnit.{1}), True)).1
+is not definitionally equal to the right-hand side
+  (Test.mk (∀ (x : PUnit.{2}), True)).1
+⊢ (Test.mk (∀ (x : PUnit), True)).1 = (Test.mk (∀ (x : PUnit), True)).1
+-/
+#guard_msgs in
+example : (Test.mk (∀ _ : PUnit.{1}, True)).1 = (Test.mk (∀ _ : PUnit.{2}, True)).1 := by
+  rfl