No. Mutation essentially breaks subtyping. The infamous ArrayStoreException in Java is the story of how references (which should be invariant) are treated as covariant and therefore causes runtime exceptions.
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.
No. When references or arrays of references are treated as contravariant, you would have the opposite problem of ArrayReadException. You can now store things into arrays safely but you can no longer extract things from arrays safely.
