Nested inductives cannot have indices

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The definition of Foo1 below succeeds, but Foo2 fails with the error (kernel) invalid nested inductive datatype 'Prod', nested inductive datatypes parameters cannot contain local variables.

inductive Foo1 : Nat -> Nat -> Type where 
| bar1 : ∀ (a b: Nat), (Foo1 a b × Foo1 a b) -> Foo1 a b

inductive Foo2 : Nat -> Nat -> Type where 
| bar2 : ∀ (a b c: Nat), (Foo2 a c × Foo2 b c) -> Foo2 a c

Expected behavior: The definition of both Foo1 and Foo2 to succeed.

Actual behavior: Foo2 fails with the error (kernel) invalid nested inductive datatype 'Prod', nested inductive datatypes parameters cannot contain local variables.

Reproduces how often: 100%

Versions

Checked on:

• Lean (version 4.0.0-nightly-2022-12-16, commit f6cd6c069587, Release) MacOS
• Lean (version 4.0.0-nightly-2022-10-22, commit 1e00eff3e7e8, Release) MacOS

Additional Information

For this trivial example expanding Prod works, i.e.

inductive Foo2 : Nat -> Nat -> Type where 
| bar2 : ∀ (a b c: Nat), Foo2 a c -> Foo2 b c -> Foo2 a c

but my use case is more complex.

Start with the self-contained Foo1 and Foo2 definitions in the issue, comparing the failing nested Prod case with the expanded constructor form. Done means the original Foo2 definition is accepted without the invalid nested inductive datatype error, while preserving the reported behavior.