There is an objection here that I bring from my history and linguistics background and that’s that no specification is perfectly clear in all cases, and no implementation matches everyone’s reading of the spec.
Part of learning to code in any language is to use the language to your advantage and avoid problematic behavior. Type systems offer some security guarantees, but categorization is a fun problem with serious edge cases and philosophical difficulties.
Yes, Java’s type system is unsound. Long run, chances are one will fund any complex type system to be unsound.