Swift type checking is undecidable

I too had this opinion of it from starting to read a (now out-of-date) book on Swift and Cocoa. It seemed some of the decisions eg. no fall-through for switch statements were done to reduce the possibility of bugs but just made it more irritating. I don't know if the language has changed in this regard though.

I always thought C# was the meeting place between Visual Basic and C++, where it was familiar enough to both language users to migrate, although occasionally different enough to cause problems (eg. generics vs templates). I don't know what Swift is "related to" in this regard - any ideas?

Of course, my lack of knowledge about Swift may show me up here so I am happy to be corrected and educated. This was merely an observation.

The Swift discussion in the article is very good and logically laid out.

The important context in the intro is, "The type checker needs to be able to determine that x and y have the same type, and reject the code if not. This is what we mean by computing canonical types."

There's a summary at the end titled, "what does this mean?" which says that undecidability doesn't bite in practice with real-world code, but the type system features discussed in the post have been the cause of bugs: "We are also aware of examples where we don't manage to canonicalize types properly, causing miscompiles and crashes. We've been fixing these gradually over time, but we continue to discover more problems as we fix them. This was a strong hint that the underlying approach was not correct, which is why I spent some time thinking about the fundamentals of this problem. Indeed, we can now see that the reason we have struggled with correctness in this area of the language is that a solution is impossible in the general case."

So the question arising from this undecidability is how to fix it: "What we need to do is come up with an appropriate restriction to the combination of SE-0142 and SE-0157. [...] I'm optimistic that introducing this restriction should have very little impact on real-world code."

No. This probably is similar to the definite assignment problem (https://en.wikipedia.org/wiki/Definite_assignment_analysis) in the sense that the problem for the current language is undecidable, but you can pick a usable subset of the language in which it is solvable (Java picked a very small subset for the definite assignment problem, making it very easy to implement that aspect of the language, without losing much expressiveness in practice)

If so, the main question the developers of Swift face is to decide in what way(s)/how much to constrain the current language.

A side effect of that could be that the compiler gets faster because the type checker will no longer have to consider some dark corners of the type system that were removed from the language.