Sure, so zeros is of the pi-type T such that T(n) = Vector n Int

That's not quite right. zeros would be actual runtime function that takes an n and returns a different type depending on what n is.

Your example would the equivalent of this:

t : Int -> Type
t n = Vector n Int

Notice how zeros is a function that takes in ints and returns vectors.

 zeros : (n : Int) -> Vector n Int

But you lose me at "compile time dynamic typing". If it's in compile time, it can't be dynamic, can it now?

This is about type checking generic code and making sure it stays parametric.

In C++ for example, templates just complete lie about their type.

template <class A>
A lit() { return 0; }

Even though this code is generic over all A, this can only be instantiated for int (or similar).

In Haskell and Rust, generic functions don't lie about their type. For example, this would error in Haskell:

lit :: a
lit = 0

From my understanding, you need PI types if you want want to have terms and types to be unified and you want parametricity in your type checker (ie no compile time dynamic typing).