Two things. Firstly, it is simply not the case that all constraints must be able to be statically enforced for them to constitute part of the type's definition

Two things. Firstly, it is simply not the case that all constraints must be able to be statically enforced for them to constitute part of the type's definition. I'd guess that's a huge part of the confusion here. But, yes, actually all WUFFS indexing is statically checked. It's using inference to conclude the range of the index, so if it won't fit that's a static type mismatch.