I mean, what stops it is

> this will likely require some additions to the contract specification.

You need a lot more machinery to move this stuff to compile time, and not everything can be checked at compile time. The first example in the post would require you to validate that a <= v's len before indexing in order to be evaluated at compile time, for example. (Which of course is a runtime check anyway...)