Array size unification instead of inference from index constraints

[jleben]

There might be an alternative to the complex array size inference from index constraints. The following might be simpler, more intuitive and still powerful enough:

For each array dimension, if bound is not provide in an array definition, then assume one from the context:

1. Explicit type annotation:

a :: [5]int
a[i] = i * 2;

This would also simplify piecewise array definition using equations - avoid repeating constraints for array bounds. E.g. avoid repeating j < 5 in the following:

a :: [~,5]int
a[i,j] = 0 if i < j;
a[i,j] = log(i-j);

2. Context of array expression - x[1] has size [5], because it must have the same size as x[0]:

x = [0 -> [5: i -> i], 1 -> [j -> j]]

This would make obsolete issues #1, #3.