`rfl` does not work for unit-like opaque constants

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Usually, any two terms of the same unit-like type (with a single constructor with no parameters) are considered definitionally equal. However, when comparing two opaque constants, the definitional equality check fails prematurely.

Steps to Reproduce

example (a b : Unit) : a = b := rfl -- succeeds

opaque a : Unit
opaque b : Unit

/--
error: Type mismatch
  rfl
has type
  ?m.3 = ?m.3
but is expected to have type
  a = b
-/
#guard_msgs in
example : a = b := rfl

Expected behavior:

• Opaque constants should mostly behave like free variables.
• Any two terms of type Unit should be definitionally equal and rfl should certify this.

Actual behavior:

rfl cannot prove opaque a b : Unit to be definitionally equal, but it can prove two such fvars to be.

Versions

Lean 4.33.0-nightly-2026-07-09
Target: x86_64-unknown-linux-gnu

Diagnosis

private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
  [...]
  if t != t' || s != s' then
    Meta.isExprDefEqAux t' s'
  else
    [...]
    if t.isConst && s.isConst then
      -- The `return false` is where we exit prematurely.
      if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
    [...]
    else
      whenUndefDo (isDefEqProjInst t s) do
      whenUndefDo (isDefEqStringLit t s) do
      -- This `return true` is the exit we'd like to take.
      if (← isDefEqUnitLike t s) then return true else
      isDefEqOnFailure t s

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal reproduction and inspect the isExprDefEqExpensive entry point, especially the opaque-constant branch and the isDefEqUnitLike check shown in the diagnosis. Run the #guard_msgs example before and after changes. Done means rfl proves equality between the two opaque Unit constants and the regression behavior is covered by a test.