>>40n might be received from input, in which case you have to insert a runtime check. On the other hand, n might be the result of a convoluted calculation that may make a runtime check unnecessary. In that case you would have to prove that this particular calculation preserves this particular invariant. And this proof may require a hell of a lot of writing because the compiler is not an AI and does not understand code the way you do.
Then there's the problem of modularity: if you export a function that preserves some invariants, you have to be able to declare that property, because the client must be able to prove things about your code without seeing your implementation. And that means more writing on your part.