Hmm. This means we'd have to do mod every time we accessed an array which seems not great, right? But probably it could be optimized away for the common/easy cases.
Now, having refined the type this way, when you try elsewhere in the code to read some unknown byte into n, WUFFS will reject that because who knows if it exceeds 40? To make the code compile, you need to actually write code that ensures n is always less than 40.
Of course you aren't going to write big general purpose software under this sort of constraint, it's like having a two year old following you everywhere insisting on a detailed explanation of why you are doing every single thing and asking the most irritating "But why?" questions after each explanation, exhausting. But if you're processing untrusted data it's exactly what you needed to stay safe.
But I don't get how this would practically work. Would each array have a preferred n that is used for the mod operation? For most situations where that makes sense, using a 2d array seems more logical.
I assume the braces are there for "I want to skip doing the wrapping"