I definitely agree that one can paint themselves into a static-typing corner where refactoring becomes painful (but as I said, usually because of OOP). Also in big projects care needs to be taken to keep compilation times manageable.
> Languages should facilitate thinking of enforced correctness as a gradual concept, like gradual typing in Python, so the programmer has freedom to make these choices.
Depends on the domain. In web-based non-critical applications, maybe. If there's a bug, users gets and error etc. reports it, you push a fix to prod and things are usually OK. In things I mostly worked with (embedded, automotive, on-premise appliances, systems, p2p, finance), the cost of debugging and fixing small bugs is far too high.
I am supporter of gradual typing though, if someone wants to go with dynamic typing route.