Need a way to require a particular capability to be in a capture set

[odersky]

Minimized example

The following attempt to link capabilities of Async contexts and sources fails.

import language.experimental.captureChecking
import caps.{Capability, CapSet}

trait Async:
  def await[T, Cap >: CapSet^{this} <: CapSet^](src: Source[T, Cap]^): T

trait Source[+T, Cap^]:
  final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this)```
    // error: Type argument Cap does not conform to lower bound caps.CapSet^{this}

The error makes sense. What we'd need to assert is that also Source.this is in the Cap^ parameter of Source. But we can't express this with a lower bound. This fails:

trait Source[+T, Cap >: CapSet^{this} <: CapSet^]: // error: illegal occurrence of Source.this

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:

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^}, _: caps.Contains[Cap, this]) = ac.await[T, Cap](this)```
    // error: Type argument Cap does not conform to lower bound caps.CapSet^{this}```

[Linyxus]

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?

[odersky]

@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)```

[Linyxus]

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?

[odersky]

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.

[odersky]

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.

[odersky]

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.

[Linyxus]

I agree, this looks good!