Properly deal with multiple conditional sources of conformances

[kyouko-taiga]

A "source of conformance" is a declaration that introduces a conformance of a type T to a trait P. Even with global coherence, a program may contain multiple sources of conformances introducing T : P because of trait refinement:

type A { ... }
conformance A: Equatable { ... }
conformance A: Hashable { ... }

Because Hashable refines Equatable, the above program has two sources of conformances for A: Equatable. Indeed, even if we remove the first conformance declaration, we'll still be able to conclude A: Equatable from the last declaration.

I naively thought we could ignore this issue but I didn't consider conditional conformances. For example:

type B<T> { ... }
conformance B: Equatable { ... }
conformance B: Hashable where T: Hashable { ... }

Again, there are two sources of conformances for B<Int>: Equatable but one is conditional and so we can't use any source at random. We have to use the one introducing Equatable specifically, or the one introducing its least specified super trait. Sadly that causes a problem because trait refinement doesn't form a tree so there could be ambiguous choices.

trait P {}
trait Q: P {}
trait R: P {}

type B<T> { ... }
conformance B: Q where T: Hashable {}
conformance B: R where T: Comparable {}

There are two sources of conformances for B<Int>: P with different where clauses and there's no criterion deciding that one is a better choice than the other.

AFAIU, Swift addresses this issue with two crucial restrictions. First, Swift says that a conditional conformance T: P where C does not imply a conformance T: P0 where C for any trait P0 refined by P. Under this rule, the above example would be illegal because B: Q where T: Hashable does not imply B: P. Second, given two traits P, P0 such that the former refines the latter, Swift says that if T : P where C and T : P0 where C0, then C must subsume C0.

We most likely have to impose the same rules.

[kyouko-taiga]

In fact, it's possible that the problem isn't as hard as I thought if we frame it in the context of universally quantified extensions.

Let's think about what trait refinement means in Hylo. When we say that Q refines P we're not describing a subtyping relationship (at least in the commonly understood sense) but rather a sort of implication stating that a conformance to Q implies a conformance to P. Intuitively, if the conformance to P is conditional, we could expect that the conformance to Q must satisfy the same conditions but I don't think that's actually true.

Consider the following to illustrate:

trait P {}
trait Q: P {}
type A<T> {}
conformance A: Q where T: Hashable {}

If we give an equivalent program to Swift, the compiler will complain that "conditional conformance of type 'A' to protocol 'Q' does not imply conformance to inherited protocol 'P'". I think the error makes sense iff

1. the declaration of ∀T, A<T>: Q cannot also act as a source of conformance for ∀T, A<T>: P.
2. we assume that declaring T : R1 implies there exists T : R0 for each trait R0 refined by R1.

I'm under the impression that none of these requirements is actually justified. To understand, we first have to realize that a trait nothing more than an abstract type with a single generic parameter, named Self. I'm using the term "abstract" as it relates to abstract classes in languages like Java or Scala.

trait Copyable { fun copy() -> Self }
// is notionally equivalent to
abstract type Copyable<Self> { fun copy() -> Self }

When we're saying that a trait "refines" another trait, we're merely placing a bound on the Self parameter of the former. With this idea in mind, we could rewrite the program using universally quantified extensions:

trait P {}
trait Q {} where Self: P
type A<T> {}
conformance<T where T: Hashable> A<T>: Q {}

The failure that Swift reports is due to the fact that nothing proves A<T>: P. This requirement is stated explicitly in the declaration of Q, where it reads Self: P and is rewritten as A<T>: P after substituting the Self parameter of Q for A<T>.

Okay, but what's the difference between this program and one in which the conformance is not conditional?

// ...
conformance<T> A<T>: Q {}

Well, there is almost none. We still have to prove A<T>: P here. It seems to me that Swift simply makes an exception for unconditional conformances and I don't see an obvious reason why it can't apply the same logic to conditional conformances too. So, unless I'm missing something, the first requirement I stated above can be dropped.

Now regarding the second requirement, let's assume we can write the following:

// ...
conformance<T where T: Hashable, A<T>: P> A<T>: Q {}
                                 ~~~~~~~~

Here I'm asking for a conformance A<T>: P in the where clause. Now the conformance no longer assumes that A<T> also conforms to T and so we no longer have to prove this requirement. We can just take it for granted. It is only when we'll try to exercise the conformance that we'll have to prove A<T>: P, i.e., at "use site".

These observations give us two design choices:

• conformance<T where T: Hashable> A<T>: Q {} implicitly acts as a source of conditional conformance for A<T>: P.
• conformance<T where T: Hashable> A<T>: Q {} only declares A<T>: Q and we're left to search for proof that A<T>: P also holds at use sites.

[Nobody1707]

The difference is that Swift treats the unconditional conformance of a protocol as a conformance to that protocol as well as all protocols the stated protocol refines. This is much easier to see when the protocols have requirements:

protocol P {
  func foo()
}

protocol Q: P {
  associatedtype Bar
  var bar: Bar { get }
}

struct Baz<T> { }

An unconditional conformance to P requires you to implement foo() or else it gives an error:

extension Baz: Q {
    typealias Bar = Void
    var bar: Bar { () }
}

error: type 'Baz<T>' does not conform to protocol 'P' protocol requires function 'foo()' with type '() -> ()'; add a stub for conformance

This is because the unconditional extension is actually just sugar for:

extension Baz: P, Q {
   ...
}

Whereas the conditional conformance:

extension Baz: Q where T: Hashable {
    typealias Bar = Void
    var bar: Bar { () }
}

Is properly:

extension Baz: Q where T: Hashable, Self: P {
    typealias Bar = Void
    var bar: Bar { () }
}

The unconditional conformance includes a promise that P will be implemented, while the conditional one has only a requirement that P was already implemented. This was largely an ease of use feature so that programmers didn't need to explicitely spell out that they were conforming to, for instance, both Collection and MutableCollection. The programmer could simply state that he was conforming to MutableCollection and the intent to implement Collection would be implied.