This is basically the solution py2many uses for handling overflow from fixed width integer types when transpiling from python to low level systemsy languages such as Rust/C++ and Go.
Please file bugs if something deviates from what's expressed here.
This is an explicit deviation from python's bigint, which doesn't map very well to systemsey languages. The next logical step is to build on this to have dependent and refinement types.
Please file bugs if something deviates from what's expressed here.