Update mutatibility status only in open VarStates

Author: odersky

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

@@ -297,7 +297,7 @@ sealed abstract class CaptureSet extends Showable:
   /** The subcapturing test, using a given VarState */
   final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): Boolean =
     TypeComparer.inNestedLevel:
-      val this1 = this.adaptMutability(that)
+      val this1 = if vs.isOpen then this.adaptMutability(that) else this
       if this1 == null then false
       else if this1 ne this then
         capt.println(i"WIDEN ro $this with ${this.mutability} <:< $that with ${that.mutability} to $this1")

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

@@ -1,5 +1,5 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/linear-buffer.scala:7:29 ---------------------------------
-7 |    def bar: BadBuffer[T]^ = this // error
+7 |    def bar: BadBuffer[T]^ = this // error // error separation
   |                             ^^^^
   |                   Found:    BadBuffer[T]^{BadBuffer.this.rd}
   |                   Required: BadBuffer[T]^
@@ -15,6 +15,11 @@
   |                           ^^^^^^^^^^^^^
   |      Separation failure: method append'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:7:13 ------------------------------------------------------
+7 |    def bar: BadBuffer[T]^ = this // error // error separation
+  |             ^^^^^^^^^^^^^
+  |         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:10:29 -----------------------------------------------------
 10 |    def bar: BadBuffer[T]^ = this // error // error
    |                             ^^^^

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

@@ -4,7 +4,7 @@ import language.experimental.captureChecking
 class BadBuffer[T] extends Mutable:
   update def append(x: T): BadBuffer[T]^ = this // error
   def foo =
-    def bar: BadBuffer[T]^ = this // error
+    def bar: BadBuffer[T]^ = this // error // error separation
     bar
   update def updateFoo =
     def bar: BadBuffer[T]^ = this // error // error

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

@@ -9,7 +9,7 @@
   |    Cannot call update method set of self
   |    since its capture set {self} is read-only.
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:10:25 -----------------------------------
-10 |    val self2: Ref[T]^ = this // error
+10 |    val self2: Ref[T]^ = this // error // error separation
    |                         ^^^^
    |                         Found:    Ref[T]^{Ref.this.rd}
    |                         Required: Ref[T]^
@@ -58,7 +58,7 @@
    |    Cannot call update method set of Ref[T^{}]^{Ref.this.rd}
    |    since its capture set {Ref.this.rd} of method self5 is read-only.
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:20:27 -----------------------------------
-20 |    def self6(): Ref[T]^ = this // error
+20 |    def self6(): Ref[T]^ = this // error // error separation
    |                           ^^^^
    |                         Found:    Ref[T]^{Ref.this.rd}
    |                         Required: Ref[T]^
@@ -109,3 +109,13 @@
    |  ^^^^^^^^^^
    |  Cannot call update method set of Ref[Int]^{r6*.rd}
    |  since its capture set {r6*.rd} is read-only.
+-- Error: tests/neg-custom-args/captures/mutability.scala:10:15 --------------------------------------------------------
+10 |    val self2: Ref[T]^ = this // error // error separation
+   |               ^^^^^^^
+   |               Separation failure: value self2's type Ref[T]^ hides non-local this of class class Ref.
+   |               The access must be in a consume method to allow this.
+-- Error: tests/neg-custom-args/captures/mutability.scala:20:17 --------------------------------------------------------
+20 |    def self6(): Ref[T]^ = this // error // error separation
+   |                 ^^^^^^^
+   |                 Separation failure: method self6's result type Ref[T]^ hides non-local this of class class Ref.
+   |                 The access must be in a consume method to allow this.

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

@@ -7,7 +7,7 @@ class Ref[T](init: T) extends caps.Mutable:
   def sneakyHide(x: T) =
     val self = this
     self.set(x)  // error
-    val self2: Ref[T]^ = this // error
+    val self2: Ref[T]^ = this // error // error separation
     self2.set(x) // error
 
     val self3 = () => this
@@ -17,7 +17,7 @@ class Ref[T](init: T) extends caps.Mutable:
 
     def self5() = this
     self5().set(x)  // error
-    def self6(): Ref[T]^ = this // error
+    def self6(): Ref[T]^ = this // error // error separation
     self6().set(x) // error
 
 class Ref2[T](init: T) extends caps.Mutable:

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

