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.