> the type checker/borrow checker has to understand arithmetic rules like `a != a+1`

I was actually thinking of this when I wrote, but the opposite case. A lot of compilers already know about that, and exploit it to their benefit (and sometimes the programmers dismay[1]). Overflow semantics matter here.

That said, it's looks like an interesting area for Rust. I'm sure it's already been discussed to death somewhere in the community. :)

1: https://news.ycombinator.com/item?id=14163111

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.