If your array type (the only reified generic type in Java) is going to be parameterized by a single type, then you're right that it needs to be invariant.

One alternative would be to keep track of two types for an array: the most general type that can be stored into it and the most general type that might come back out of it. Any type cast that makes the types storable more strict or the type expected coming out less strict should be allowed. If you throw in a bottom type in your type system, then you get immutable arrays for free.

Of course, such a type system would probably cause a revolt among the majority of Java programmers for being too complex.