It absolutely matters, type systems don't exist in a pure universe, they are important because we use them to interact with human needs. A good type system pushes out typing concerns to the outer boundary of of the system. For that you don't need static typing, you need strong typing. Refactoring in a statically typed system can be an incredibly tedious process with tons of boilerplate. At the other extreme if you allow duck typing and monkeypatching then you wind up with a problem where debugging becomes a problem. There's a middle ground that a lot of very good and productive programming languages occupy.
You're not going to find many people who agree that static-typing makes refactoring harder. The classic issues with large coupled dynamically-typed systems is how difficult refactoring is without runtime errors.
You also have to be more precise when you hand-wave about benefits of "strong typing" as you can read this very comments section to see how nobody agrees on what that means.
By 'type concerns' i mean coercing the real world into the type system. You want that to be at the edge.
IMO, treating a program as a proof is somewhat impracticable as you see with very pure functional programming paradigms struggle with universal state monads.
