Skip to content

Capture checking's rd break tracked val's refinements #25251

@natsukagami

Description

@natsukagami

Compiler version

Latest main (71bfc7c)

Minimized code

import language.experimental.captureChecking
import language.experimental.modularity
import caps.*

trait Collection[+T] extends Stateful:
  self: Collection[T]^ =>
    type Index

    // slice should have its Index type member a subtype of the Collection's Index
    def getSlice(): (Collection[T] { type Index <: self.Index })^{this.rd} = new Slice(this)

class Slice[+T](tracked val coll: Collection[T]) extends Collection[T]:
  type Index = coll.Index

Output

-- [E007] Type Mismatch Error: a.scala:10:77 -----------------------------------
10 |    def getSlice(): (Collection[T] { type Index <: self.Index })^{this.rd} = new Slice(this)
   |                                                                             ^^^^^^^^^^^^^^^
   |Found:    Slice[T^'s1]{
   |  val coll: Collection[T]^{Collection.this.rd};
   |    val coll: Collection[T]^{Collection.this.rd}
   |}^{Collection.this.rd}
   |Required: Collection[T]{type Index <: Collection.this.Index}^{Collection.this.rd}
   |
   |Note that {Collection.this} is an exclusive capture set of the stateful type (Collection.this : Collection[T]^),
   |it cannot subsume a read-only capture set of the stateful type Collection[T]^{Collection.this.rd}.
   |
   |Note that capability `Collection.this.rd` cannot flow into capture set {}.
   |
   |where:    ^ refers to the root capability caps.any
   |
   | longer explanation available when compiling with `-explain`

Expectation

The code compiles if capture checking is turned off and capture sets removed.
The code compiles if getSlice() is update and captures this, and slice takes a Collection[T]^:

trait Collection[+T] extends Stateful:
  self: Collection[T]^ =>
    type Index

    // slice should have its Index type member a subtype of the Collection's Index
    update def getSlice(): (Collection[T] { type Index <: self.Index })^{this} = new Slice(this)

class Slice[+T](tracked val coll: Collection[T]^) extends Collection[T]:
  type Index = coll.Index

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions