In a nutshell, all dependent type systems are very impractical to use and are widely seen as going way past the point of diminishing returns for real world scenarios. It's not really a coincidence that most illustrations of dependently type programs never go beyond a simple list/stack/vector structure.

I'll take a statically typed language with a decent type system and and assortment of tests any day over a dependently typed language.