Perhaps I’m missing something basic here, but why aren’t you just using infinite-precision rationals and just be done with it? This is the type-checker, not the runtime, right? So you should be perfectly safe using something less efficient than native ints, yes? Just arrange to check in all computations on constant-expressions/values, for overflow, and everything should be fine, yes?
Maybe I’m just missing something really basic. But for example, recently, perusing the Ocaml AST, I noticed that it went from using “int” in integer-constants, to using strings + a one-char indication of which type the string was a member of.