After playing with dependent types and type driven development, almost every language has been spoiled for me :(
So imagine how you would design a language with dependent types that would match the productivity of Interface Builder when designer GUIs.
Or a being able to provide something like Unity.
Not only the whole interactive design process, but also the ability to ship UI components that can be integrated into the designer's toolbox.
How would a drag & drop action, or mouse click binding an event to a slot, reflect into the existing type definitions.
Plus that was just one example, I can pick Delphi, Smalltalk, Windows Forms/WPF/UWP, VB or plenty others as example.
I guess you did this with Idris?
When moving from dynamically/untyped/unityped languages to those with types, you are liberated from having to check the shape of inputs. If you're given something that claims to be a list of strings, it absolutely is a list of strings, and you can proceed without thinking about it's list-ness or string-ness any further.
When moving from a typed language to a dependently typed language, you are liberated from having to check the state of inputs. You don't have to worry that your file handle is closed, or ensure that you update the state of the object correctly to satisfy some protocol (if you don't, you will be picked up on it!). If you are writing a parser, you don't need to check that the parser returned the form that you just called - you know upfront.
There are other niceties: the type of the function is always a very rough exposition of what the function should do. With dependent types, it becomes considerably clearer. Consider these two functions, which could have very similar implementations (in some Idris-like syntax):
f : Int -> Int -> Bool
data T : Int -> Int -> Type where
Tz : T 0 x
Ts : T a b -> T (a + 1) (b + 1)
g : (x : Int) -> (y : Int) -> Maybe (T x y)
The flipside of your description of moving from un typed to typed to dependent typed languages is the amount of specification you need to think about and add to your code. This is awesome for component interfaces, but it can often get in the way of internal code. For example, if I try to redactor a long function and extract a few bits, those bits may only be called with very specific argument values, despite what the types I have on hand (or am willing to define) might say. Languages without some dynamic escape hatches can force you to create code that is too general, or define extremely specific types, for situations that really don't call for it.
It also makes very generic or dynamic code much harder to write, or requiring ever more complex constructions. For example, most mainstream typed languages can't express something as simple as 'a function that returns either an A or a B' without resort g to dynamic typing and casting. And even in Haskell, a lot of code is more loosely typed than might be expected. For example, even though measurement units are often touted as a feature of typed languages, there are no complex mathematics libraries that use measurement units, simply because it is so much effort to correctly type everything, for relatively little gain.
There is always a necessary distinction between specification and implementation: if there weren't, one of them would have no value. We often suggest that the intent of a piece of code should be specified in comments, and this is in that category. This way, the compiler can read your comment and figure out if it needs updating! Languages without dependent types work this way too - but you have to try very hard indeed to be eloquent in type signatures, and being able to talk about values lets you say a bit more.
Coming onto your second point: if the function is only valid for some set of values of the given type, why is it 'not really called for' to create specialised types for it? If you call it with something else and it runs, it will be a bug. Newtypes or wrappers are common patterns.
I think that most mainstream typed languages have common constructs to offer that 'A or a B' value you want: this is solved via inheritance, `Either`, `Result`, or `std::variant`.
My point about newtypes and wrappers is that they are almost pure overhead for helper functions. There is a reason why we don't define precise types for each of our intermediate calculations in general, and this doesn't change when we move those computations to a separate function.
Finally, inheritance is not a real solution for returning A or B, with inheritance I can only return a C that both A and B derive from, and this C often doesn't exist and can't be added post-hoc. What you normally do is go for Object or void*, which is much closer to dynamic typing than inheritance. And most mainstream typed languages don't have Either or Result. C++ with std::variant is the only exception, I forgot that it was added. BTW, I should be more explicit - the way I see it, the mainstream typed languages are Java, C#, C, C++, and maybe Go.
You can achieve this with other languages (e.g. Smalltalk), but many of the most popular languages feel more like inanimate tools (some very good ones!).