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

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.

Start by running the minimal self-contained Lean example from the issue against the reported nightly version and inspect the included simp trace. Investigate the isDefEq and simp interaction around proof irrelevance and the unification problem shown. Done means the example works without explicitly supplying h, or simp clearly reports that the pattern is unsupported, with regression coverage for the behavior.