Of course you have do deal with receiving data at run time, but I think very few people appreciate that it's actually possible to do the "input verification" at one specific point in your program and then have a "proven" safe input and then never have to do any validation/verification again. This even goes for things like "give me a vector of integers between 1 to 3 of size exactly 9 as input". Of course you still have to handle the invalid cases in that one specific place, but that's no different from how you'd ideally do validation anyway. That stuff already should be in a single place, and dependent types make that utterly obvious at compile time :).
(I think I may actually be agreeing with what you're saying, but I though it worth expounding on what dependent types can do for you.)
Btw, AFAIUI Liquid Types, at least as far as LiquidHaskell goes, is still a thing, though it's definitely quite "researchy" and who knows whether it'll become 'mainstream'.
Liquid Types also seem to be somewhat orthogonal to dependent types since they usually just rely on an external solver that works by "magic" (SMT) and which has built-in knowledge of e.g. arithmetic whereas most attempts at dependent types seem to want to avoid building in any of that knowledge in favor of induction + a more general "tactics" or "elaboration" type solving where the programmer guides the solver along. (Idris is an example of the latter, I think.)
Coming from dynamic languages towards appreciation of static types, this sort of thing is inspiring. I've been looking forward to writing some practical work in those languages when children and time give the chance.
This can be done with "tainting" types, which are simple intersection types (even Java has them as one of its new pluggable type systems [1]), and doesn't require dependent types.
You're going to get garbage data from paying customers. With a good information architecture you'll have 'lines' in the system and all of the data that goes past a certain point is guaranteed to be sanitized, at which point all this formalism helps you avoid really bad mistakes.
What ends up happening most times is a set of proprietary bespoke thunking layers that progressively sanitize the data until its usable. Everybody writes their own and they either suck or took lots of effort to get right. Or, the entire system is full of uncertainty and reads like a Choose Your Own Adventure as written by a squirrel.
Maybe there's a space there between the user and the formal type system that needs a set of transformation tools. Like htmltidy, but without the html.
The second thing is that sometimes you're going to get dynamic data at run time and you're going to have to use a run time property checker anyways. So for example if you needed to parse a bunch of text sent in by the user. You can still use dependent types to offload as much as possible to the type system, but at some point you'll have to deal with receiving user data. And if we go back to my first point, people are uncomfortable with using new things. They won't have a good idea of when to put what into the type system and what into the run time, so the default will be to just do it all at run time.
Liquid types look kind of promising, but I'm not sure if it's still an active research area. The stuff rust is doing with affine types is also promising. It's not dependent, but you can make a bunch of very nifty compile time checked apis. Finally, ML style types are slowly becoming more familiar in general in the industry. Once everyone is fully familiar with type parameters, they'll start to ask about kinds and values in types. However, it may take a while.