Unlock existentials with fixed associated types

[AnthonyLatsis]

This proposal is a step towards generalized existentials and focuses on adding support for values of existential type when the associated types are known and representable (fully concrete).

protocol P { associatedtype X }
protocol Q: P where X == Never {}

struct Conformer: Q {}

let foo: Q = Conformer() // OK

---

This proposal has been merged with the more general proposal on lifting the “Self or associated type” constraint on existentials (#1176)

[AnthonyLatsis]

Could you surround the error message in ticks? The error is already confusing and inaccurate enough, we would not want people to read it as ordinary text.

[filip-sakel]

I don't think that'd be wrong. I think we should either find a satisfactory definition that doesn't require ticks (and maybe reference the recognizable error in parenthesis with the ticks) or just not include the ticks (and maybe note that this is similar to the infamous error message). I say that because the introduction should be plain text and include a proper definition for what's to be discussed.

[AnthonyLatsis]

The problem is that a real definition is not as simple, but we shouldn't need to clarify the exact definition of which existential types are not supported today (being relative is enough for this proposal). While the plain text makes for an awful explanation, a quote completes the explanation by having everyone recognize the error message.

I say that because the introduction should be plain text

There is no such rule or convention for SE proposals.

[filip-sakel]

There is no such rule or convention for SE proposals.

I'm aware of that. I am, however, concerned about how understandable that will be to future readers. Reading older proposal is quite common; therefore, if we opt to use an error message relevant to the current diagnostics, this proposal might be confusing to future readers. That's why I propose finding a short - yet elegant - definition that will make sense even without knowledge of the current diagnostics' error messages (I'm not saying that finding such a definition is easy).

Of course, this the current message is not absolutely terrible; it still makes sense, even without being completely accurate or easily graspable. Thus, future readers, without necessarily understanding that this used to be an error message, would still be able to understand what we are referring to. So, I've added the ticks, but let me know what you think:

Today, Swift protocols are divided into two categories: those that can be used as fully-fledged types, and those that can only be used as generic constraints because they have 'Self' or associated type requirements. However, in some cases where a protocol inherits and fixes the associated types of another protocol - that doesn't have Self requirements, this constraint seems rather unintuitive. This proposal aims to relax this needless constraint allowing such protocols to be used as Types.

[AnthonyLatsis]

To save us the troubles of properly defining what "Self requirements" actually means (which is not at all trivial), let us define this in terms of which protocols will become supported

Now, a protocol can be used as a type when

• the implementations of its associated type requirements are known
• there are no Self references in requirements that are already preventing it from being supported

[filip-sakel]

I agree with the idea of not using the non-obvious term "Self requirements", however I have a couple of notes on your updated definition:

1. Saying "the implementations of its associated type requirements are known" implies that for the rule to apply, the given protocol must have associated requirements; that's not true.

2. (Personal Preference) Saying: "the implementation of a requirement is known" may confuse some readers. Maybe, saying: "its associated types are known" would suffice. Another direction we could take is use the word "fixed" instead of "known", since the compiler may know the implementation of such a requirement, but still not make it usable as a type due to it not being fixed.

3. Saying "are already preventing it from being supported" isn't really necessary. It is implied by this definition that whatever doesn't meet the outlined criteria will be unusable as a type.

With all the above changes, the improved definition would look like this:

Now, a protocol can be used as a type when:

1. the implementations of its associated type requirements — if there are any such requirements — are fixed, and when
2. there are no Self references in requirements.

[AnthonyLatsis]

Saying "the implementations of its associated type requirements are known" implies that for the rule to apply, the given protocol must have associated requirements; that's not true.

How about "Now, a protocol with associated type requirements can used as a type when ..."?

Another direction we could take is use the word "fixed" instead of "known", since the compiler may know the implementation of such a requirement, but still not make it usable as a type due to it not being fixed.

Knowing the implementations of all associated type requirements implies that they (the implementations) are fully concrete. "Fixed" is inaccurate for some cases of class-constrained existentials. As soon as I add the missing example, the meaning behind "known" should become more clear.

Saying "are already preventing it from being supported" isn't really necessary. It is implied by this definition that whatever doesn't meet the outlined criteria will be unusable as a type.

We want to avoid explaining "Self references" (not all references to Self count). Dropping that part of the sentence makes the criteria opaque.

[AnthonyLatsis]

A single "Do Nothing" alternative becomes a logical extension of the motivation section. Since "Do Nothing" is indeed the only foreseeable alternative in our case, could we make this part of the motivation instead?

[filip-sakel]

I've removed the Alternatives Considered section altogether and moved some of the Do Nothing section's arguments to the Motivation section.

Motivation

[...]

All in all, this behavior seems like an abnormality in the exitentials system. There has, also, been post after post asking why this feature isn’t yet implemented. Tackling this ‘issue’ will strengthen the foundation of existentials allowing for exciting future additions.

[AnthonyLatsis]

Looks good! As an aside, there is the generics system, but I have never heard anyone use the term "existentials system" before. Unless you know of a source, could you replace it with "type system"?

[AnthonyLatsis]

This proposal has been merged with the more general proposal on lifting the “Self or associated type” constraint on existentials (#1176)