This proposal is to add the capability for an interface to require other types
to be implemented, not just the Self
type. The interface-implemented
requirement feature also has some concerns:
- If the interface requirement has a
where
clause, there are concerns about being able to locally check whether impls satisfy that requirement. - A function trying to make use of the fact that a type implements an interface due to an interface requirement, or a blanket impl, may require the compiler perform a search that we don't know will be bounded.
The first version of interface-implemented requirements for interfaces was introduced in proposal #553: Generics details part 1.
This proposal adds two sections to the generics details design document:
This proposal advances these goals of Carbon:
- Language tools and ecosystem:
The motivation for this expressive power of interface requirements comes
from discussions about how to achieve symmetric behavior with interfaces
like
CommonTypeWith
from proposal #911: Conditional expressions. - Fast and scalable development:
The requirement that the source provide the proof of any facts that would
require a recursive search using
observe
declarations means that the expense of that search is avoided except in the case where there is a compiler error. If the search is successful, the results of the search can be copied into the source, and afterward the search need not be repeated.
We could allow
requirements with where
constraints
to be satisfied by implementations that could be specialized, as long as the
constraints were still satisfied. Unfortunately, this is not a condition that
can be checked locally. Continuing the example from that section, consider four
packages
-
A package defining the two interfaces
package Interfaces api; interface A(T:! Type) { let Result:! Type; } interface B(T:! Type) { impl as A(T) where .Result == i32; }
-
A package defining a type that is used as a parameter to interfaces
A
andB
in blanket impls:package Param api; import Interfaces; class P {} external impl [T:! Type] T as Interfaces.A(P) where .Result = i32 { } // Question:Is this blanket impl of `Interfaces.A(P)` sufficient // to allow us to make this blanket impl of `Interfaces.B(P)`? external impl [T:! Type] T as Interfaces.B(P) { }
-
A package defining a type that implements the interface
A
with a wildcard impl:package Class api; import Interfaces; class C {} external impl [T:! Type] C as Interfaces.A(T) where .Result = bool { }
-
And a package that tries to use the above packages together:
package Main; import Interfaces; import Param; import Class; fn F[V:! Interfaces.B(Param.P)](x: V); fn Run() { var c: Class.C = {}; // Does Class.C implement Interfaces.B(Param.P)? F(c); }
Package Param
has an implementation of Interfaces.B(Param.P)
for any T
,
which should include T == Class.C
. The requirement in Interfaces.B
in this
case is that T == Class.C
must implement Interfaces.A(Param.P)
, which it
does, and Class.C.(Interfaces.A(Param.P).Result)
must be i32
. This would
hold using the blanket implementation defined in Param
, but the wildcard impl
defined in package Class
has higher priority and sets the associated type
.Result
to bool
instead.
The conclusion is that this problem would only be detected during
monomorphization, and could cause independent libraries to be incompatible with
each other even when they work separately. These were significant enough
downsides that we wanted to see if we could live with the restrictions that
allowed local checking first. We don't know if developers will want to declare
their parameterized implementations final
in this situation anyway, even with
the limitations on final
.
This problem was discussed in the #generics channel on Discord.
We could require the Carbon compiler to do a search to discover all interfaces that are transitively implied from knowing that a type implements a set of interfaces. However, we don't have a good way of bounding the depth of that search.
In fact, this search combined with conditional conformance makes the question "is this interface implemented for this type" undecidable in Rust. Note: it is possible that the acyclic rule would avoid this problem in Carbon for blanket impls, but it doesn't apply to interface requirements.
This problem was observed in a discussion in #typesystem on Discord.