That's why I like the index type idea: [n] i = ...; int i1 = length(i); /* fine, but we dont know what i1 is */ [n] i2 = length(i); /* error, we as

That's why I like the index type idea: [n] i = ...; int i1 = length(i); /* fine, but we dont know what i1 is */ [n] i2 = length(i); /* error, we assume length can return any int */ [n] i3 = length(i) < n else panic(""); /* also fine, and maybe we can optimize out the check, but we don't have to */