fix: isDefEq when zetaDelta := false

src/Lean/Meta/ExprDefEq.lean

@@ -1674,11 +1674,12 @@ private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
   -- | Expr.mdata _ t _,    s                   => isDefEqQuick t s
   -- | t,                   Expr.mdata _ s _    => isDefEqQuick t s
   | .fvar fvarId₁, .fvar fvarId₂ => do
-    if (← fvarId₁.isLetVar <||> fvarId₂.isLetVar) then
-      return LBool.undef
-    else if fvarId₁ == fvarId₂ then
-      return LBool.true
+    if fvarId₁ == fvarId₂ then
+      return .true
+    else if (← fvarId₁.isLetVar <||> fvarId₂.isLetVar) then
+      return .undef
     else
+      -- If `t` and `s` are not proofs or let-variables, we still return `.undef` and let other rules (e.g., unit-like) kick in.
       isDefEqProofIrrel t s
   | t, s =>
     isDefEqQuickOther t s

tests/lean/run/heapSort.lean

@@ -175,13 +175,13 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
 attribute [simp] Array.heapSort.loop
 
 /--
-info: Array.heapSort.loop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α) :
-  Array.heapSort.loop lt a out =
+info: Array.heapSort.loop.eq_1.{u_1} {α : Type u_1} (gt : α → α → Bool) (a : BinaryHeap α gt) (out : Array α) :
+  Array.heapSort.loop gt a out =
     match e : a.max with
     | none => out
     | some x =>
       let_fun this := ⋯;
-      Array.heapSort.loop lt a.popMax (out.push x)
+      Array.heapSort.loop gt a.popMax (out.push x)
 -/
 #guard_msgs in
 #check Array.heapSort.loop.eq_1

tests/lean/run/zetaDeltaFalseDefEqIssue.lean

@@ -0,0 +1,14 @@
+import Lean
+
+/--
+info: true
+true
+-/
+#guard_msgs in
+open Lean Meta in
+run_meta do
+  withLetDecl `x (mkConst ``Nat) (mkNatLit 10) fun x => do
+    IO.println (← isDefEq x x)
+    withConfig (fun c => { c with zeta := false, zetaDelta := false }) do
+      IO.println (← isDefEq x x) -- Should return `true` even if `zetaDelta := false`
+      return ()