ATS uses infinite precision ints only for the proof/dependent type checking. The ints used at runtime are machine ints. It's to avoid overflow during type system checking.