From d288619d06fec5a26ce660cf4ba106e26d8e9432 Mon Sep 17 00:00:00 2001
From: Salkutsan Aleksey <48477233+kernelpanic888@users.noreply.github.com>
Date: Sat, 25 Jul 2026 16:35:36 +0200
Subject: [PATCH 1/4] fix: recognize opaque constants of unit-like types

---
 src/Lean/Meta/ExprDefEq.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index c5cc39145b4c..1a8288f4cdd7 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -2222,7 +2222,7 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
     if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
       return true
     if t.isConst && s.isConst then
-      if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
+      if  then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
     else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
       return true
     else

From 71e4ada9dc231c5e2191ad6ef85e0829ca819d8d Mon Sep 17 00:00:00 2001
From: Salkutsan Aleksey <48477233+kernelpanic888@users.noreply.github.com>
Date: Sat, 25 Jul 2026 16:35:54 +0200
Subject: [PATCH 2/4] test: cover opaque unit-like constant equality

---
 tests/elab/14348.lean | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 tests/elab/14348.lean

diff --git a/tests/elab/14348.lean b/tests/elab/14348.lean
new file mode 100644
index 000000000000..890b35df54bb
--- /dev/null
+++ b/tests/elab/14348.lean
@@ -0,0 +1,8 @@
+module
+
+/-! Regression test for issue #14348: opaque constants of a unit-like type are definitionally equal. -/
+
+opaque a : Unit
+opaque b : Unit
+
+example : a = b := rfl

From 0ebf6bebde680dae095483b342ef3546a7b89f12 Mon Sep 17 00:00:00 2001
From: Salkutsan Aleksey <osalkutsan@godaddy.com>
Date: Thu, 30 Jul 2026 22:16:12 +0200
Subject: [PATCH 3/4] fix: restore opaque unit-like fallback

---
 src/Lean/Meta/ExprDefEq.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 1a8288f4cdd7..67e1bef823ef 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -2221,8 +2221,8 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
     -- which is very costly because it requires us to unify the fields.
     if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
       return true
-    if t.isConst && s.isConst then
-      if  then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
+    if t.isConst && s.isConst && t.constName! == s.constName! then
+      isListLevelDefEqAux t.constLevels! s.constLevels!
     else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
       return true
     else

From 2fdb44626720846e0d07602fa99b5496325c2fbe Mon Sep 17 00:00:00 2001
From: Salkutsan Aleksey <osalkutsan@godaddy.com>
Date: Thu, 30 Jul 2026 22:40:42 +0200
Subject: [PATCH 4/4] fix: limit constant fallback to unit-like types

---
 src/Lean/Meta/ExprDefEq.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 67e1bef823ef..0643b15fc60f 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -2221,8 +2221,11 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
     -- which is very costly because it requires us to unify the fields.
     if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
       return true
-    if t.isConst && s.isConst && t.constName! == s.constName! then
-      isListLevelDefEqAux t.constLevels! s.constLevels!
+    if t.isConst && s.isConst then
+      if t.constName! == s.constName! then
+        isListLevelDefEqAux t.constLevels! s.constLevels!
+      else
+        isDefEqUnitLike t s
     else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
       return true
     else