Leaking capability in Scott-encoded wrapper

[Linyxus]

Compiler version

cc-experiment branch

Minimized code

trait Cap { def use(): Int }
type Id[X] = [T] -> (op: X => T) -> T
def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)

def bar() = {
  def withCap[X](op: ({*} Cap) => X): X = {
    val cap: {*} Cap = new Cap { def use() = { println("cap is used"); 0 } }
    val result = op(cap)
    result
  }

  val leak = withCap(cap => mkId(cap))
  leak { cap => cap.use() }   // bad
}

Output

It compiles.

Expectation

It should not compile. We expect the type of val leak to be Id[□ {*} Cap], so it will expect a function of (□ {*} Cap) => Unit in leak(...). It will not be possible to adapt cap => cap.use() : ({*} Cap) -> Unit to the type (□ {*} Cap) => Unit since the adaption cap => (unbox cap).use() tries to unbox a reference capturing universal capability.

We should issue an error on leak(...).

[Linyxus]

Note: the following code using a case class fails the compilation, as expected:

trait Cap { def use(): Int }
case class Id[X](x: X) {
  def apply[T](op: X => T): T = op(x)
}
def mkId[X](x: X): Id[X] = Id(x)

def bar() = {
  def withCap[X](op: ({*} Cap) => X): X = {
    val cap: {*} Cap = new Cap { def use() = { println("cap is used"); 0 } }
    val result = op(cap)
    result
  }

  val leak = withCap(cap => mkId(cap))
  leak { c => c.use() }
}

[odersky]

Until recently, this used to give an error at the expected line leak { cap => cap.use() }, which is a bit strange since the original fix was to box some arguments and boxing no longer works with type aliases such as Id.

With #23171 that error is gone. I tried to make a class based version that re-introduces boxing and that would hopefully give an error again:

trait Cap { def use(): Int }
class Id[X](val value: [T] -> (op: X => T) -> T)
def mkId[X](x: X): Id[X] = Id([T] => (op: X => T) => op(x))

def bar() = {
  def withCap[X](op: (lcap: caps.Capability) ?-> Cap^{lcap} => X): X = {
    val cap: Cap = new Cap { def use() = { println("cap is used"); 0 } }
    val result = op(using caps.cap)(cap)
    result
  }

  val leak = withCap(cap => mkId(cap))
}

That gives a crash due to a stack-overflow. The stacktrace seems to indicate a cycle in capture set propagation. That crash is present already in main.

The original and class based versions are in #23171 as tests/pending/neg-custom-args/captures/i15938.scala and i15938a.scala.