One of the core issues is that arbitrary dependent types require writing difficult formal proofs [0]. Xavier Leroy, who, as the main author of CompCert -- probably the only non-trivial program proven end-to-end [1] with the use of a proof assistant based on dependent types -- has often said that even he, a world expert, had found this so laborious that he views manual proofs as viable only to small programs (and CompCert, while non-trivial, is certainly a small program). Short of that, the question is exactly how useful it is to prove only those properties that are easy to prove. Another issue is that there may be better alternatives (which could be combined with restricted, "easy", forms of dependent types. Contract systems (like Java's JML), are as expressive as dependent types, but separate specification from verification, meaning, they allow you to state program properties formally, and then use either (expensive) formal proofs or weaker forms of verification (like generated tests) to verify them. Proofs are both extremely costly and are very rarely a requirement; their added confidence beyond other, weaker, but far cheaper, forms of verification is very rarely worth their tremendous cost.

[0]: See this example of a simplified Quicksort in Idris: https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris

[1]: End-to-end verification is ensuring that global correctness properties (e.g., "the database is always consistent", or "no user ever gets access to another's data") are preserved all the way to source code or even to machine-code. Most "formally verified" software, at least in industry, isn't verified end-to-end. Rather, either global properties are verified not against the code but a high-level description of the software or only local properties are verified at the code level, or both (but with a gap).