Think through declarations of bounds for checked array variables.

[dtarditi]

Currently, it is possible to declare bounds for a fixed-size checked array, Consider the following example of declaring a global array with bounds:

int len;
float g50 checked[10] : count(len);

This implies that 0 <= len < 10 must hold true through the program. Currently there is no constraint on len. We could add require a where clause for len that implies that len is always within range of the fixed size array. We would face a similar issue for variable-sized arrays.

Forbidding bounds on fixed-sized arrays is not a reasonable option. It is a C idiom to have a incomplete array type as part of an interface:

extern int len;
extern float g50 checked[]

[dtarditi]

We could forbid bounds on fixed-sized arrays, and allow bounds on incomplete array types. It makes sense for a bounds declaration on::

extern float arr checked[];

We could disallow

extern float arr checked[10];

We would still need to define what hapens if arr is declared as an incomplete type with bounds and then declared as a complete type without bounds., though We would probably require that the declared bounds on the incomplete type be provably within range. This would allow something like:

int len where len <= 10;
extern float arr checked[] : count(len);
extern float arr checked[10];

This isn't quite right under the current language rules.. We require that bounds declarations be syntactically identical across redeclarations of an entity (unless the entity has an unchecked type, in which case the bounds declaration can be omitted).

Following that rule, the bounds declarations have to be identical.

int len where len <= 10;
extern float arr checked[] : count(len);
extern float arr checked[10] : count(len)

This suggests s that we should allow bounds on fixed-sized checked arrays because we need them for consistency of the language definition. We do need to add a rule that the bounds from the type of a fixed-size array must imply that any declared bounds are valid.