Right, we only have compiler-automated picking today, but we ought to also have a mechanism by which a conformance could be specified directly. This is why we have a lot of the paranoid restrictions around conformances today, like "no overlapping conformances", "no private conformances", and so on, because they would make it easier to end up in a situation where the compiler can't make a consistent automated choice, and we'd need "named" conformances or something to let source code direct it.
Overlapping conformances might get you somewhat closer to what you're looking for, since it would let you describe different conformances for different constraints:
protocol P {
static var isEquatable: Bool { get }
}
extension P {
static var isEquatable: Bool { false }
}
extension P where Self : Equatable {
static var isEquatable: Bool { true }
}
// strawman syntax `named <identifier>` to name a conformance
extension Array: P named AnyArrayP {}
extension Array: P named EquatableArrayP where Element: Equatable {}
func foo<T: P>(x: T) { print(x.isEquatable) }
// strawman syntax `using <identifier>` to pick a specific conformance
foo(x: [1, 2, 3] using AnyArrayP) // prints false
foo(x: [1, 2, 3] using EquatableArrayP) // prints true
but that still has the issue where, in a generic context where you have a T without an Equatable constraint, you could only pick the AnyArrayP conformance.
Given a conformance, the set of witnesses it uses is the same across all generic arguments. We effectively look up the witnesses in the context of the place where the X: P conformance is declared, based on its set of generic constraints. We only generate witness tables to instantiate different associated types, or to handle protocol resilience when an ABI-stable library introduces new protocol requirements with default implementations that need to be injected into existing binaries.
The main problem with "looking it up" is that there isn't a good way to guarantee a good answer because of the possibility of multiple conformances, and the ability for dynamic code loading to change the behavior of lookup at runtime. All of our generics features thus far avoid depending on global lookup.
One possibility might be to add formal optional constraints to the language, so that you can write P as:
protocol P where Self ?: Equatable { ... }
This would give the type system enough information to try to collect an Equatable conformance up front when forming a P conformance, and plumb that information through witness table instantiation so that we know it's dependent on Equatable conformance.
As far as #2 goes, I think the design of traits and type classes in Rust, Haskell, and other languages would be informative. In those languages, default implementations are explicitly declared as such, and protocol conformances are established in dedicated declarations. This makes it possible to diagnose up front when declarations fail to fulfill their roles. We've been using warnings to softly nudge users in the direction of using one-extension-per-conformance, which gives better near-miss diagnostics, but we don't currently really have a good way of guaranteeing good diagnostics in the face of potentially surprising behavior.