I'll answer this:
often it leaves the programmer wandering through old concepts, without knowing where to apply dependent types
Sure types can be used to eliminate certain types of silly bugs, like when you apply a function to its arguments in a wrong order, but this is not what types are really for. Types structure your reasoning and allow to zoom into the structure of your computation.
Say you process lists and use head and tail a lot, but these are partial functions, so you decide to switch to something safer and now you process NonEmpty a instead of [a]. Then you realize that you also do a lot of lookups (a partial function again) and that it won't be too troublesome to maintain lengths of your lists statically in this particular case, so you switch to something like NonEmptyVec n a, where n is the statically known length of a vector. Now you have eliminated lots of possible bugs, but this is not the most important thing that happened.
The most important thing is that now you look at the type signatures and see what kind of input functions expect and what kind of output they produce. Possible behaviour of a function has been narrowed by its type signature and now it's much easier to identify where in the pipeline the function belongs. But also the more detailed types you have, the more encapsulated your entity is: a function of type NonEmpty a -> b no longer relies on the assumption that a non-empty list will be passed to it, instead it explicitly requires this invariant to hold. You've turned a jelly-like tightly coupled computation into a fine-grained one.
What rich types are for is to guide humans (before code writing, during code writing, after code writing) and reduce their ability to produce bugs in the first place — not for spotting them a posteriori. Simple types I consider unavoidable, because even if you write code in a dynamically typed language, you still distinguish between a string and a picture.
Enough chit-chat, here is a real world example of usefulness and, more importantly, naturalness of dependent types. I'm targeting an API with the help from the Servant library (which is an amazing piece of code and is dependently typed also, so you might want to check it):
type API a r = ReqBody '[JSON] (Operation a) :> Post '[JSON] (Result r)
So we send a request of type Operation a (automatically encoded to JSON by Servant) and receive a Result r response (automatically decoded from JSON by Servant). Operation and Result are defined like this:
data Method = Add | Get
data Operation a = Operation
{ method :: !Method
, params :: !a
}
data Result a = Result
{ result :: !a
}
The task is to perform operations and receive responses from a server. The problem however is that when we Add things, the server responses with a AddResults, and when we Get things, the server's response depends on what we passed together with the Get method. So we write a type family:
type family ResultOf m a where
ResultOf Add a = AddResults
ResultOf Get DictionaryNames = Dictionaries
The code reads better than my description above. It only remains to lift Methods to the type level, so we define an appropriate singleton (which is the way to emulate dependent types in Haskell currently):
data SMethod m where
SAdd :: SMethod Add
SGet :: SMethod Get
And here is the type signature of the main function (omitted lots of unrelated things):
perform :: SMethod m -> a -> ClientM (ResultOf m a)
perform receives a method in a singleton form and some value and returns a computation in the Servant's ClientM monad. This computation returns a result which type depends on both the method and the type of the value: if we SAdd, we get AddResults; if we SGet DictionaryNames, we get Dictionaries. Very sensible and very natural — no need to invent where to apply dependent types: the task loudly requires them.
