Explain read-only consumes

 - New section in separation checking doc page
 - Slight generalization of expectsReadOnly
 - Lots of tests variations of #24373

Author: odersky

compiler/src/dotty/tools/dotc/cc/Mutability.scala

@@ -105,7 +105,9 @@ object Mutability:
     def expectsReadOnly(using Context): Boolean = tp match
       case tp: PathSelectionProto =>
         tp.selector.isReadOnlyMember || tp.selector.isMutableVar && tp.pt != LhsProto
-      case _ => tp.isValueType && !tp.isMutableType
+      case _ =>
+        tp.isValueType
+        && (!tp.isMutableType || tp.captureSet.mutability == CaptureSet.Mutability.Reader)
 
   extension (cs: CaptureSet)
     private def exclusivity(tp: Type)(using Context): Exclusivity =
@@ -118,11 +120,12 @@ object Mutability:
      *    - the expected type is a value type that is not a mutable type,
      *    - the expected type is a read-only selection
      */
-    def adjustReadOnly(pt: Type)(using Context): Capability =
+    def adjustReadOnly(pt: Type)(using Context): Capability = {
       if ref.derivesFromMutable
           && (pt.expectsReadOnly || ref.exclusivityInContext != Exclusivity.OK)
       then ref.readOnly
       else ref
+    }.showing(i"Adjust RO $ref vs $pt = $result", capt)
 
   /** Check that we can call an update method of `qualType` or perform an assignment
    *  of a field of `qualType`.

docs/_docs/reference/experimental/capture-checking/separation-checking.md

@@ -188,6 +188,38 @@ def linearAdd[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
 ```
 `linearAdd` returns a fresh buffer resulting from appending `elem` to `buf`. It overwrites `buf`, but that's OK since the `consume` modifier on `buf` ensures that the argument is not used after the call.
 
+### Consume Parameters and Read Accesses
+
+A good way to conceptualize consume is to that it reserves the passed capability beyond the call with the consume parameter. In the previous `Buffer` example, if we do
+```scala
+  val buf1 = linearAdd(buf, elem)
+```
+then the exclusive `buf` capability is reserved and therefore no further accesses to `buf` are possible. This means that `linearAdd` can safely overwrite `buf` by appending `elem` to it.
+
+By the same token, when we pass a read-only capability to a consume parameter, it is
+only this capability that is reserved beyond the call. For instance, here is a
+method that consumes a read-only buffer:
+```scala
+def contents[T](consume buf: Buffer[T]): Int ->{buf.rd} T =
+  i => buf(i)
+```
+The `contents` method takes a read-only buffer and turns it into a function that
+produces for each valid index the element of the buffer at that index. Passing a
+buffer to `contents` effectively freezes it: Since `buf.rd` is reserved, we cannot
+use the exclusive `buf` capability beyond the point of call, so no further appends
+are possible. On the other hand, it is possible to read the buffer, and it is also possible
+to consume that read capability again in further calls:
+```scala
+val buf = Buffer[String]()
+val buf1 = linearAdd(buf, "hi") // buf unavailable from here
+val c1 = contents(buf1)         // only buf.rd is consumed
+val c2 = contents(buf1)         // buf.rd can be consumed repeatedly
+```
+Note that the only difference between `linearAdd` and `contents` is that `linearAdd`'s consume parameter has type `Buffer[T]^` whereas the
+corresponding parameter in `contents` has type `Buffer[T]`. The first type expands
+to `Buffer[T]^{cap}` whereas the second expands to `Buffer[T]^{cap.rd}`.
+
+
 ### Consume Methods
 
 Buffers in Scala's standard library use a single-argument method `+=` instead of a two argument global function like `linearAdd`. We can enforce linearity in this case by adding the `consume` modifier to the method itself.

tests/neg-custom-args/captures/i24373.check

@@ -0,0 +1,24 @@
+-- Error: tests/neg-custom-args/captures/i24373.scala:28:2 -------------------------------------------------------------
+28 |  x1.sink1 // error
+   |  ^^
+   |  Separation failure: Illegal access to (x1 : Foo^), which was passed to a
+   |  consume parameter or was used as a prefix to a consume method on line 27
+   |  and therefore is no longer available.
+   |
+   |  where:    ^ refers to a fresh root capability in the type of value x1
+-- Error: tests/neg-custom-args/captures/i24373.scala:32:2 -------------------------------------------------------------
+32 |  x2.sink2 // error
+   |  ^^
+   |  Separation failure: Illegal access to (x2 : Bar^), which was passed to a
+   |  consume parameter or was used as a prefix to a consume method on line 31
+   |  and therefore is no longer available.
+   |
+   |  where:    ^ refers to a fresh root capability in the type of value x2
+-- Error: tests/neg-custom-args/captures/i24373.scala:49:8 -------------------------------------------------------------
+49 |  sink6(x6) // error
+   |        ^^
+   |        Separation failure: Illegal access to (x6 : Bar^), which was passed to a
+   |        consume parameter or was used as a prefix to a consume method on line 48
+   |        and therefore is no longer available.
+   |
+   |        where:    ^ refers to a fresh root capability in the type of value x6

tests/neg-custom-args/captures/i24373.scala

@@ -0,0 +1,52 @@
+trait Foo:
+  consume def sink1: Unit = ()
+
+trait Bar extends Foo, caps.Mutable:
+  consume def sink2: Unit = ()
+
+class C extends caps.Mutable:
+  def sink4(consume x: Foo^) = ()
+
+object Foo:
+  extension (consume self: Foo^)
+    def sink: Unit = ()
+
+def Test =
+
+  def sink3(consume self: Foo^): Unit = ()
+
+  def sink5(consume self: Bar): Unit = ()
+
+  def sink6(consume self: Bar^): Unit = ()
+
+  val x: Bar^ = new Bar {}
+  x.sink
+  x.sink // no error: rd/rd
+
+  val x1: Foo^ = new Foo {}
+  x1.sink1
+  x1.sink1 // error
+
+  val x2: Bar^ = new Bar {}
+  x2.sink2
+  x2.sink2 // error
+
+  val x3: Bar^ = new Bar {}
+  sink3(x3)
+  sink3(x3) // no error: rd/rd
+
+  val x4: Bar^ = new Bar {}
+  val c = C()
+  c.sink4(x4)
+  c.sink4(x4) // no error: rd/rd
+
+  val x5: Bar^ = new Bar {}
+  sink5(x5)
+  sink5(x5) // no error: rd/rd
+
+  val x6: Bar^ = new Bar {}
+  sink6(x6)
+  sink6(x6) // error
+
+
+

tests/neg-custom-args/captures/i24373a.check

@@ -0,0 +1,44 @@
+-- Error: tests/neg-custom-args/captures/i24373a.scala:15:8 ------------------------------------------------------------
+15 |  sink2(x1)  // error
+   |        ^^
+   |        Separation failure: Illegal access to (x1 : Bar^), which was passed to a
+   |        consume parameter or was used as a prefix to a consume method on line 13
+   |        and therefore is no longer available.
+   |
+   |        where:    ^ refers to a fresh root capability in the type of value x1
+-- Error: tests/neg-custom-args/captures/i24373a.scala:19:8 ------------------------------------------------------------
+19 |  sink1(x2)  // error
+   |        ^^
+   |        Separation failure: Illegal access to x2.rd, which was passed to a
+   |        consume parameter or was used as a prefix to a consume method on line 18
+   |        and therefore is no longer available.
+-- Error: tests/neg-custom-args/captures/i24373a.scala:20:8 ------------------------------------------------------------
+20 |  sink2(x2)  // error
+   |        ^^
+   |        Separation failure: Illegal access to (x2 : Bar^), which was passed to a
+   |        consume parameter or was used as a prefix to a consume method on line 18
+   |        and therefore is no longer available.
+   |
+   |        where:    ^ refers to a fresh root capability in the type of value x2
+-- Error: tests/neg-custom-args/captures/i24373a.scala:25:8 ------------------------------------------------------------
+25 |  sink2(x3)  // error
+   |        ^^
+   |        Separation failure: Illegal access to (x3 : Bar^), which was passed to a
+   |        consume parameter or was used as a prefix to a consume method on line 23
+   |        and therefore is no longer available.
+   |
+   |        where:    ^ refers to a fresh root capability in the type of value x3
+-- Error: tests/neg-custom-args/captures/i24373a.scala:29:8 ------------------------------------------------------------
+29 |  sink3(x4)  // error
+   |        ^^
+   |        Separation failure: Illegal access to x4.rd, which was passed to a
+   |        consume parameter or was used as a prefix to a consume method on line 28
+   |        and therefore is no longer available.
+-- Error: tests/neg-custom-args/captures/i24373a.scala:30:8 ------------------------------------------------------------
+30 |  sink2(x4)  // error
+   |        ^^
+   |        Separation failure: Illegal access to (x4 : Bar^), which was passed to a
+   |        consume parameter or was used as a prefix to a consume method on line 28
+   |        and therefore is no longer available.
+   |
+   |        where:    ^ refers to a fresh root capability in the type of value x4

tests/neg-custom-args/captures/i24373a.scala

@@ -0,0 +1,34 @@
+trait Foo
+trait Bar extends Foo, caps.Mutable
+
+def Test =
+
+  def sink1(consume self: Foo^): Unit = () // consumes read-only reference
+
+  def sink2(consume self: Bar^): Unit = () // consumes exclusive reference
+
+  def sink3(consume self: Bar): Unit = () // consumes read-only reference
+
+  val x1: Bar^ = new Bar {}
+  sink1(x1)
+  sink1(x1)  // ok, rd/rd
+  sink2(x1)  // error
+
+  val x2: Bar^ = new Bar {}
+  sink2(x2)
+  sink1(x2)  // error
+  sink2(x2)  // error
+
+  val x3: Bar^ = new Bar {}
+  sink3(x3)
+  sink3(x3)  // ok, rd/rd
+  sink2(x3)  // error
+
+  val x4: Bar^ = new Bar {}
+  sink2(x4)
+  sink3(x4)  // error
+  sink2(x4)  // error
+
+
+
+

tests/neg-custom-args/captures/i24373b.check

@@ -0,0 +1,5 @@
+-- Error: tests/neg-custom-args/captures/i24373b.scala:3:18 ------------------------------------------------------------
+3 |trait Bar extends Foo, caps.Mutable // error
+  |                  ^^^
+  |                  illegal inheritance: trait Bar which extends `Mutable` is not allowed to also extend trait Foo
+  |                  since trait Foo retains exclusive capabilities but does not extend `Mutable`.

tests/neg-custom-args/captures/linear-buffer.check

@@ -33,42 +33,48 @@
    |             ^^^^^^^^^^^^^
    |       Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
    |       The access must be in a consume method to allow this.
--- Error: tests/neg-custom-args/captures/linear-buffer.scala:22:17 -----------------------------------------------------
-22 |  val buf3 = app(buf, 3) // error
+-- Error: tests/neg-custom-args/captures/linear-buffer.scala:23:17 -----------------------------------------------------
+23 |  val buf3 = app(buf, 3) // error
    |                 ^^^
    |                 Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a
-   |                 consume parameter or was used as a prefix to a consume method on line 20
+   |                 consume parameter or was used as a prefix to a consume method on line 21
    |                 and therefore is no longer available.
    |
    |                 where:    ^ refers to a fresh root capability in the type of parameter buf
--- Error: tests/neg-custom-args/captures/linear-buffer.scala:29:17 -----------------------------------------------------
-29 |  val buf3 = app(buf1, 4) // error
+-- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 -----------------------------------------------------
+30 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
    |                 Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
-   |                 consume parameter or was used as a prefix to a consume method on line 27
+   |                 consume parameter or was used as a prefix to a consume method on line 28
    |                 and therefore is no longer available.
    |
    |                 where:    ^ refers to a fresh root capability in the type of value buf1
--- Error: tests/neg-custom-args/captures/linear-buffer.scala:37:17 -----------------------------------------------------
-37 |  val buf3 = app(buf1, 4) // error
+-- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 -----------------------------------------------------
+38 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
    |                 Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
-   |                 consume parameter or was used as a prefix to a consume method on line 34
+   |                 consume parameter or was used as a prefix to a consume method on line 35
    |                 and therefore is no longer available.
    |
    |                 where:    ^ refers to a fresh root capability in the type of value buf1
--- Error: tests/neg-custom-args/captures/linear-buffer.scala:47:17 -----------------------------------------------------
-47 |  val buf3 = app(buf1, 4) // error
+-- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 -----------------------------------------------------
+48 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
    |                 Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
-   |                 consume parameter or was used as a prefix to a consume method on line 42
+   |                 consume parameter or was used as a prefix to a consume method on line 43
    |                 and therefore is no longer available.
    |
    |                 where:    ^ refers to a fresh root capability in the type of value buf1
--- Error: tests/neg-custom-args/captures/linear-buffer.scala:51:8 ------------------------------------------------------
-51 |    app(buf, 1)  // error
+-- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------
+52 |    app(buf, 1)  // error
    |        ^^^
    |        Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot
    |        be passed to a consume parameter or be used as a prefix of a consume method call.
    |
    |        where:    ^ refers to a fresh root capability in the type of parameter buf
+-- Error: tests/neg-custom-args/captures/linear-buffer.scala:62:20 -----------------------------------------------------
+62 |  val c3 = contents(buf)  // error
+   |                    ^^^
+   |                    Separation failure: Illegal access to buf.rd, which was passed to a
+   |                    consume parameter or was used as a prefix to a consume method on line 59
+   |                    and therefore is no longer available.

tests/neg-custom-args/captures/linear-buffer.scala

@@ -12,6 +12,7 @@ class BadBuffer[T] extends Mutable:
 
 class Buffer[T] extends Mutable:
   consume def append(x: T): Buffer[T]^ = this // ok
+  def apply(i: Int): T = ???
 
 def app[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
   buf.append(elem)
@@ -49,3 +50,14 @@ def Test4(consume buf: Buffer[Int]^) =
 def Test5(consume buf: Buffer[Int]^) =
   while true do
     app(buf, 1)  // error
+
+def contents[T](consume buf: Buffer[T]): Int ->{buf.rd} T =
+  i => buf(i)
+
+def Test6 =
+  val buf = Buffer[String]()
+  val buf1 = app(buf, "hi") // buf unavailable from here
+  val c1 = contents(buf1)         // only buf.rd is consumed
+  val c2 = contents(buf1)         // buf.rd can be consumed repeatedly
+  val c3 = contents(buf)  // error
+

tests/pos-custom-args/captures/i24373b.scala

@@ -0,0 +1,13 @@
+trait Foo extends caps.ExclusiveCapability
+
+trait Bar extends Foo, caps.Mutable
+
+def Test =
+
+  def f(self: Foo^): Unit = ()
+
+  val x: Bar^ = new Bar {}
+  val g = () => f(x) // `Foo` is not Mutable so `x.rd` is charged here
+
+  val _: () ->{x.rd} Unit = g  // surprising, but correct
+