I think you might be misunderstanding what type erasure does. It's really just about whether type information is retained at run time, in order to support run time type checks. Hindley-Milner type checking, on the other hand, happens at compile time.
In a rigorously statically typed language like Haskell that does all the type checking at compile time, there is no need to retain types at run time, so they are erased. Java is a less statically typed language. Variables have types, but you're allowed to upcast all the way up to Object, and then do a dynamic type check and downcast at a later time. It's just that the language won't do this transparently for you the way it will in a more fully dynamically typed language. In order to support this, though, Java cannot erase types.
The controversy with Java is that, when generics were introduced, they decided that generic type parameters would be erased. This greatly undercuts the soundness of the type system. If you're not careful (or if you're trying to be clever), you can insert a String into an object that had been declared to be a List<Integer>, and you won't get any errors until you try to iterate over the list and a run-time type check suddenly blows up your program because some code finds itself interacting with a String even though the compiler's static type check had confirmed that the code should have only ever been able to operate on Integers.
The thing to call attention to here, though, is that this is at least as much about Java's relatively weak static type system as it is about erasing type parameters. If Java (the language) had something closer to a Hindley-Milner type system with stronger static type checks, then it might have been able to catch shenanigans like that at compile time. It's a question of framing: the problem could have been handled by using type reification to enable stronger run-time type checks, but it might also have been solved by using stronger compile-time type checks to eliminate the need for those run-time checks in the first place.
That said, this is pretty deep out in speculative territory, since it's doubtful that either option could have been executed without major breaking changes, which Java definitely wasn't going to do.
> If you're not careful (or if you're trying to be clever), you can insert a String into an object that had been declared to be a List<Integer>
It's less about type erasure and more about missing covariance/contravariance in Java generics. Scala also has type erasure in generics (same JVM), but won't allow that (unless you explicitly upcast). HM doesn't recognize inheritance, so it's in a completely different category.
> The controversy with Java is that, when generics were introduced, they decided that generic type parameters would be erased. This greatly undercuts the soundness of the type system.
Not at all.
Like you said yourself, type erasure has consequences at runtime but zero impact on the type system.
What you probably mean is that the type system can be circumvented at runtime, but you don't need erasure for this, standard operations such as casting already allow that.
It has zero impact on a static type system, but it has huge impact on any run-time type checking.
So, for example, you can't really do dynamic typing and type erasure. More generally, you can't do any dynamic type checking, including casts when types have been erased. OCaml does a more complete version of type erasure, and also lacks a casting operation. Because you can't safely cast if the run-time can't dynamically verify that the cast is valid.
(Tangentially, and Java is a great example of this - static and dynamic typing are not a binary. There are actually quite a few different kinds of type disciplines, and, in practice, it's common for languages to do some things statically and some dynamically.)
The soundness problem for Java is that, with the way it did generics, they don't really fit cleanly into Java's original type discipline. There are some things that tradition would have dictated be handled dynamically, but can't be in the case of generics because generic types only have partial run-time type information. At the same time, they weren't handed by the compiler, either, presumably because, historically, they fell outside the type checker's bailiwick. So they ended up being nobody's responsibility, and just not checked.
Nowadays we do generally get warnings for the most common situations where this happens, but there's no real way to fix them. You just silence the warning with an annotation to tell the compiler, "Trust me, I know what I'm doing." Meaning that, yeah, there's even a little bit of weak typing in Java. At least as of Java 5.
In a rigorously statically typed language like Haskell that does all the type checking at compile time, there is no need to retain types at run time, so they are erased. Java is a less statically typed language. Variables have types, but you're allowed to upcast all the way up to Object, and then do a dynamic type check and downcast at a later time. It's just that the language won't do this transparently for you the way it will in a more fully dynamically typed language. In order to support this, though, Java cannot erase types.
The controversy with Java is that, when generics were introduced, they decided that generic type parameters would be erased. This greatly undercuts the soundness of the type system. If you're not careful (or if you're trying to be clever), you can insert a String into an object that had been declared to be a List<Integer>, and you won't get any errors until you try to iterate over the list and a run-time type check suddenly blows up your program because some code finds itself interacting with a String even though the compiler's static type check had confirmed that the code should have only ever been able to operate on Integers.
The thing to call attention to here, though, is that this is at least as much about Java's relatively weak static type system as it is about erasing type parameters. If Java (the language) had something closer to a Hindley-Milner type system with stronger static type checks, then it might have been able to catch shenanigans like that at compile time. It's a question of framing: the problem could have been handled by using type reification to enable stronger run-time type checks, but it might also have been solved by using stronger compile-time type checks to eliminate the need for those run-time checks in the first place.
That said, this is pretty deep out in speculative territory, since it's doubtful that either option could have been executed without major breaking changes, which Java definitely wasn't going to do.