Unless you solve the [1] Entscheidungsproblem, taking two symbolic expressions (ie. two complex types) and finding if they are equal is unsolved and thought to

Unless you solve the [1] Entscheidungsproblem, taking two symbolic expressions (ie. two complex types) and finding if they are equal is unsolved and thought to be equivalent to solving the halting problem. [2] SAT style solvers are the best we have at the moment. Heuristics can be improved, of course. But we are really just shooting for common use cases in a turing complete language. Which really means...in a universe of infinite code and types that can be created - we are choosing to speed up our compiler for certain ones at the dismay of others. Overall though, since Swift is going to be used for making mostly trivial mobile apps, I don't really hold the academic high hat over it, let it take all the assumptions it wants. [1] https://en.wikipedia.org/wiki/Entscheidungsproblem https://en.wikipedia.org/wiki/Entscheidungsproblem [2] https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem