Kinda. Let's be honest: in production this often turns into a pain in the ass. There's some value in dependent typing, but providing evidence that concatenating UTF-8 strings is associative is not one of them.

For example if my function returns a Vector[A, N] (a vector of A's with size N), and I try to pass it's return value to a function that expects a of type Vector[A, 2] my code will not compile. This is because there is no way one can prove forall A N. Vector[A, N] satisfies Vector[A, 2].