As the workhorse example, consider the length-indexed Vector:

    data Vec : Nat -> Type -> Type

Each Vec has its length in its type. You get a type error if you try the following:

    f : Vec 3 Int -> Int
    f [1, 2, 3, 4] -- error: wanted a Vec 3 Int, found a Vec 4 Int

and with that, consider the following program:

    import Data.Vect
    
    readInts : (n : Nat) -> IO (Vect n Int)
    readInts 0 = pure []
    readInts (S n) = do
      x <- getLine
      rest <- readInts n
      pure $ (cast x) :: rest
    
    main : IO ()
    main = do
      length <- getLine
      ints <- readInts (fromInteger . cast $ length)
      pure ()

The above program doesn't know what the type of `ints` is in the do-block precisely. It has a length specified by the user! But we can reason about its length - and the type system would ensure that its length is propagated and handled properly everywhere we try to use it.

It's just standard dependent types. Types don't (necessarily) get erased, but all the type checking itself is done at compile time.

I don't think it makes sense to think of it as specifically "statically kinded", since kinds (which are just types higher on the universe hierarchy) can also be present at runtime.

The terminology is nearing its limit when talking about these kind of things.

I believe that static typing here means that there is no need for runtime dynamics type checks (outside of things like dynamic dispatch as with haskell typeclasses).

That is you can have a body of code where a variable can assume multiple incompatible types, but you always know that it will be the right one.

I would say it is a change in paradigm. Similarly to how rust' borrow checker and lifetimes change the paradigm of manual vs GC memory management

It is more that you can have values like `payload : if byte[TYPE_OFFSET] == TYPE_INT then Int else String`.

You are required to disambiguate the type before anything useful can be done. What has happened is that you have types being passed around by functions and evaluations which reflect dynamic behaviour at runtime - but there is a type statically known at all times for each part of the program.