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₂

definition real_foo.mk (A : Type)
                       (n : nat)
                       (p₁ : prod (foo A 0) (foo A 1))
                       (p₂ : prod (foo A n) (foo A (n+1)))
                         : foo A (n+2) :=
match p₁, p₂ with
| prod.mk f₁ f₂, prod.mk f₃ f₄ :=  foo.mk (fprod.mk f₁ f₂) (fprod.mk f₃ f₄)
end

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)) (up to locals-renaming), 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

definition real_foo.mk (A : Type)
                       (n : nat)
                       (p₁ : prod (foo A 0) (foo A 1))
                       (p₂ : prod (foo A n) (foo A (n+1)))
                         : foo A (n+2) :=
match p₁, p₂ with
| prod.mk f₁ f₂, prod.mk f₃ f₄ := foo.mk (fprod₁.mk f₁ f₂) (fprod₂.mk f₃ f₄)
end

Trade-offs

I don't think it matters much, and the second one is probably easier to implement. However, the first one may be preferable if we expect many nested applications that will unify semantically but not syntactically.