You could actually have runtime checks by default (in a hypothetical language), and have a smart compiler elide them whenever possible.
int32 a, b = ...;
a+b; // there is a check
// implicitly:
// if (MAX_INT32 - a
but
int32 a = ...;
// after here: typeof(a) = int32
int32 b = rand_int(0, 1000);
// after here: typeof(b) = int32[x|where x >=0 and x
So the compiler would be able to narrow down the type of a variable, and know what operations are safe to perform. This is probably impossible in the general case (halting problem and so on), but I believe it is very doable if you restrict yourselves to a limited number of subranges. This is like a kind of dependent types, but completely internal (you could expose them, if you wanted though).
The compiler can't only use this extra information to remove overflow checks, but you can also have a language that guarantees there is no overflow - add two int32 and the result is an int64, and so on. And if it can infer that the result fits in an int16, then it can put it in there. But most of the time you would just use int, which means: integer variable of enough length to store my data. int8, int16, int32, maybe a BigNum. Kind of like python does it, but with the ability to pick optimized native types if needed.