[hmry]

Not OP, and not sure about OCaml and Haskell, but one example where Java's type system is unhelpful/incorrect is mutable subtyping.

E.g. Java assumes Cat[] is a subtype of Animal[]. But this only holds when reading from the array. The correct behavior would be:

- `readonly Cat[]` is a subtype of `Animal[]`

- `writeonly Cat[]` is a supertype of `Animal[]`

- `readwrite Cat[]` has no relationship with `Animal[]`

But Java doesn't track whether a reference is readable or writable. The runtime makes every reference read-write, but the type checker assumes every reference is read-only.

This results in both

- incorrect programs passing the type checker, e.g. when you try to write an Animal to an Animal[] (which, unbeknown to you, is actually a Cat[]), you get a runtime exception

- correct programs not passing the type checker, e.g. passing a Animal[] into an writeCatIntoArray(Cat[] output) function is a type error, even though it would be safe.

(Although all that is assuming you're actually following the Liskov substitution principle, or in other words, writing your custom subtypes to follow the subtyping laws that the type checker assumes. You could always override a method to throw UnsupportedOperationException, in which case the type checker is thrown out of the window.)

Interestingly, AFAIK Typescript makes these types both subtypes and supertypes at the same time, in the interest of not rejecting any correct programs. But that also allows even more incorrect programs.

[moring]

Did you mean arrays instead of lists? Arrays behave as you describe (with ArrayStoreException when you write a wrong value to an array). List<> is invariant WRT its type parameter.

[hmry]

Yeah, sorry, you're right. I have edited my comment. Thanks for the correction!

[repelsteeltje]

Another issue is that Java's initial containers were type-less and were then type generics were retro fitted as erasures.

[bmandale]

All type checkers either permit incorrect programs, reject correct programs, or are turing complete.