>How did you use scala? Did you write java code in scala as most people with a C++/C#/java background do? Because that would completely explain the rest of your post.

Nope.

My issue here is that types, once defined, rarely change in any significant fashion. Refactoring is (generally) an exercise in mutation of logic, not so much the underlying types. When types do change the code that operates on them drastically changes as well. We're no longer refactoring at that point, we're re-writing and then the issues more or less disappear.

>The obvious example of that being a bad assumption is that static type systems can completely eliminate unexpected NULL errors.

What? In Scala it is perfectly possible to pass an uninitialized reference to a piece of code. The type checker most definitely isn't going to catch that. It can merely verify that the reference itself is of the right type. This is actually a common runtime error in those languages.

>It can eliminate "oops I used the count as the X co-ord by mistake" style errors.

Just as long as the count and the X co-ord are of different types. Which I'd guess isn't always the case.

> It can eliminate a huge class of errors that java programmers don't recognize are in fact type errors.

I will concede that static type systems do catch some errors that aren't caught by dynamic languages. My belief is that the class of errors they catch are among the most trivial, and most easily caught in testing (unit-testing or otherwise). Thus I simply don't see big gains in either runtime correctness or refactorability. Maybe slight ones, but nothing worth the loss of expression provided by more dynamic languages. This is true of even softer type systems such as Hindler-Milner (although type inference continues to improve, there might be some middle ground here to explore in the future).

There is no doubt some philosophy at play here. The discussion here is much broader than refactoring alone. I for one find that giving up some formal proof about the correctness of the program is worth the freedom dynamic languages provide.

I'll leave my favorite quote on the subject:

"Static type checking limits programs to only expressing things that the static type system can prove are OK, as opposed to expressing things that the human programmer believes are OK. That's the source of both the expressiveness loss with statically checked languages, and the class of runtime type errors which are unique to dynamically checked languages." - Anton van Straaten