match elaboration fails to unify definitionally equal types

[cppio]

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.