match elaboration fails to unify definitionally equal types

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

inductive Mem (a : α) : List α → Type
  | head (as : List α) : Mem a (a::as)
  | tail (b : α) {as : List α} : Mem a as → Mem a (b::as)

def del : @Mem α a as → List α
  | .head as => as
  | .tail b mem => b :: del mem

def memOfDel : (mem : Mem c as) → Mem a (del mem) → Mem a as
  | .head _, mem => .tail _ mem
  | .tail _ mem, .head _ => .head _
  | .tail _ mem, .tail _ mem' => .tail _ (memOfDel mem mem')

The above code gives the following error:

type mismatch
  Mem.head ?m.1321
has type
  Mem ?m.1320 (?m.1320 :: ?m.1321) : Type
but is expected to have type
  Mem a (del (Mem.tail ?m.1316 mem)) : Type

However, the definitional equation for the tail case of del should result in the solution ?m.1316 = ?m.1320 = a and ?m.1321 = del mem.
Separating out the second match and adding a type ascription results in an even more inscrutable error:

def memOfDel' : (mem : Mem c as) → Mem a (del mem) → Mem a as
  | .head _, mem => .tail _ mem
  | .tail b mem, (mem' : Mem a (b :: del mem)) =>
    match mem' with
    | .head _ => .head _
    | .tail _ mem' => .tail _ (memOfDel' mem mem')

type mismatch
  mem'
has type
  Mem a (b :: del mem) : Type
but is expected to have type
  Mem a (del (Mem.tail b mem)) : Type

It is easy to verify that these are definitionally equal:

example : Mem a (b :: del mem) = Mem a (del (Mem.tail b mem)) := rfl

Using .tail (as := _as) b mem in memOfDel' succeeds, but it is not clear from the error message why this is necessary.

Steps to Reproduce

Run the code above.

Expected behavior: The code succeeds with no errors.

Actual behavior: The code gives the errors above.

Versions

Lean 4.16.0-nightly-2025-01-06

Impact

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

The issue names no repository file or test; start by running its minimal self-contained Lean example against the stated nightly version. Investigate match elaboration for memOfDel and its handling of definitionally equal types. The work is complete when both reproductions elaborate successfully and the behavior has regression coverage.