Java Arrays are not fully type-safe because they are covariant: ArrayStoreException can occur on an aliased array. Java Collections, on the other hand, are invariant in their type parameter: e.g., List<Thread> is not a subtype of List<Runnable> (which may be somewhat counterintuitive).
The motivation seems to do with Lists and other collections being mutable, so to keep the type system sane, their type parameters necessarily have to be invariant.
If a programming language only supported immutable types, could a type system where type parameters were either covariant or contravariant (but never invariant) work? In other words, to use Scala's way of expressing variance, one would have List[+E], Function[-T, +R], Map[+K, +V], etc.
I know that there are some older languages (e.g., GNU Sather) that seem to get away with supporting just co-/contravariant parameter types.
My general question is: in a world of completely immutable data types, is there a case where one would specifically need an invariant parameter type (as opposed to either co- or contravariant)? Are there some examples for immutable data structures that would only be correct with an invariant type parameter?
So, every type system either allows some unsound programs or forbids some sound programs or both (this is a consequence of Rice's theorem), so a good working assumption is that yes, any stricture you come up with is bound to rule out some sound programs that would otherwise have been allowed. On the other hand, humans are infinitely clever, so in another sense the answer is no: if you add a stricture like you describe, that's OK, people will figure out a way around it when they need to. (Of course, sometimes the workaround they'll come up with will be one you don't like, such as abandoning your language.)
But I think what you're really asking for is a convincing case: a realistic example where, given the choice between supporting that example straightforwardly and sticking with your proposal to require all type parameters to be either covariant or contravariant, your gut will tell you to abandon the proposal so you can support that example straightforwardly.
Since you've already identified various cases where a type parameter can't be covariant and various cases where a type parameter can't be contravariant (for example, Function[-T, +R] is fine, but the reverse would be totally unsound), a good approach is to search for cases where the same type parameter is used twice, once in a way that can't be covariant and once in a way that can't be contravariant. A trivial example would be UnaryOperator[T] <: Function[T, T], analogous to Java's java.util.function.UnaryOperator<T>, whose 'apply' method returns the same type as it accepts. A UnaryOperator[String] can't be used as a UnaryOperator[Object] (because you can't pass it an arbitrary Object), but a UnaryOperator[Object] can't be used as a UnaryOperator[String], either (because even if you pass it a String, it might return some different Object).
For a more fleshed-out realistic example . . . imagine a binary search tree TreeMap[K, +V] <: Map[K, V], analogous to Java's java.util.TreeMap<K,V>. Presumably we want to support methods such as 'firstKey' and 'floorEntry' and 'iterator' and so on (or at least, some of them), so we can't make K contravariant: a TreeMap[Object, Foo] can't be used as a TreeMap[String, Foo], because when we retrieve a key, the key might not be a String.
And since it's a binary search tree, it needs a Comparator[K] internally, which immediately makes it tricky for K to be covariant: if you use a TreeMap[String, Foo] as a TreeMap[Object, Foo], then you're implicitly using a Comparator[String] as a Comparator[Object], which doesn't work. Now, since the map certainly only contains String keys, perhaps the 'get' method can work around this by pre-checking the type of the key before calling using Comparator[String]; but the 'floorEntry' and 'ceilingEntry' methods are still a problem: what entry comes "before" or "after" an arbitrary object that can't be compared to the keys in the map?
And even though you've said that your map is immutable, you probably still want some sort of 'put' method, just, a purely functional one that returns a modified copy of the map. (Purely functional red black trees support the same invariants and worst-case asymptotic time complexities as mutable ones, so type system aside, this is certainly a reasonable thing to do.) But if a TreeMap[String, Foo] can be used as a TreeMap[Object, Foo], then its 'put' method needs to support returning a binary search tree that contains a non-String key — even though its Comparator[String] doesn't define an ordering for such keys.
(In a comment, you mention that Scala actually defines Map[K, +V] with an invariant key type. I've never used Scala, but I bet that this is exactly why.)