The meta-level definitional equality check spuriously fails for constants with differing universe parameters

Description

The definitional equality check at the meta level (not the kernel) always fails when checking equality of two expressions that are both references to the same constant when the universe parameters are not equal. However, it is still possible that both might unfold to definitionally equal terms or that they may satisfy the rule that all inhabitants of unit-like types are definitionally equal.

Steps to Reproduce

Use the following code:

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 _ _

/--
error: type mismatch
  rfl.{1}
has type
  Eq.{1} T.{u} T.{u} : Prop
but is expected to have type
  Eq.{1} T.{u} T.{v} : Prop
-/
#guard_msgs in
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'''

Expected behavior:

test should type check successfully, just like the other two versions do. There should be a delta reduction of T, as the kernel is using, or alternatively an application of the rule for unit-like types.

Actual behavior:

It does not type check.

There seems to be a general assumption in this code that all constants are injective WRT universe levels. I think this is true for type constructors and constructors, but not for definitions. This assumption is manifest in the following two locations:

Versions

This occurs at least in 4.12 and the latest nightly (4.15.0-nightly-2024-11-15)

Link to live.lean-lang.org

Additional Information

For applications, the problem is not manifest. All of the following are accepted:

abbrev T2.{u} (_ : Nat) : Unit := (fun (α : Sort u) => ()) PUnit.{u}

def test2.{u, v} : T2.{u} 0 = T2.{v} 1 := rfl

def test2'.{u, v} : T2.{u} 0 = T2.{v} 1 := rfl (a := ())

theorem test2''.{u, v} : T2.{u} 0 = T2.{v} 1 := by
  unfold T2
  rfl

Impact

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

leanprover / lean4