Refine withReachCaptures

[Linyxus]

Follow-up of this comment.

Previously, we avoid refining co-variant caps to reach capabilities as long as there exist contra-variant caps. This limits expressivity. One counter-example is church-encodings: types like [R] -> (op: (IO^, IO^) => R) -> R cannot be refined, since the parameter op has a covariant cap.

This PR refines the treatment: only when a contra-variant cap is possibly reached by a co-variant cap do we refuse the refinement. Examples:

• The co-variant cap in (c: IO^{cap}) -> IO^{cap} cannot be refined, as it could refer to the impure contra-variant parameter c.
• p : [R] -> (op: (IO^{cap}, IO^{cap}) => R) -> R can be safely refined to [R] -> (op: (IO^{p*}, IO^{p*}) => R) -> R, as op is not possibly reached from the two co-variant caps.

[odersky]

What is the status of this wrt soundness?

[Linyxus]

I found a deeper unsoundness issue of this approach.

To recap, the underlying principle of this approach is to refine co-variant caps to both the reach capability and deeply-impure contra-variant dependent parameters in scope. For instance,

f : (x: Box[IO^]) -> Box[IO^]

should be refined to

f : (x: Box[IO^]) -> Box[IO^{f*, x*}]

In practice, augmenting the capture set with reachable parameters (like x* here) might be over-complicated. So, in the implementation we do not refine a cap if there is any impure dependent parameter in scope. So in this example, f will not be refined.

Similarly, the following function will not be refined either:

f : (x: Box[IO^]) -> [R] -> (op: Box[IO^] => R) -> R

Since based on the underlying principle, it should be refined to the complex form

f : (x: Box[IO^]) -> [R] -> (op: Box[IO^{f*, x*}] => R) -> R

But such a scheme falls apart quickly, for instance, just swapping the order of the first three arguments, the function is refined by our scheme:

g : [R] -> (op: Box[IO^] => R) -> (x: Box[IO^]) -> R

gets refined to

g : [R] -> (op: Box[IO^{g*}] => R) -> (x: Box[IO^]) -> R

We assume that x, an argument introduced after op, cannot possibly flow into the first cap. This is false:

val g = [R] => op => x => op(x)

If we were to refine g, we would get the following unsound code:

val g = [R] => op => x => op(x)
withIO: localIO =>
  val g1 : [R] -> (op: Box[IO^{g*}] => R) -> (x: Box[IO^]) -> R = g
  val g2 : (op: Box[IO^{g*}] => Box[IO^{g*]]) -> (x: Box[IO^]) -> Box[IO^{g*}] = g1[Box[IO^{g*}]]
  val bad : Box[IO^{g*}] = g2(x => x)(localIO)
  bad  // leaked

Essentially, in the scheme in this PR, when we see a cap at a covariant position in a function:

f : (x1: T1) -> (x2: T2) -> ... -> (xk: Tk) -> (xs: List[IO^{cap}]) -> U

we assume that cap indicates something reachable from f* and from x1 ... xk. But this is false: cap could well indicate capabilities flowing into the closure in U.

There is no easy way to patch this scheme. Ideally we should refine g as:

g : [R] -> (op: Box[IO^{g*, x*}] => R) -> (x: Box[IO^]) -> R

but this is ill-formed: we cannot name x in op.

[Linyxus]

Turns out to be unsound. Closed.