Pi-type over a list in dependent type theory
You asked several questions.
You asked about a type indexed by a list, so you can do this.
data DataType (A : Type) (F : A -&gt; Type) : List A -&gt; Type where
  empty : DataType A F []
  _bla_ : forall {xs} {x} -&gt; DataType A F xs -&gt; F x -&gt; DataType A F (x ∷ xs)

Where F is a type family that is indexed by the elements of the list.
Apart from that, you mentioned tuples. Probably you want a sized vector (Data.Vec in stdlib) for tuples. For instance, Vec Nat 3 is such a type that 1 ∷ 2 ∷ [] and 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] are both invalid instances, only 1 ∷ 2 ∷ 3 ∷ [] is.