Compiling nested inductive types

Dealing with multiple nested applications of the same inductive type

Consider the following inductive type declaration:

inductive foo (A : Type) : nat → Type :=
| mk : Π (n : nat), prod (foo A 0) (foo A 1) → prod (foo A n) (foo A (n+1)) → foo A (n+2)

There are two separate occurrences of inductive type applications with foo inside:

prod (foo A 0) (foo A 1)
prod (foo A <n>) (foo A (<n> + 1))

There are at least two different options for how to encode this into a mutually inductive type.

Option 1: Abstract all indices

Since foo occurs twice in the first inductive type application, we can create a copy of prod that takes two indices (one for each foo occurrence), and which otherwise mimics prod:

foo_prod : ℕ → ℕ → Type
foo_prod.mk : Π (n₁ n₂ : ℕ), foo A n₁ → foo A n₂ → foo_prod n₁ n₂

We can then search for other occurrences in the declaration of foo that match the pattern prod (foo A ?M1) (foo A ?M2). The second occurrence matches this and so can be captured by foo_prod as well. The resulting mutually inductive type is as follows:

inductive foo (A : Type) : nat → Type :=
| mk : Π (n : nat), fprod A 0 1 → fprod A n (n+1) → foo A (n+2)
with fprod : nat → nat → Type :=
| mk : Π n₁ n₂, foo A n₁ → foo A n₂ → fprod A n₁ n₂

Option 2: Only abstract non-parameter locals

The other option is to only generalize as much as is necessary to process each nested application in sequence. For prod (foo A 0) (foo A 1), we do not need our new inductive type to have any indices. However, since it does not syntactically match prod (foo A <n>) (foo A (<n> + 1)), we need to create a second copy of prod as well, and this second copy must take <n> as an index. Here is the result:

inductive foo (A : Type) : nat → Type :=
| mk : Π (n : nat), fprod₁ A → fprod₂ A n → foo A (n+2)
with fprod₁ : Type :=
| mk : foo A 0 → foo A 1 → fprod₁ A
with fprod₂ : nat → Type :=
| mk : Π (n : nat), foo A n → foo A (n+1) → fprod₂ A n