SE-352: Losing constraints when type-erasing resulting values

Evolution Discussion
1

Hi all,

I wanted to talk about this part of https://github.com/apple/swift-evolution/blob/main/proposals/0352-implicit-open-existentials.md#losing-constraints-when-type-erasing-resulting-values. The idea at the time was that once SE-353 was fully implemented, the inferred type of an erased value might change, eg from any Sequence to any Sequence<Int>, since a more precise upper bound could now be expressed.

Thus, the erasure had to be annotated with an explicit coercion, eg, as any Sequence, to avoid a possible source break in the future. If you don't state the implicit coercion, it outputs a diagnostic inferred result type requires explicit coercion due to loss of generic requirements.

Now, SE-353 was implemented, and we now compute the most precise upper bound that can be expressed with parameterized protocol types. The check remains, though, and as the proposal states, it is still possible to write down a generic signature and a type parameter, such that the type parameter's most precise upper bound cannot be expressed by existential types.

For example, if I have the generic signature <T where T: Collection> and I'm erasing a value of type T.SubSequence, the most precise upper bound we can write down today is any Collection. However, T.SubSequence has the special property that T.SubSequence.SubSequence == T.SubSequence, which not all any Collections satisfy. So really, using invented syntax, the most precise possible upper bound is actually any Collection<.SubSequence == .Self> or any <T> T where T: Collection, T.SubSequence == T or whatever.

For this reason, we ask you to insert the coercion here, because as we saw above the upper bound here is imprecise:

func f<T: Collection>(_: T) -> T.SubSequence { fatalError() }
let v: any Collection = [1, 2, 3]
f(v)

However, if you change the return type of f() to just T, the diagnostic is still emitted, even though clearly any Collection completely describes the T in <T where T: Collection>, and indeed we've had a few bug reports of this nature.

Now, it's certainly possible we will gain more expressive existential types in the future, and at that time we can consider changing the upper bound computation again to make use of this new expressivity. Requiring these coercions now would lessen the possibility of source breaks in the future, so if we could fix up the bugs with a bit of implementation effort, that would be great.

On the other hand, I'm not sure the problem is solvable. Consider just the case of a generic signature <Self where Self: P>, and P has a bunch of recursive associated types and same-type requirements:

protocol P {
  associatedtype A: P
  associatedtype B: P where ...
}

For every string T of A's and B's, Self.T conforms to P, so we can erase Self.T to any P. Is this the most precise upper bound? Well, here's the actual property you want:

Given T, any P will be the most precise upper bound for T, if and only if for all possible strings U, V, whenever Self.T.U is equivalent to Self.T.V, then Self.U is equivalent to Self.V.

If you can find such a pair U, V where Self.U is distinct from Self.V, But Self.T.U is equivalent to Self.T.V, you know the answer is 'no'. But you can't enumerate all possible pairs and test each one. I don't know how to implement a solution to this problem. (It might even be undecidable, but I'm not sure yet. Certainly it's undecidable for a general finitely-presented monoid because so is equivalence, but even for a monoid presented by a finite convergent rewrite system, I'm not quite sure you can solve it in 100% of cases.)

Instead, I propose removing the diagnostic, arguing that it has outlived its usefulness now that constrained existentials are available, and plugging the remaining gaps is not worth the effort: Cleanups and fixes for opened existentials by slavapestov · Pull Request #69950 · apple/swift · GitHub. If you're a fan of this diagnostic, please speak now, or forever hold your peace.

12 Likes