What @xwu is getting at, and that I believe you understand (though disagree with), is that this issue isn't a technical limitation of Swift, but an explicit design decision to not support, because of the implications for the type system.
I'm guessing that you're aware of this, but any logical system has an inherent conflict between soundness and completeness. Soundness implies that truthful statements in the system can only be used to lead to more truthful statements, while completeness implies that all truthful statements can be produced by the system, one way or another. Less abstractly, for type systems, this means that:
- A sound type system is one which only allows programs with valid type relationships to compile
- i.e., "if it compiled, it must have been valid"
- A complete type system is one which will compile any program with valid type relationships
- i.e., "if it is valid, it will compile"
Soundness is great for correctness: "the program compiled, so from a type perspective, it will do what I want". Completeness is great for getting stuff done: "man, I'm glad the compiler got out of my way to let me do what I want".
Unfortunately, you cannot have both, not as an implementation limitation, but as a limitation of the universe. It is not possible to have a system which is both completely sound and complete at the same time: either the system is sound but there will be programs that exist that, although correct, will not compile, or the system is complete but there will be programs which are incorrect that do compile. In a very practical sense, it comes down to tradeoffs, and priorities.
Static type systems tend to lean more toward providing soundness, while dynamic type systems tend to lean more toward providing completeness. Swift, as a matter of intentional design, leans heavily toward soundness, even at the cost of certain programs being impossible to represent.
The examples that both you and @realityworks have provided are pretty clear violations of the Liskov substitution principle, to which Swift adheres. This principle covers some pretty fundamental rules that prop up the soundness of subtyping relationships, and breaking these rules leads to inconsistencies in the type system that cannot somehow be patched up.
Whether intentionally or not, the request here ends up boiling down to Swift relaxing its rules about subtyping relationships — which I think is antithetical to Swift's goals. This also isn't something that can be supported "just a little bit", for example, but not more generally.
(This isn't at all to say that Swift's type system is perfect, or that there aren't countless cases where the compiler can do more to allow correct-but-hard-to-express programs to compile more easily, but this is a pretty foundational set of rules to relax that I simply don't see happening.)
In very reduced terms: it’s not possible to have 1 + 1 occasionally equal 3 without also having some pretty far-reaching consequences.