Optimisers reason about this, yes, but they don't define the user-facing language model. They take valid code and transform it in to (hopefully) faster valid code[1] and don't generally emit diagnostics or fail compilation, this means that they can do much more guess work and heuristics rather than having to have predictable, reliable or definable behaviour, all of which are useful for humans writing code (having a predictable optimiser is useful too, but difficulty writing any code at all is worse than difficulty optimising the spots where the optimiser isn't hitting performance targets).
Integrating this sort of thing into the type system "properly" (as in, actually part of the language and doing all of what I think Animats wants) basically means going a long way towards full dependent typing.
[1]: behaviour on invalid code, such as C relying on signed integer overflow, is unspecified/undefined. Languages like, say, Rust and Haskell generally try to guarantee the optimiser never gets invalid code by flagging such instances at compile time, unlike most/all C and C++ compilers.
Integrating this sort of thing into the type system "properly" (as in, actually part of the language and doing all of what I think Animats wants) basically means going a long way towards full dependent typing.
[1]: behaviour on invalid code, such as C relying on signed integer overflow, is unspecified/undefined. Languages like, say, Rust and Haskell generally try to guarantee the optimiser never gets invalid code by flagging such instances at compile time, unlike most/all C and C++ compilers.