> You raise an interesting point, but it is my understanding that Swift is by far not the only language that has a shaky foundation in terms of type theory. Other type systems can at least be unsound, I don't know if any of them is undecidable.

It's more common than you'd think: https://typing-is-hard.ch

> the type errors that Swift returned were simply wrong and to fix it you had to put in type annotations in a bunch of places (without necessarily knowing where, just from the error messages)

The diagnostics engine was completely overhauled in Swift 5.2, so this shouldn't happen anymore: https://swift.org/blog/new-diagnostic-arch-overview/