Can we make capture checking use less global inference?

[odersky]

The capture checker employs a global type inference scheme using a propagation constraint solver. Capture sets are constrained by subcapturing constraints or are defined as results of type maps of other capture sets. This can lead to long chains of maps that are hard to debug and that make formulation of capture checking algorithms more difficult.

Can we use a more local scheme where we "solve" constraints of capture sets for each inferred result type? That would largely avoid the need for stored type maps. But it would work only if we can compute the type of each definition only from its local scope. The following example shows that this is not always possible:

case class Box[T](x: T)
def test(io: Object^): Unit =
  def foo(): Unit = bar()
  def bar(): Unit =
    val x = () =>
      foo()
    val y = Box(io)
    println(y.x)

If we print this with -Xprint:cc, we get:

def test(io: Object^): Unit =
      {
        def foo(): Unit = bar()
        def bar(): Unit =
          {
            val x: () ->{io} Unit = () => foo()
            val y: Box[box Object^{io}]^? = Box.apply[box Object^{io}](io)
            println(y.x)
          }
        ()
      }

The interesting bit is the type of x. How did the checker find out it captures io? Here's how:

• x's right hand side calls foo, so the capture set of the closure includes the use set of foo.
• foo calls bar so the use set of foo includes the use set of bar.
• io is used as an argument to Box in bar but this is in boxed form, so this does not contribute to the use set of bar.
• The inferred type of y ends up to be Box[box Object^{io}].
• bar unboxes y.x of type y* in the final println.
• This means we charge the deep capture set of y's type to the use set of bar.
• The deep capture set is {io}, so that set ends up as the use set of bar and foo and as the capture set of the type of x.

This means that to compute the type of x we have to know the use sets of foo and bar, which means we have to also analyze the rest of bar after the definition of x. What's more, this computation involves the full
capture checking machinery including reach captures and their underlying deep capture sets. So there does not seem to be an easy way to have a simpler use set computation followed by local capture set inference.

On the other hand, maybe we could use a standard fixed point iteration approach:

• Keep track of which definitions are currently traversed.
• When including call captures, compute the use set of the callee before proceeding, providing the callee is not currently analyzed.
• If the callee is currently analyzed we have a cycle like the one in the example. Pick the current use set of the callee and mark that set as "observed".
• If an observed use set acquires new elements, set a flag that capture set inference needs to be repeated.
• If at the end of the inference the flag is set, we do a new iteration, with the use sets computed so far.

In the example above, this would lead to the following steps:

• When capture-checking foo, we need the use set of bar, so we capture-check bar.
• When capture checking bar, we need to check the RHS of x, which means we need the use set of foo.
• Since foo is currently checked, we assume its use set is as computed so far, i..e. it is empty, and we mark it as observed.
• This gives the wrong type () -> Unit for x.
• We complete checking of bar which gives a use set of {io}.
• We complete checking of foo which gives again a use set of {io}. We remark that this use set has changed after it was observed.
• We restart the whole capture checking of test with use sets of {io} for bar and foo.

I believe cycles will be quite rare, so computationally this might be a win.

[odersky]

There seems to be wrong behavior even with the current scheme. Here is a variant of the example:

class Box[T](x: T):
  def m: T = ???
def test(io: Object^): Unit =
  def foo(): Unit = bar()
  def bar(): Unit =
    val x = () =>
      foo()
    val y = Box(io)
    println(y.m)
    val _: () -> Unit = x // error

We get an error on the last line, as expected:

10 |    val _: () -> Unit = x // error
   |                        ^
   |                        Found:    (x : () ->{io} Unit)
   |                        Required: () -> Unit
   |

But if we duplicate the last line and place a copy of it earlier, it compiles without errors

class Box[T](x: T):
  def m: T = ???
def test(io: Object^): Unit =
  def foo(): Unit = bar()
  def bar(): Unit =
    val x = () =>
      foo()
    val _: () -> Unit = x // no error!
    val y = Box(io)
    println(y.m)
    val _: () -> Unit = x // no error!

[odersky]

In fact, computing use sets eagerly with cycle detection can collide with the lazy evaluation of types. E.g.

def foo() = bar()
def bar(): Int = foo()

If we analyze the body of foo, and, getting to the bar() call, switch from rechecking foo to rechecking bar to get its use set, we then need to get the return type of foo() to compare it with the return type of bar(). But the return type of foo is not computed yet, so our analysis would have to be aborted.

An alternative scheme could be:

• We use the same order of evaluation as in the current system with global type inference.
• When computing the full inferred type of a val or def, we solve all capture set variables that come up. Solving means marking these sets as constant.
• If we add an element to a use set we also add the element to all supersets. This can lead to a conflict if a superset is a solved set that does not already contain the element. Normally, we would fail in this case and report an error. But in the new scheme, we do not fail and still add the element to the use set, but also set the flag that capture checking needs to be repeated.

[odersky]

The issue with the scheme in the previous comments is that use sets also appear in other contexts. For instance, the use set of a class is also included in capture set of the type of this in the class. So these might still need to be mapped, or we need to find a good point where these use sets are frozen.

In a sense the best scheme is to be more lazy. Maybe still keep solving capture sets of vals or defs (but we could also drop this part). But otherwise we solve a capture set variable at the moment we apply a map to it. So we never have Mapped or BiMapped sets. We mark these sets as provisionally solved with the id of the current capture checking iteration. Then, if a new element is added to a use set and its propagation fails because a new element needs to be added to a provisionally solved set, we add the original element to the use set anyway, but schedule a new recheck iteration. The new iteration gets a higher id than the previous one, so we can treat previously solved capture sets as open again by comparing ids.

If a subcapturing comparison for some other set fails for the same reason, we probably should fail with an internal error to figure out why this happens.

[odersky]

This is addressed in #22910. We now drop regular maps (these evaluate capture set elements into constants) and fuse chains of BiTypeMaps into a single map.