Interestingly, arithmetic on the Mill CPU does this (at the machine level instead of at the language level). You can get modulo addition, saturating addition, widening addition, and excepting addition.
http://millcomputing.com/wiki/Instruction_Set_by_Category#Si...
Generic (compound) constraints could also be useful.
Like this:
(Value >= 0 && Value <= 1000 && (Value & 1) == 0) || Value in(value_enum)
Would limit Value to even numbers between [0 .. 1000] except if it's an enum (for error values).
Hmm, I can see why that would be useful but that makes it much harder to reason about in order to automatically eliminate checks wherever possible; you can guarantee that adding a number in [0,100) to [0,100) will produce a number in [0,200) without needing to apply checks, but one of your Values may generate an error if you just increment it.
Compilers already reason about values like that. They can prove certain bits in an integer to have certain values, etc, not just about ranges. Actual checks could be optimized away pretty often.
Simple example: Say, you multiply a number by two. From that, the compiler data flow analysis knows the lowest bit can only be zero. So it can safely optimize away anything that checks that bit.
So rather than declaring vaguely that you want an "integer", you'd specify bounds, signed-ness (two or one's complement), and what happens on overflowing the bounds (wrap / saturate / exception / trap / set flag / set NAN etc.)
Saturated arithmetic intrinsics are widely available but generally not used by generated code. Similarly I've never seen an attempt at doing "integer NaN", which could be quite useful in some situations.
You'd probably also want some flags to say "give me a compiler error or warning if this code doesn't compile to intrinsics and is being emulated instead".