I've been thinking about something similar. My idea is to let programmers specify various constraints they care about on numeric-typed variables, including min

I've been thinking about something similar. My idea is to let programmers specify various constraints they care about on numeric-typed variables, including min/max value. Then the compiler has the freedom to choose any representation(s) it cares to that matches the constraints. For complicated constraints that are difficult to prove at static-compilation time, some checks might be deferred until linktime (when static call contexts are available) or runtime.