Capability class is not properly boxed in implicit type argument

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking

@annotation.capability
class CanIO

def allowIO[T](op: (c: CanIO) => T): T = ???

def bad(c: CanIO): CanIO = c

def test: Unit = {
  val ok = allowIO(bad) // error
  val boom = allowIO[CanIO](bad)  // should be an error, too
}

Output

-- [E007] Type Mismatch Error: issues/capclass.scala:30:19 ---------------------------------------------------------------------------------------------------------------------------------------------
30 |  val ok = allowIO(bad) // error
   |                   ^^^
   |                   Found:    ? CanIO -> {*} CanIO
   |                   Required: (c: CanIO) => box {*} CanIO
   |
   | longer explanation available when compiling with `-explain`
1 error found

Expectation

Both ok and boom should issue an error, but now boom won't b/c of the explicit type argument. This is because in Setup the type arugment CanIO in allowIO[CanIO] will not be boxed when it is written out explicitly.

[noti0na1]

I think this issue can be closed now since both variables cause errors as expected.

[Linyxus]

Yes you are right. The issue is not longer reproducible due to the change in the way we guard scoped capability (previously, it depends on the boxes but now there is a no-covariant-cap check on type arguments).

But the root cause of this issue (that in some cases capability classes are not recognised as impure and therefore not properly boxed) is not fixed. So it is still causing other soundness problems, like the following variant of this issue:

import language.experimental.captureChecking
@annotation.capability
class IO:
  def brewCoffee(): Unit = ???
def usingIO[T](op: IO => T): T = ???

type Wrapper[T] = [R] -> (f: T => R) -> R
def mk[T](x: T): Wrapper[T] = [R] => f => f(x)
def useWrappedIO(wrapper: Wrapper[IO]): () -> Unit =
  () =>
    wrapper: io =>
      io.brewCoffee()
def main(): Unit =
  val escaped = usingIO(io => useWrappedIO(mk(io)))
  escaped()  // boom

With a combination of mk and useWrappedIO we successfully trick the capture checker into believing that a closure that makes use of a capability is pure.

[Linyxus]

I checked the issue again and it turns out that actually the recent reproduction is completely a new one with a different cause. Another minimisation that is more salient:

def runOps(ops: List[() => Unit]): () -> Unit =
  () =>
    ops.foreach: op =>
      op()