Nested inductives cannot have indices

[blaxill]

Prerequisites

• [X] 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.

[nomeata]

Here is another example of this issue:

inductive Tree : Nat → Type where
 | node : {n : Nat} → List (Tree n) → Tree (n + 1)

I expect this will be an idiom that programming language theory users will want often (e.g. expressions with their context as index and n-ary binders).

But (at least with the current architecture) support for this would require significant extra complexity in the Lean kernel, which we of course want to avoid. So for now the best advise is to expand the data types you are recursing through into mutual datatypes.