[mafribe]

I'm not saying this can't be done, au contraire! Indeed cost coherent programming idioms can be converted into typed language primitives. But there is a price to pay in terms of typing system complexity.

It's a slippery slope argument: if you add this, why stop there? Especially if you require run-time checks.

If there was a compelling set of operation that preserved the invariants without run-time checks, and it was expressive, i.e. it covered a large number of cases that you'd otherwise had to put into "unsafe" and it didn't ruin type inference ...