> Turns out, the type system they built guarantees 100% that type checking is undecidable (in software developer terms, you can crash the compiler by typing per

> Turns out, the type system they built guarantees 100% that type checking is undecidable (in software developer terms, you can crash the compiler by typing perfectly legal Swift code and nobody at Apple knows how to fix it without breaking existing code because they didn't even know they built a language that has this property up until very recently). Undecidability means there's no algorithm that is guaranteed to terminate, not that any algorithm will crash. In this case, using a completion procedure to convert the same-type constraints into a confluent rewrite system should be sufficient. If completion fails an error can be diagnosed. This shouldn't break any real code in practice.