failed to generate equational theorem

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

Starting in version 4.18.0, Lean fails to generate equational theorems for certain well-founded recursive definitions.

Steps to Reproduce

inductive IsZero : Nat → Type
  | mk : IsZero .zero

def isZero : ∀ n, Option (IsZero n)
  | .zero => some .mk
  | .succ n => match isZero n with
               | none => none
               | some .mk => none
  termination_by n => n

Expected behavior: Code succeeds with no errors.

Actual behavior: The following error:

error: failed to generate equational theorem for 'isZero'
case h_2
x n : Nat
⊢ ((match (motive :=
        (n : Nat) →
          Option (IsZero n) →
            ((y : Nat) → (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y n.succ → Option (IsZero y)) →
              Option (IsZero n.succ))
        n, isZero n with
      | n, none => fun x => none
      | .(Nat.zero), some IsZero.mk => fun x => none)
      fun y a => isZero y) =
    match n, isZero n with
    | n, none => none
    | .(Nat.zero), some IsZero.mk => none

Versions

v4.18.0-rc1, v4.18.0, v4.19.0-rc1, v4.19.0-rc2

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 self-contained IsZero/isZero reproducer against the listed Lean versions and the latest nightly release. Compare the expected successful compilation with the equational-theorem generation error and use that failure as the regression boundary. Done means the reproducer compiles without errors while preserving its well-founded recursive definition.