SE-0309: Unlock existential types for all protocols

[Dante-Broggi]

@sighoya

I disagree. But maybe the term existential is redefined in Swift context, but this would lead to more confusion for users coming from other languages already knowing existentials.

So, I believe that this side discussion is fundamentally about a disagreement over the definition of "existential".

IIUC, your definition of "existential" is similar to:

a value of an existential of protocol P is a value v for which there exists a type T, such that v is of type T and T conforms to P.

Under this definition the value boxed in any P and both possible extensions of some P are existentials.

---

However, IIUC the definition of "existential" in general use in the Swift community is similar to:

a value of an existential of protocol P is a value b which contains a value v for which there exists a type T, such that v is of type T and T conforms to P, and b contains proofs of those statements about v.

Under this definition, any P, but not the value boxed in it, is an existential, but some P is not, because the proofs for some P are not stored in the value, but in the context.