Generics made Java’s type system unsound due to an unanticipated edge case. The Go team got a bunch of top-class type theorists (e.g. Phil Wadler) to make sure that Go’s generics implementation doesn’t introduce a similar problem.
>just an academically interesting property - had zero real life impact.
Only because Java runs on the JVM, which preserves enough type information that an exception will be thrown if you try to treat a list of String as a list of Integer. In a language that compiles to native code with full type erasure, that could give rise to serious security problems.
You can just imagine what Go critics would be saying on HN if Go's generics implementation allowed that kind of thing to happen!
No, you need to go way way out of your way to make a real world example for that - otherwise it would have been discovered by a bug, not by academics. It’s similar to Java’s generics being Turing complete - cool, but you can never make use of that/write it accidentally.
I am not as inclined as you to think that accidentally creating an unsound type system is no big deal. Soundness is exactly the property that makes type systems useful. Note the adverb at the beginning of the paper’s abstract:
> Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM.
