unfortunate interaction of `isDefEq`, `simp` and proof irrelevance

[hargoniX]

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

On Zulip a user proposed the following MWE:

structure Struct (n : Nat) : Prop where

def Struct.data {n} (s : Struct n) : Nat := n

variable (m : Nat)

structure Extend m extends Struct m

@[simp]
theorem fact (h : Extend m) : h.data = m := rfl

set_option pp.all true in
set_option trace.Meta.Tactic.simp true in
example (h : Extend m) : h.data = m := by simp only [fact]
/-
[Meta.Tactic.simp.discharge] fact discharge ❌️
      Extend m
[Meta.Tactic.simp.unify] eq_self.{u_1}:1000, failed to unify
      @Eq.{?u.151} ?α ?a ?a
    with
      @Eq.{1} Nat (@Struct.data m (@Extend.toStruct m h)) m
-/

The surprising behavior here is that h is left as an obligation for the simp discharger to solve instead of being solved through unification. The main reason for this seems to be that in the unification problem:

 @Struct.data ?m (@Extend.toStruct ?m ?h) =?= @Struct.data m (@Extend.toStruct m h)

only ?m but not ?h gets assigned. This is presumably the case because the subterm (@Extend.toStruct m h) is a proof so we directly skip it and never see the opportunity to assign ?h. This is not a deal breaker of course because the user can manually supply h to simp but still an unfortunate situation.

Context

#lean4 > Bizarre `simp` error

Steps to Reproduce

1. Run above example

Expected behavior: Should work without errors or alternatively simp should inform the user this is not a good pattern.

Actual behavior: Only works when h is provided explicitly to simp

Versions

Lean 4.28.0-nightly-2025-12-25
Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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