Internal error in mkElimApp: Expected first 3 arguments of motive in conclusion to be one of the targets

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

inductive Ind (pair : Type × Unit) : Unit → pair.fst → Type where
| mk q : Ind _ () q

example (i : Ind (Unit, ()) () ()) : True := by
  cases i -- Error here
  sorry

Produces:

Internal error in mkElimApp: Expected first 3 arguments of motive in conclusion to be one of the targets:
  ?m.10 () ()

Expected behavior: The cases tactic succeeds.

Actual behavior: It fails with an internal error.

Versions

Lean 4.24.0-nightly-2025-09-06
Target: x86_64-unknown-linux-gnu

Impact

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

Start with the minimal inductive example in the issue and reproduce the failure from the cases tactic. Trace the mkElimApp error and the eliminator construction involved in handling the indexed Ind type. Done means the example's cases i succeeds without the internal error and existing tests remain passing.