I think it was Oleg Kiselyov who pointed out that if you push these expressive dependent type systems to their (illogical?) extreme, what you end up with is a situation where the language in which types are written is itself a dynamically typed programming language.

When I was an undergraduate, formal specifications (e.g. Z) were all the rate. What we've discovered since then is that formal specifications are just as hard to debug as code. Possibly even harder.

hugo
I had also commented asking if anyone would elaborate why almost nothing useful is written in the great language that is Haskell [...]

I can answer that one. Apart from European banks (several of which write a lot of their code in Haskell), Haskell, like most programming languages, has developed an implicit theory about what it is "for". Haskell is "for" research and development of programming languages. You will probably never write a nontrivial program in Haskell, but chances are almost certain that the programming language that your employer asks you to write code in tomorrow will have acquired some of its more interesting features from Haskell.

It is for this reason that Haskell's unofficial motto is "avoid success at all costs".