The point is that you don't need a static language to get many of the benefits of types, you just need your language that allows you to express type-based properties. One of the way to do that is to have a set of formal rules for deriving the type of every expression in a program, but that's not actually necessary.
It enables a whole class of highly effective program manipulations that are just unavailable to a non-statically-checked language.
* Changing the collection's type and not knowing until runtime -- when your program crashes -- that it's being used wrong.
* Changing the collection's type and the program refusing to compile until all usage is corrected.
Because of this, I don't agree with the most modifier you're attempting to apply. The difference to me is confidence. In the former, how confident am I that I didn't miss a use-case on some branch? Considering that the program will crash or otherwise fail to operate, that seems like something I want to be pretty confident about.
It's very useful to have something telling you that everything looks OK. That something can be testing, but why rely on writing good tests when we have formal proof systems available?
> For example, most of these advantages apply to Julia as well...
and then you listed it as an advantage.