Failure to generate equality theorem for matcher

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

The generation of equational lemmas for some matchers fail. I have not investigated the issue further.

Steps to Reproduce

inductive NatTy where
  | nat

inductive NatExt : (Γ : List NatTy) → NatTy → Type where
  | const : Nat → NatExt Γ .nat

def foo  : NatExt Γ B → NatExt Δ B
    | .const a => sorry

/-Failed to realize constant foo.match_1.eq_1:
  failed to generate equality theorems for `match` expression `foo.match_1`-/
#check foo.match_1.eq_1

Expected behavior: No error

Actual behavior: Failed to realize constant foo.match_1.eq_1: failed to generate equality theorems for `match` expression `foo.match_1`

Additional informations

Note that this only triggers if NatTy has only one constructor. Adding another one, or matching on B in foo fixes the issue.

Versions

Lean 4.31.0-nightly-2026-04-10 Target: x86_64-unknown-linux-gnu
live.lean-lang.org

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 reproducer in live.lean-lang.org with the reported Lean nightly version and inspect the equality-theorem generation path for foo.match_1.eq_1. Done means the snippet produces no error and #check foo.match_1.eq_1 succeeds, including when NatTy has only one constructor.