To have immutable arrays that are statically checked for immutability in a statically typed language, the immutability needs to be part of the array's type. That requires syntax at least; not insurmountable - we can take inspiration from C++, and imagine e.g. final int[] foo vs. int final[] foo (the latter meaning that the array itself is immutable, and that it can be replaced, but only by another immutable array).

But do keep in mind that this fundamentally makes the immutability a property of the variable, not the object it holds. The point of static typing, and thus static checking, is to examine the statically available information; and the objects don't exist until runtime.

Converting references would probably not be desirable. Of course it would defeat the purpose to be able to treat an immutable array as if it were immutable. But binding a mutable array to an "immutable array" type variable is also not that useful; while that could help the programmer avoid certain kinds of unintended mutations, it would not allow for any additional reasoning about the code (i.e. "the array's elements will not change within this scope") as long as anyone else could have a reference to the same array object.

To have immutable arrays that are statically checked for immutability in a statically typed language, the immutability needs to be part of the array's type. That requires syntax at least; not insurmountable - we can take inspiration from C++, and imagine e.g. final int[] foo vs. int final[] foo (the latter meaning that the array itself is immutable, and that it can be replaced, but only by another immutable array).

But do keep in mind that this fundamentally makes the immutability a property of the variable, not the object it holds. The point of static typing, and thus static checking, is to examine the statically available information; and the objects don't exist until runtime.

Converting references would probably not be desirable. Of course it would defeat the purpose to be able to treat an immutable array as if it were mutable. But binding a mutable array to an "immutable array" type variable is also not that useful; while that could help the programmer avoid certain kinds of unintended mutations, it would not allow for any additional reasoning about the code (i.e. "the array's elements will not change within this scope") as long as anyone else could have a reference to the same array object.