diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 06e6a5d48e..f8a0cad4bd 100644
--- a/src/Lean/Meta/Check.lean
+++ b/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)
diff --git a/tests/lean/issue3232.lean b/tests/lean/issue3232.lean
index 5f2201b7b0..5f1f7e11e3 100644
--- a/tests/lean/issue3232.lean
+++ 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}
diff --git a/tests/lean/issue3232.lean.expected.out b/tests/lean/issue3232.lean.expected.out
index 52c52b58a2..f2a26a00f6 100644
--- a/tests/lean/issue3232.lean.expected.out
+++ b/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
diff --git a/tests/lean/run/exposeDiff.lean b/tests/lean/run/exposeDiff.lean
new file mode 100644
index 0000000000..0444168aba
--- /dev/null
+++ b/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