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 scen

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.