I do agree if "compiler-enforced" is your target then by definition you'll choose compiler enforcement.
For me the cost is too high. I'd rather solve my documentation needs through other far less costly means.
> ...ease of refactoring.
This is one of the lies espoused by the strong static typer. The claim here usually is that the compiler will tell you where you're broken through each step of the refactor.
The irony is that the effect is the opposite of what is claimed: requiring a refactor to be formally/machine-verified correct through each iteration is a huge drag on refactoring.
In a non-strongly typed language I can iteratively refactor and execute parts of my program even if a formal verified/strong-type prover would reject the program.
This equates to way better throughput/speed over the formal static verifier/typer.
Formal static verification may give you a host of benefits but in what most of us are doing Time is the most important resource by far. And formal verification/strong-type systems are downright hostile to Time. Which is especially offensive because the claims of stability can be readily achieved through much more efficient and agile techniques than formal verification.