Skip to content

Wanted: A way to declare fields with fresh captures to be contained #24137

@odersky

Description

@odersky

Compiler version

3.8.0

Minimized example

import caps.{cap, Shared, SharedCapability}

open class A

class B(elem1: A^{cap.only[Shared]}, elem2: A^{cap.only[Shared]}):
  private var curElem: A^ = elem1 // problem is curElem contibutes cap to B().
  def next() =
    curElem = elem2

class Async extends caps.SharedCapability

def test(async: Async) =
  val a: A^{async} = A()
  val b = B(a, a)
  val _: B^{async} = b  // error, but could be OK if we have a way to mark
                        // curElem above as not contributing anything
  val b1: B^{async} = B(a, a)

Output

In PR #24136 with -Ycc-verbose:

-- Info: test.scala:14:6 -------------------------------------------------------
14 |  val b = B(a, a)
   |      ^
   |Note: instance of class B captures a <fresh in val b hiding 's1> that comes from a field
   |Note: variable curElem in class B captures a <fresh in val curElem hiding '{B.this.elem1, B.this.elem2}>
-- [E007] Type Mismatch Error: test.scala:15:21 --------------------------------
15 |  val _: B^{async} = b  // error, but could be OK if we have a way to mark
   |                     ^
   |        Found:    (b : B{val elem1: A^{a}; val elem2: A^{a}}^{cap, a})
   |        Required: B^{async}
   |
   |        Note that capability cap is not included in capture set {async}.
   |
   |        where:    cap is a fresh root capability in the type of value b
   |
   | longer explanation available when compiling with `-explain`
-- Info: test.scala:17:6 -------------------------------------------------------
17 |  val b1: B^{async} = B(a, a)
   |      ^
   |Note: instance of class B captures a <fresh in val b1 hiding 's2> that comes from a field
-- [E007] Type Mismatch Error: test.scala:17:23 --------------------------------
17 |  val b1: B^{async} = B(a, a)
   |                      ^^^^^^^
   |Found:    B{val elem1: (a : A^{async}); val elem2: (a : A^{async})}^{cap, a}
   |Required: B^{async}
   |
   |Note that capability cap is not included in capture set {async}.
   |
   |where:    cap is a fresh root capability created in value b1 when constructing instance B
   |
   | longer explanation available when compiling with `-explain`
2 errors found

Expectation

The system now adds a ^ to every B(...) instance because B contains variable curElem which captures ^. We can make the code pass by annotating curElem with caps.unsafe.untrackedCaptures. It would be nice to have a safe analogue of this annotation. In the example above we can argue that even though curElem's declared type captures ^, every value assigned to it does not capture a fresh cap. So the ^ in curElem acts as an upper bound of a set of concrete capabilties. This means it need not contribute a fresh cap to B(...).

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