Nested datatypes and vector

Stream: new members

[Borja Sierra]

Hello, I was trying to define a datatype of propositional formulas over an arbitrary language in the following way:

 structure prop_lang :=
mk :: (Symb : Type) (Arity : Symb → ℕ)

inductive Form (Var : Type) (ℒ : prop_lang)
| V {} : Var → Form
| Conn {} : Π (c : ℒ.Symb) , vector Form (ℒ.Arity c) → Form

but using the standard vector datatype (lists with fixed length) it gives me the following error:

nested inductive type compiled to invalid inductive type
nested exception message:
nested occurrence 'subtype.{1} (_nest_1_1.list.Form Var ℒ) (fun (l : _nest_1_1.list.Form Var ℒ), (eq.{1} nat (list.length.{0} (_nest_1_1.Form Var ℒ) l) (prop_lang.Arity ℒ c)))' contains variables that are not parameters

while if I define it with:

inductive myvector (α : Type) : nat → Type
| nil {} : myvector 0
| cons   : Π {n}, α → myvector n → myvector (n +1)

everything goes okay. I imagine this is because vector isn't really a datatype but it is a set over the list datatype while myvector is a proper datatype. After this I have some questions:
1) The error is really due to what I am supposing to?
2) It is a good idea to work with myvector datatype? I know it is quite standard in other languages (like Agda) but it seems that in lean it is not so used.
3) It is possible to define Form with vector (set of lists of fixed length) as a datatype (not as a set of well-formed formula over
a datatype where ill-formed formulas can be build).
Thanks to everyone!

[Mario Carneiro]

My recommendation is to avoid nested inductive types in lean 3 (and maybe lean 4, we'll see). You should just code it as a regular inductive type. One way to do this, similar to what is done in the flypitch project:

structure prop_lang :=
mk :: (Symb : Type) (Arity : Symb → ℕ)

inductive PreForm (Var : Type) (ℒ : prop_lang) : ℕ → Type
| V {} : Var → PreForm 0
| Symb (c : ℒ.Symb) : PreForm (ℒ.Arity c)
| App {n} : PreForm (n + 1) → PreForm 0 → PreForm n

def Form (Var : Type) (ℒ : prop_lang) := PreForm Var ℒ 0

[Mario Carneiro]

That is, you say "everything goes okay with myvector" but actually you will have issues when you want to e.g. define functions out of the nested inductive