Unsoundness in CC with global objects and separate compilation

[Linyxus]

Compiler version

main

Minimized code

File 1:

import language.experimental.captureChecking
import caps.*
class IO extends SharedCapability:
  def println(msg: String): Unit = ()
val io: IO = new IO
def assertPure(op: () -> Unit): Unit = ()

File 2:

import language.experimental.captureChecking
import caps.*
def test1(): Unit =
  assertPure(() => io.println("hello"))  // error, as expected
def test2(): Unit =
  def test(): Unit = io.println("hello")
  assertPure: () =>  // should be error, but ok
    test()

Output

Only one error in test1.

Expectation

Both should be error.

Note that this is only triggered when the code is separate in two files. When test2 is in the same file with io, the error shows up as expected.

[Linyxus]

cc @odersky

[noti0na1]

The bug may be related to top-level definitions in package objects? If io is wrap inside an object, we will get expected errors.

[odersky]

I suspect we get the errors alsoi if both classes are in the same named package. There's an exception that classes in the empty package do not need explicit use clauses (since that would invalidate 100s of tests and generally make quick experimentation a pain).

[odersky]

Indeed, if I put both files in a test package I get:

-- Error: IO.scala:5:4 ---------------------------------------------------------
5 |val io: IO = new IO
  |    ^
  |a field `io` with `any` in its type need to be put in an object that extends Capability
-- [E223] CaptureChecking Error: Test.scala:4:19 -------------------------------
4 |  assertPure(() => io.println("hello"))  // error, as expected
  |                   ^^
  |Reference `test.io` is not included in the allowed capture set {}
  |of the enclosing top-level definitions in package test.
  |
  |The top-level definitions should be wrapped in an object with a uses clause:
  |
  |    uses test.io
-- [E223] CaptureChecking Error: Test.scala:6:21 -------------------------------
6 |  def test(): Unit = io.println("hello")
  |                     ^^
  |Reference `test.io` is not included in the allowed capture set {}
  |of the enclosing top-level definitions in package test.
  |
  |The top-level definitions should be wrapped in an object with a uses clause:
  |
  |    uses test.io
3 errors found

[odersky]

You see how annoying these kinds of errors would be if IO.scala was just a stand-alone test?

[odersky]

The question is what to do here. Maybe we can restrict safe code to always be in a named package. @noti0na1 would that work for Tacit?

[noti0na1]

The question is what to do here. Maybe we can restrict safe code to always be in a named package. @noti0na1 would that work for Tacit?

I think this is ok for tacit. tacit uses repl driver, and every code is already wrapped inside a special repl object.

[odersky]

I think this is ok for tacit. tacit uses repl driver, and every code is already wrapped inside a special repl object.

But we'd need to wrap it in a package, not an object. I don't think object would help.

Here's a version that wraps IO in an object:

import caps.*
object o:
  class IO extends SharedCapability:
    def println(msg: String): Unit = ()
  val io: IO = new IO
  def assertPure(op: () -> Unit): Unit = ()

///////////////

import caps.*
import o.*
def test1(): Unit =
  assertPure(() => io.println("hello"))  // error, as expected
def test2(): Unit =
  def test(): Unit = io.println("hello")
  assertPure: () =>  // should be error, but ok
    test()

That only has one error not the expected two errors.