Closed odersky closed 1 day ago
I couldn't see the reason why the Cap of Source has to contain Source.this. Async.await requires its capture argument at least contains Async.this, which is async.this in this case. Given that we have async: Async^{Cap^}, ideally we should be able to show that Async.this <: {Cap^}, and thus pass the subtype check?
@Linyxus In fact yes, the error message is misleading.
// error: Type argument Cap does not conform to lower bound caps.CapSet^{this}
should be
// error: Type argument Cap does not conform to lower bound caps.CapSet^{ac}
I believe a substitution or asSeenFrom was not done correctly here in the annotation at Typer, which is when the error was issued.
But the problem remains: we can't assure the lower bound in Source
.
The variant with Contains
should read.
trait Async:
def await[T, Cap^](using caps.Contains[Cap, this])(src: Source[T, Cap]^): T
trait Source[+T, Cap^]:
final def await(using ac: Async^{Cap^})(using caps.Contains[Cap, ac]) = ac.await[T, Cap](this)```
I believe by Contains[Cap, ac] we are asking for the constraint {ac} <: {Cap^}. But, given that ac: Async^{Cap^}, wouldn't {ac} <: {Cap^} already hold?
I believe by Contains[Cap, ac] we are asking for the constraint {ac} <: {Cap^}. But, given that ac: Async^{Cap^}, wouldn't {ac} <: {Cap^} already hold?
Good point. We need to verify that. But the original problem is elsewhere. We can't have a lower bound CapSet^{this}
in Async.await
because that bound cannot be satisfied in Source
. That's a test done before capture checking. So I believe we still might want to use Contains
but only in Async
:
trait Async:
def await[T, Cap^](using caps.Contains[Cap, this])(src: Source[T, Cap]^): T
trait Source[+T, Cap^]:
final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
With Self
based type classes we could use a context bound for Contains
:
trait Async:
def await[T, Cap^: Contains[this]])(src: Source[T, Cap]^): T
Then it looks nicer.
The idea for Contains
is simple. We can put a definition in caps like so:
given Contains[C <: CapSet^, R <: Singleton]()
So Contains
instances are always available for typer. Then during capture checking, when we see an argument of type
Contains[Cs, ref.type]
check that {ref}
subcaptures Cs
.
I agree, this looks good!
Fixed by #21361
Minimized example
The following attempt to link capabilities of Async contexts and sources fails.
The error makes sense. What we'd need to assert is that also
Source.this
is in theCap^
parameter ofSource
. But we can't express this with a lower bound. This fails:Indeed the
this
of a class cannot be used in the bounds of the class parameters.I believe we should look for a different way to express this. Maybe a magic type class,
caps.Contains
? Something along the lines of: