diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 3bc3e69ab997..7ec4842a7c87 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -2426,7 +2426,10 @@ 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 t.constName! == s.constName! then
+        isListLevelDefEqAux t.constLevels! s.constLevels!
+      else
+        isDefEqUnitLike t s
     else if (← pure t.isApp <&&> pure s.isApp) then
       if (← isDefEqApp t s) then return true
       isDefEqAppFallback t s
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