@@ -9,7 +9,7 @@
   |    Cannot assign to field fld of self
   |    since its capture set {self} is read-only.
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:9:25 ---------------------------------------
-9 |    val self2: Ref[T]^ = this // error
+9 |    val self2: Ref[T]^ = this // error // error separation
   |                         ^^^^
   |                         Found:    Ref[T]^{Ref.this.rd}
   |                         Required: Ref[T]^
@@ -44,7 +44,7 @@
    |    Cannot assign to field fld of Ref[T^{}]^{Ref.this.rd}
    |    since its capture set {Ref.this.rd} of method self5 is read-only.
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:19:27 --------------------------------------
-19 |    def self6(): Ref[T]^ = this // error
+19 |    def self6(): Ref[T]^ = this // error // error separation
    |                           ^^^^
    |                         Found:    Ref[T]^{Ref.this.rd}
    |                         Required: Ref[T]^
@@ -88,3 +88,13 @@
    |  ^^^^^^^^^^^^^^^
    |  Cannot assign to field fld of Ref[Int]^{r6*.rd}
    |  since its capture set {r6*.rd} is read-only.
+-- Error: tests/neg-custom-args/captures/mutvars.scala:9:15 ------------------------------------------------------------
+9 |    val self2: Ref[T]^ = this // error // error separation
+  |               ^^^^^^^
+  |               Separation failure: value self2's type Ref[T]^ hides non-local this of class class Ref.
+  |               The access must be in a consume method to allow this.
+-- Error: tests/neg-custom-args/captures/mutvars.scala:19:17 -----------------------------------------------------------
+19 |    def self6(): Ref[T]^ = this // error // error separation
+   |                 ^^^^^^^
+   |                 Separation failure: method self6's result type Ref[T]^ hides non-local this of class class Ref.
+   |                 The access must be in a consume method to allow this.

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

@@ -6,7 +6,7 @@ class Ref[T](init: T) extends caps.Mutable:
   def sneakyHide(x: T) =
     val self = this
     self.fld = x  // error
-    val self2: Ref[T]^ = this // error
+    val self2: Ref[T]^ = this // error // error separation
     self2.fld = x
 
     val self3 = () => this
@@ -16,7 +16,7 @@ class Ref[T](init: T) extends caps.Mutable:
 
     def self5() = this
     self5().fld = x  // error
-    def self6(): Ref[T]^ = this // error
+    def self6(): Ref[T]^ = this // error // error separation
     self6().fld = x
 
 class Ref2[T](init: T) extends caps.Mutable:

tests/neg-custom-args/captures/ro-mut-conformance.check

@@ -4,14 +4,22 @@
    |  Cannot call update method set of a
    |  since its capture set {a} is read-only.
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 ---------------------------
-12 |  val t: Ref^{cap} = a  // error
+12 |  val t: Ref^{cap} = a  // error // error separation
    |                     ^
    |                     Found:    (a : Ref)
    |                     Required: Ref^
    |
    |                     Note that {cap} is an exclusive capture set of the mutable type Ref^,
    |                     it cannot subsume a read-only capture set of the mutable type (a : Ref).
    |
+   |                     Note that capability cap².rd is not included in capture set {cap}.
+   |
    |                     where:    ^ and cap refer to a fresh root capability in the type of value t
+   |                               cap²      is a fresh root capability in the type of parameter a
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:9 -------------------------------------------------
+12 |  val t: Ref^{cap} = a  // error // error separation
+   |         ^^^^^^^^^
+   |         Separation failure: value t's type Ref^ hides parameter a.
+   |         The parameter needs to be annotated with consume to allow this.

tests/neg-custom-args/captures/ro-mut-conformance.scala

@@ -9,7 +9,7 @@ class Ref extends IRef, Mutable:
 def test1(a: Ref^{cap.rd}): Unit =
   a.set(42)  // error
 def test2(a: Ref^{cap.rd}): Unit =
-  val t: Ref^{cap} = a  // error
+  val t: Ref^{cap} = a  // error // error separation
   def b: Ref^{cap.rd} = ???
   val i: IRef^{cap} = b // ok, no added privilege from `cap` on an IRef
   t.set(42)

tests/pos-custom-args/captures/consume-shared.scala

@@ -0,0 +1,9 @@
+import caps.*
+class C extends SharedCapability
+
+def foo(consume x: C): C = x
+
+def test(consume x: C) =
+  val y: C = C()
+  foo(x)
+  foo(y)