Type systems invariably have soundness issues when subtyping is allowed. They might've fixed it in the last couple years, but as an example I'm pretty sure Java

Type systems invariably have soundness issues when subtyping is allowed. They might've fixed it in the last couple years, but as an example I'm pretty sure Java and C# both have bugs where some methods should be co/contra-variant and others should not but the language only supports subtyping acting one way or the other for the whole type. For a concrete example: 1. Suppose Civic is a subtype of Car 2. Suppose you have a List<Civic> 3. Suppose a method asks for a List<Car> 4. You can "clearly" provide that original list of civics because every single thing in the list is a Car, and it's a list of those things, so it adheres to what the method seems to want -- maybe the method computes average cylinder count or something. 5. Everything we just described is fine and dandy so long as the list itself is immutable (the individual cars could still be mutable safely), but running some of the mutable list methods will cause runtime crashes and segfaults. E.g., if you append a toyota camry to the list then you've somehow snuck a camry into the original List<Civic>. In that example, some of the methods would be safe if you interpreted a List<Civic> as a List<Car> (like grabbing the car at a particular index and finding that the particular car is a civic), but others require the subtyping relationship to go the other direction (e.g., if you interpreted the List<Civic> as a List<BlueCivic> and appended a BlueCivic then the invariants expected by `append` work in both cases). That sort of thing just scratches the tip of the iceberg, and as a rule of thumb all your type systems are unsound, _especially_ if they involve subtyping. Things you would hope would be caught at compile-time are punted off to scary runtime heisenbugs that might not be detected for ages. The type system is helpful at reducing errors but woefully incomplete even for the things it's supposed to catch.