Defining and Transforming Capabilities from other Capabilities

[bracevac]

Compiler version

3.6-NIGHTLY

Minimized code

//> using scala 3.6.0-RC1-bin-20240918-be10596-NIGHTLY
//> using dep org.scala-lang::scala2-library-cc-tasty-experimental:3.6.0-RC1-bin-20240918-be10596-NIGHTLY
import language.experimental.captureChecking
import caps.Capability
import caps.unbox

trait File extends Capability
case class Logger(f: File^) extends Capability // <- will work if we remove the extends clause

def mkLoggers(@unbox files: List[File^]): List[Logger^] = files.map(Logger(_))

@main def run = () 

Output

-- [E007] Type Mismatch Error: -------------------------------------------------
1 |def mkloggzer(@unbox files: List[File^]): List[Logger^] = files.map(Logger(_))
  |                                                                    ^^^^^^^^^
  | Found:    (caps.Exists -> Logger){
  |   def apply(ex$13: caps.Exists): Logger^{ex$13}; val f: File^{_$1}}^{_$1}
  | Required: Logger{val f: File^?}^{_$1}
  |
  | Note that reference ex$13.type
  | cannot be included in outer capture set {_$1}
  |
  | longer explanation available when compiling with `-explain`
1 error found

Expectation

The example should compile. It compiles if we omit extends Capability for Logger, but I would expect that Logger should be tracked as a capability.

[odersky]

The issue is probably linked the expansion of case classes that extend Capability. It was not an explicit design goal that case classes should be able to extend Capability so this was not tried out yet,

[bracevac]

@odersky it also fails if we make Logger an ordinary class and create instances with new.

[odersky]

I verified that this version compiles:

import language.experimental.captureChecking
import caps.Capability
import caps.unbox

trait File extends Capability
class Logger(f: File^)   // <- will work if we remove the extends clause

def mkLoggers(@unbox files: List[File^]): List[Logger^] = files.map(new Logger(_))

Which variant did you have in mind?

[odersky]

Unrelated problem: This also fails.

def mkLoggers1[F <: File^](@unbox files: List[F]): List[Logger^] =
  files.map((f: F) => new Logger(f))

Here's the error trace:

sc i21614.scala -explain
-- [E007] Type Mismatch Error: i21614.scala:9:33 -------------------------------
9 |  files.map((f: F) => new Logger(f))
  |                                 ^
  |                                 Found:    (f : F^)
  |                                 Required: File^
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: f
  | I tried to show that
  |   (f : F^)
  | conforms to
  |   File^
  | but none of the attempts shown below succeeded:
  |
  |   ==> (f : F^)  <:  File^
  |     ==> F^  <:  File^
  |       ==> F  <:  File^
  |         ==> F  <:  File
  |           ==> box File^  <:  File
  |             ==> subcaptures {cap} <:< {} 
  |               ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |         ==> box File^  <:  File^
  |           ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |           ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |     ==> F  <:  File
  |       ==> box File^  <:  File
  |         ==> subcaptures {cap} <:< {} 
  |           ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |     ==> (f : F^)  <:  File
  |       ==> (box File^)^  <:  File
  |         ==> subcaptures {cap} <:< {} 
  |           ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |     ==> F^{f}  <:  File^
  |       ==> F  <:  File^
  |         ==> F  <:  File
  |           ==> box File^  <:  File
  |             ==> subcaptures {cap} <:< {} 
  |               ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |         ==> box File^  <:  File^
  |           ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |           ==> {} accountsFor (caps.cap : caps.Capability), which has capture set {cap}  = false
  |

It has to do with boxing. Somehow we don't realize that if F <: File^ then F
conforms to File^. I guess because it's really F <: Box File^. But we should be able to box adapt in this case. @Linyxus WDYT?

[Linyxus]

I suspect this is a known issue #19076.

[Linyxus]

Basically, to correctly handle these cases it seems necessary to interleave subtyping and box adaptation. I remember Yaoyu @noti0na1 once had a look at this issue.

[bracevac]

I verified that this version compiles:

import language.experimental.captureChecking
import caps.Capability
import caps.unbox

trait File extends Capability
class Logger(f: File^)   // <- will work if we remove the extends clause

def mkLoggers(@unbox files: List[File^]): List[Logger^] = files.map(new Logger(_))

Which variant did you have in mind?

It fails again when inheriting from Capability:

class Logger(f: File^) extends Capability

So I'm not sure if the issue is tied to case classes specifically.

[odersky]

Yes, my failure is a duplicate of #19076. Something we need to fix, but it does not look easy.

About Capability classes; the problem arises since creating an instance of a Capabaility class always adds cap (unless an explicit capture set is given). So we try to box a Logger^ in map, which fails.

I'll add it as a test case so we can maybe track better error messages in the future.