Checked exceptions are decent example here. The set of checked exceptions a function might throw is part of its signature, and the built-in function types don't declare any checked exceptions.
But I've run into others. I find that Optional<T> and Java Streams have some design quirks that are mostly no big deal if you're using them in predominantly object-oriented or procedural code, but quickly become irritating if you're trying to follow a scrupulously functional idiom. And some of the design implications of how Java did generics at a language level have a way of sneak attacking you when you're trying to scrupulously follow a functional idiom. Not because of type erasure (really, Haskell is the poster child of type erasure; this definitely isn't about type erasure), but because some limitations in what kinds of generic types the language will actually allow you to express can quickly back you into mind-bending workarounds like the the curiously recurring template pattern.
THAT SAID
I'm really thinking here of functional programming in more of the ML/Haskell tradition, which is a peculiar way of doing things that does tend to lean pretty hard on the type system. If we're just talking about using higher-order functions, that's great. Higher order functions absolutely have a place in object-oriented programming. Java should have had them decades earlier than it did. The virtual machine that the JVM was largely based on was for a language that used them heavily, Strongtalk, and I'm not sure I understand why the Java team took them out. I'm sure there was some technical challenge, but I can't help but wonder if it's really because Java was born during the great "Lisp vs Everyone Else" war of the 80s and 90s, and the feature was purged for political reasons.
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.
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.
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.
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.
What language are you talking about here?
1. I once happened to have a look at a Python codebase where some poor soul had tried to write Java in Python. Quite literally. It was not a good experience.
2. Many moons ago I had a task of implementing a repetitive something for many somethings in C++. Being the newbie I was I just set out typing out all the methods. Then a more senior colleague of mine, after having watched the ordeal for a few minutes, asked for my keyboard to type out a signature of a templated function to suggest that I could try 'something like that'. Noticing my blank stare he proceeded to delete the scribble with the words 'It's fine, you were well on your way to finish it!'. I stopped him, and saved the snippet in a file titled 'black_magic' to later grok it. Now I know. But I didn't then. I think he was wise in his approach to reality.
3. At some point I got accidentally involved in a C# project. To my eyes it was full of accidental complexity. But I was not expected to be a core contributing member later on. So I'd do my own thing in parts of the code base allocated to me, changed all the structs to classes as required in code review, and made sure the whole thing fits together well with all the layers upon layers of abstraction. Because it wouldn't be mine to maintain, so it better be made the way people who will maintain it like it.
So, the general advice 'When in Rome...' may apply here. I mean, what's the chance that after an 'enlightened' contractor changes a Java code base to a functional paradigm comes someone 'unenlightened' just to rewrite it back? Considerable, I think.