failed to generate equality theorems for `match` expression `ctor_C'.match_1`

Hey 👋

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”)

Similar issue:

• https://github.com/leanprover/lean4/issues/2237

Description

Here is the MRE.

This code

structure CellularAutomata where
  Q: Type u
  [inv_decidable_q: DecidableEq Q] -- comment this out

structure FCellularAutomata extends CellularAutomata where
  --[inv_decidable_q: DecidableEq Q] -- ...and uncomment this, then it works
  state_accepts: Q -> Nat

def ctor_C': FCellularAutomata :=
  {
    Q := Bool,
    state_accepts
      | true  => 1+1
      | false => 2+2
  }

def FCellularAutomata.d1 (C: FCellularAutomata): Bool := true

theorem t: ctor_C'.d1 = true := by
  unfold ctor_C'
  simp -- this fails with "failed to generate equality theorems for `match` expression `ctor_C'.match_1`"
  sorry

fails with

lean-nightly.lean:19:34
Tactic state
1 goal
⊢ ctor_C'.d1 = true
Messages (1)
lean-nightly.lean:19:32
failed to generate equality theorems for `match` expression `ctor_C'.match_1`
_x_1 : DecidableEq Bool
_x_2 : (motive : (CellularAutomata.mk Bool).Q → Sort u_1) →
  (Unit → motive true) → (Unit → motive false) → (x : (CellularAutomata.mk Bool).Q) → motive x
motive : (CellularAutomata.mk Bool).Q → Sort u_1
h_1 : Unit → motive true
h_2 : Unit → motive false
⊢ _x_2 motive h_1 h_2 true = h_1 ()

Because this example works, I assume this is a bug in how the type class is referenced.

Versions

lean-nightly.lean:6:34

Impact

So far I didn't find a workaround that unblocks me. But I'm only doing this for fun, so no urgency.

Start by running the linked minimal reproducible example against the Lean nightly release and inspect the simp step after unfold ctor_C'. Trace equality-theorem generation for the ctor_C'.match_1 expression, using the working comparison example to isolate the type-class difference. Done when the original theorem closes without the reported failure.