Dependent types are not just useful for proving correctness properties, and in fact I think dependent types in Haskell are not really intended to prove really complex properties, like the full functional correctness of a compiler. Hence, I think the use of Coq or Agda proofs as an example of impracticality is a strawman argument. You might need a research team and several years to show the correctness of an operating system in Coq. You do not need that to have type-safe database access or statically checked matrix sizes. Not all non-research uses of dependent types are impractical.

You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? Should Java not have added lambdas because it already had anonymous inner classes? You can clearly get by just fine in a lot of business applications without some of these features.

I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. It’s not so clear that dependent types are too complex a solution there, especially if you look at a library like Servant, which already uses some advanced type system features, and which is actually a really practical library that is probably used in production applications as well. A library like Servant might be able to expressed more clearly with dependent types than with a hodgepodge of type system extensions. I think that wanting type-safe REST API access is already an order of magnitude more practical than model checking kernel code.