A more flexible scheme for handling the universal capability

[odersky]

• Start with sealed type parameters, extended so that class parameters can also be sealed.
• Tighten the rules so that type parameter arguments for sealed type parameters must themselves be sealed, except if the argument is from some outer scope.
• Introduce a coercion that maps a universal capture set to a local root that is enclosed by the owners of all free variables of the coerced expression.

Supersedes #18566

[odersky]

@Linyxus I am going to merge now, so that we have a stable state for IWACO. When you have time, it would still be good to do a post-merge review.

[Linyxus]

I'm testing the new scheme and found the following won't compile:

import language.experimental.captureChecking
trait Cap:
  def use: Int = 42

def test2(cs: List[Cap^]): Unit =
  val t0: Cap^{cap[test2]} = cs.head  // error
  var t1: Cap^{cap[test2]} = cs.head  // error

[odersky]

Would be good to try some variants. Does it infer the right type if the type is not given?

[Linyxus]

Without a type being given, the inferred type is Cap^.

[odersky]

For the var as well?

[Linyxus]

It behaves differently but fails either: it creates a capture set variable on LHS, but since RHS is Cap^, capture set inference complains we are pushing a cap into the capture set of a variable.

[Linyxus]

I investigated into what happened. It turns out that when the input to adaptUniversal is a TermRef, for instance, cs.head : -> box Cap^, it get adapted into something like box (cs.head : -> box Cap^)^{cap[test2]}.

[odersky]

And why does that lead to a problem? It looks like we do adapt to capture set {cap[test2]}?

[Linyxus]

It seems that tp.widenDealias turns box (cs.head : -> box Cap^)^{cap[test2]} to box Cap^. .widenDealiased is called by adaptBoxed.

Besides, nested capture set annotations accumulate. So the effective boxed capture set of box (cs.head : -> box Cap^)^{cap[test2]} is {cap, cap[test2]}, which is equivalent to {cap} modulo subcapturing.

[odersky]

Yes, I guess here they should not accumulate. In fact I am not even sure that accumulation is correct in general. I think adaptBoxed should be changed to avoid widenDealias.

[odersky]

Or else do the widenDealias eagerly in adaptUniversal where we then strip the universal capture set .

[Linyxus]

I constructed an unsound code snippet with recursion:

import language.experimental.captureChecking
trait Cap:
  def use: Int = 42

def usingCap[sealed T](op: Cap^ => T): T = ???

def badTest(): Unit =
  def bad(b: Boolean)(c: Cap^): Cap^{cap[bad]} =
    if b then c
    else
      val leaked = usingCap[Cap^{cap[bad]}](bad(true))
      leaked.use  // boom
      c

  usingCap[Unit]: c0 =>
    bad(false)(c0)

The setup is classic. We have Cap, a capability, and usingCap, which creates a temporary local capability that has to be used within a scope.

The function bad manifests the problem. It takes a boolean and a capability. Depending on the boolean value it has two cases:

• When b is true bad is just an identity. Note that the identity coerces the input capability onto the level of bad, as seen in the return type.
• Otherwise, it calls usingCap with itself, setting b to true. Note that bad(true) is just an identity. It returns the capability on the level of bad, which is perfectly valid and usable in the current scope. However, it is actually a leaked capability and using it causes undefined behaviors.

Remarks:

• I think the essence of the problem is that the meaning of scoping enforced by levels becomes vague when recursion comes into play.
• This is a soundness hole, but seems to be a weird and rare case that is merely possible to be written by an actual user.
• Does that rings a bell on the necessity of taking recursion into account in the formalism?

[odersky]

Can you translate the program to explicit levels? Does it typecheck then? Where would it go wrong?

[Linyxus]

At first glance with explicit levels that will not be a issue thanks to the polymorphism trick, but I'll verify.

[odersky]

I think one solution would be that we don't let the local root of a method appear in the external type of that method. So the following line would be in error:

def bad(b: Boolean)(c: Cap^): Cap^{cap[bad]} =

[odersky]

See 1065bd1 which fixes the problem and still allows the standard library to compile. It would be good if you could refine that further. (see commit message)

[Linyxus]

cool! Thanks. I'll look into it.

[Linyxus]

I looked into the commit and find it working in most cases I could come up with. Then I compared it with checkNoPrivateLeaks in Checking.scala which I believe checks the leaking of private types in class interfaces, but I could not figure out what is missing in the current commit. I wonder what specifically should be refined?

[odersky]

I think this should be rejected:

class C:
  object inner:
    val x: T^{cap[C]}  // error

But this should be OK:

class C:
  private object inner:
    val x: T^{cap[C]}  // ok

AFAICR that seems similar to what checkNoPrivate leaks does.