But complicated type systems are, unfortunately, rarely used in languages suitable for system programming. I only know about ATS in this group actually :-)
I have some hope for Rust because their type invariants system (I forget what they're calling it) lets you glue some of this information to variables in a compelling way without necessarily having to solve all the theoretical and practical problems that come with full dependent typing.
We'll see, I guess.
int array[10];
With dependent types function to get element from array may have type (this is pseudocode): get (array : T[n], index : m) : T {n : nat, m : nat, m < n} which would mean "function get, which takes: n long array of elements of type T, index of type m, where m is smaller than n, and returns T". Type-level naturals and bounded array access are the basic examples of dependent typing, more interesting ones may be red-black trees with guarantees about their shape put in the type or some magic for creating DSLs.