Honestly I can't think of an example of anything which is harder to model in Haskell's type system, but I think the Java and C examples demonstrate that you do have to learn different type systems to model more complex examples.
I totally agree that type systems end up reducing cognitive overhead in the long run though.
By definition, this can only happen if you use the wrong type in the wrong place : it can only be a huge bug or there is some dark magic I don’t understand.
I know a lot of langages manage to let you use strings as numbers and vice versa but I don’t see another case where you would voluntarily pass a wrong type. And this is not incompatible with string typing as long as the langage provides auto-casting.
This can lead to a runtime error, or it can make no difference whatsoever. Enforcing that consistency in the compiler is powerful but is also another obstacle to someone who's just trying to get a simple example working.
Just because there is a type error by no means qualifies it as a huge bug. That's why JavaScript and the web stack in general is successful. It fails gracefully. Instead of a rendering a website completely unusable, an error perhaps only renders a button in the wrong place.
Contrast this with Scala, where a subtle type error refuses to build at all. If you're green, hunting down the source of that error can be very arduous.
Failing at compile time can be very powerful but it can also add another obstacle to overcome.
It never happened since I switched to strictly typed langages and tbh, you rarely compile type errors if you have an IDE that shows in bright red that you are wrong.
The few times last years I had to write some Python, I really felt uncomfortable and it was really hard not to make mistakes and not to trust my IDE auto completion.
My brain is now plugged on « if I write something that is not proposed, it must be red ».
But again, I understand your point and maybe it’s just me.
Btw, there are other tools than compilers that can analyze your code for errors. Try PyCharm
But once you start adding lots of details, such as trying to specify the exact type of a stable sort operation, the overhead starts increasing dramatically. Another example I really love in this area is trying to code a type-safe MxN matrix multiplication that keeps track and validates measurement units for each element in each matrix (that is, it allows a cell in the result matrix to be 0.3m^2*s, but not 0.3m^2 + 0.1m). You'll find that few libraries, even in Haskell or F#, attempt such a thing, just because the types become infuriating and obscure the linear algebra.