[hutao]

Note that addition also won't overflow if one addend is greater than half the range, but the other addend is still small enough (e.g. for the range -128 to 127, adding 65 + 12 will not overflow, even though 65 is greater than half of 127).

Your intention of having the restricted domain "NonNegativeLessThanHalfMaxValue" is probably so that both addends have the same domain. If you go down that route, perhaps you'll also want the closure property, meaning that the range should also belong to the same set. However, then you have to deal with the overflow problem all over again...

The real point is that when adding two N-bit integers, the range must be N+1 bits, because the "carry bit" is also part of the output. I think this is a scenario where "Parse, Don't Validate" can't easily help, because the validity of the addition is intrinsically a function of both inputs together.