I think the real value of the index type is in admitting these kinds of specializations. i.e., to lean in to index as an “infinite precision” integer, rather than as an “implementation defined” integer with finite precision. Another option would be to generate run-time checks when lowering to a specific (e.g. 32- or 64-bit) target or lower to an infinite-precision implementation.