There are some languages heading towards this. ATS [1] provides a restricted form of dependent types [2] that allows you to do what you want and is designed for systems programming. You can do safe pointer arithmetic for example.
Idris [3] is another language with dependent types (and is more Rust-like) designed for systems programming. I don't think Idris has type level presberger arithmetic though making some things a bit verbose.