> The result is that the program will run in an infinite loop until either the fixed-size Int rolls over to 0, or the bignum-style integer consumes all availabl

> The result is that the program will run in an infinite loop until either the fixed-size Int rolls over to 0, or the bignum-style integer consumes all available memory. That's certainly incorrect behavior. But I'd like to see your "sufficiently powerful type system" that will handle that. I believe that Agda could do this.