fix: isDefEq for constants with different universe parameters

This PR fixes a bug at the definitional equality test (`isDefEq`). At
unification constraints of the form `c.{u} =?= c.{v}`, it was not
trying to unfold `c`. This bug did not affect the kernel.

closes #6117

src/Lean/Meta/ExprDefEq.lean

@@ -1387,15 +1387,21 @@ private abbrev unfold (e : Expr) (failK : MetaM α) (successK : Expr → MetaM
 /-- Auxiliary method for isDefEqDelta -/
 private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
   match t, s with
-  | Expr.const _ ls₁, Expr.const _ ls₂ => isListLevelDefEq ls₁ ls₂
-  | Expr.app _ _,     Expr.app _ _     =>
+  | .const _ ls₁, .const _ ls₂ =>
+    match (← isListLevelDefEq ls₁ ls₂) with
+    | .true => return .true
+    | _ =>
+    unfold t (pure .undef) fun t =>
+    unfold s (pure .undef) fun s =>
+      isDefEqLeftRight fn t s
+  | .app _ _,     .app _ _     =>
     if (← tryHeuristic t s) then
-      pure LBool.true
+      return .true
     else
       unfold t
-       (unfold s (pure LBool.undef) (fun s => isDefEqRight fn t s))
+       (unfold s (pure .undef) fun s => isDefEqRight fn t s)
        (fun t => unfold s (isDefEqLeft fn t s) (fun s => isDefEqLeftRight fn t s))
-  | _, _ => pure LBool.false
+  | _, _ => return .false
 
 private def sameHeadSymbol (t s : Expr) : Bool :=
   match t.getAppFn, s.getAppFn with

tests/lean/run/6117.lean

@@ -0,0 +1,30 @@
+import Lean
+
+abbrev T.{u} : Unit := (fun (α : Sort u) => ()) PUnit.{u}
+
+set_option pp.universes true
+
+def unitUnique (x y : Unit) : x = y := by rfl
+
+def testUnique.{u, v} : T.{u} = T.{v} := unitUnique _ _
+
+def test.{u, v} : T.{u} = T.{v} := rfl
+
+def test'.{u, v} : T.{u} = T.{v} := rfl (a := ())
+
+theorem test''.{u, v} : T.{u} = T.{v} := by
+  unfold T
+  rfl
+
+-- Use kernel defeq
+def test'''.{u, v} : T.{u} = T.{v} :=  by
+  run_tac do
+    Lean.Elab.Tactic.closeMainGoalUsing `test''' fun t _ =>
+      Lean.Meta.mkEqRefl t.eq?.get!.2.1
+
+/--
+info: def test'''.{u, v} : Eq.{1} T.{u} T.{v} :=
+Eq.refl.{1} T.{u}
+-/
+#guard_msgs in
+#print test'''