Defining a multi-dimensional array whose type tracks shape?

Stream: lean4

[Phil Nguyen]

I attempted the following definition, but it fails with (kernel) arg #4 of 'Tensor.array' contains a non valid occurrence of the datatypes being declared:

abbrev Vect (t : Type u) (n : Nat) : Type u := {xs : Array t // xs.size = n}

inductive Tensor (t : Type u) : List Nat → Type u where
| scalar : t → Tensor t []
| array : Vect (Tensor t ns) n → Tensor t (n :: ns)

If I swap out the definition of Vect with the standard textbook one, I'll get a different error (kernel) invalid nested inductive datatype 'Vect', nested inductive datatypes parameters cannot contain local variables:

inductive Vect (t : Type n) : Nat → Type n where
| empty : Vect t 0
| cons : t → Vect t n → Vect t (n+1)

inductive Tensor (t : Type u) : List Nat → Type u where
| scalar : t → Tensor t []
| array : Vect (Tensor t ns) n → Tensor t (n :: ns)

Where can I learn more about these errors, and how would one define such a datatype in Lean 4?

Thank you very much!!