From 74d649065171f14d43d66d4609ce9fbad1454695 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 6 Nov 2025 13:36:27 +0100 Subject: [PATCH 01/12] Changes to Mutable 1. Mutable and ExclsuiveCapability are not longer classifiers. This means Mutable classes can capture other capabilities. Red is still a classifier. 2. Update methods in nested classes can access exclsuive capabilities external to enclosing classes. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 8 +-- .../src/dotty/tools/dotc/cc/Mutability.scala | 6 +- .../src/dotty/tools/dotc/typer/Namer.scala | 6 +- library/src/scala/caps/package.scala | 4 +- .../captures/classified-inheritance.check | 6 +- .../captures/classified-inheritance.scala | 4 +- .../captures/classifiers-1.scala | 2 +- tests/neg-custom-args/captures/i23726.check | 6 +- tests/neg-custom-args/captures/i24310.scala | 3 +- .../captures/lazyvals-sep.check | 4 +- .../captures/linear-buffer-2.check | 10 ++-- .../captures/linear-buffer.check | 36 ++++++------ tests/neg-custom-args/captures/matrix.check | 4 +- .../captures/mut-iterator.check | 29 ++++++++++ .../captures/mut-iterator.scala | 32 ++++++++++ .../captures/mut-iterator1.check | 5 ++ .../captures/mut-iterator1.scala | 30 ++++++++++ .../captures/mut-iterator2.check | 17 ++++++ .../captures/mut-iterator2.scala | 30 ++++++++++ .../captures/mut-iterator3.check | 10 ++++ .../captures/mut-iterator3.scala | 32 ++++++++++ .../captures/mut-iterator4.check | 29 ++++++++++ .../captures/mut-iterator4.scala | 33 +++++++++++ .../captures/mut-iterator5.check | 12 ++++ .../captures/mut-iterator5.scala | 33 +++++++++++ .../neg-custom-args/captures/mutability.check | 58 +++++++++---------- .../captures/mutable-inheritance.check | 11 ++-- tests/neg-custom-args/captures/mutvars.check | 52 ++++++++--------- .../captures/ro-mut-conformance.check | 12 ++-- .../captures/scope-extrude-mut.check | 2 +- tests/neg-custom-args/captures/sep-box.check | 2 +- .../captures/sep-consume.check | 4 +- .../captures/sep-counter.check | 4 +- .../captures/sep-curried.check | 20 +++---- tests/neg-custom-args/captures/sep-list.check | 2 +- .../captures/sep-pairs-unboxed.check | 20 +++---- .../neg-custom-args/captures/sep-pairs.check | 24 ++++---- .../captures/mut-iterator.scala | 30 ++++++++++ .../captures/restrict-try.scala | 8 +-- 39 files changed, 484 insertions(+), 156 deletions(-) create mode 100644 tests/neg-custom-args/captures/mut-iterator.check create mode 100644 tests/neg-custom-args/captures/mut-iterator.scala create mode 100644 tests/neg-custom-args/captures/mut-iterator1.check create mode 100644 tests/neg-custom-args/captures/mut-iterator1.scala create mode 100644 tests/neg-custom-args/captures/mut-iterator2.check create mode 100644 tests/neg-custom-args/captures/mut-iterator2.scala create mode 100644 tests/neg-custom-args/captures/mut-iterator3.check create mode 100644 tests/neg-custom-args/captures/mut-iterator3.scala create mode 100644 tests/neg-custom-args/captures/mut-iterator4.check create mode 100644 tests/neg-custom-args/captures/mut-iterator4.scala create mode 100644 tests/neg-custom-args/captures/mut-iterator5.check create mode 100644 tests/neg-custom-args/captures/mut-iterator5.scala create mode 100644 tests/pos-custom-args/captures/mut-iterator.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 92fa632f5166..1bb4764b9206 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -573,12 +573,12 @@ class CheckCaptures extends Recheck, SymTransformer: // fresh capabilities. We do check that they hide no parameter reach caps in checkEscapingUses case _ => - def checkReadOnlyMethod(included: CaptureSet, env: Env): Unit = + def checkReadOnlyMethod(included: CaptureSet, meth: Symbol): Unit = included.checkAddedElems: elem => if elem.isExclusive then report.error( - em"""Read-only ${env.owner} accesses exclusive capability $elem; - |${env.owner} should be declared an update method to allow this.""", + em"""Read-only $meth accesses exclusive capability $elem; + |$meth should be declared an update method to allow this.""", tree.srcPos) def recur(cs: CaptureSet, env: Env, lastEnv: Env | Null): Unit = @@ -599,7 +599,7 @@ class CheckCaptures extends Recheck, SymTransformer: val nextEnv = nextEnvToCharge(env) if nextEnv != null && !nextEnv.owner.isStaticOwner then if env.owner.isReadOnlyMethodOrLazyVal && nextEnv.owner != env.owner then - checkReadOnlyMethod(included, env) + checkReadOnlyMethod(included, env.owner) recur(included, nextEnv, env) // Under deferredReaches, don't propagate out of methods inside terms. // The use set of these methods will be charged when that method is called. diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala index 57bbd9e8be44..6098088f1602 100644 --- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Mutability.scala @@ -47,7 +47,8 @@ object Mutability: extension (sym: Symbol) /** An update method is either a method marked with `update` or - * a setter of a non-transparent var. + * a setter of a non-transparent var. `update` is implicit for `consume` methods + * of Mutable classes. */ def isUpdateMethod(using Context): Boolean = sym.isAllOf(Mutable | Method) @@ -63,8 +64,9 @@ object Mutability: private def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity = import Exclusivity.* if sym == cls then OK // we are directly in `cls` or in one of its constructors + else if sym.isUpdateMethod then OK else if sym.owner == cls then - if sym.isUpdateMethod || sym.isConstructor then OK + if sym.isConstructor then OK else NotInUpdateMethod(sym, cls) else if sym.isStatic then OutsideClass(cls) else sym.owner.inExclusivePartOf(cls) diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala index 02a55be9ea5a..2e8c435e2c38 100644 --- a/compiler/src/dotty/tools/dotc/typer/Namer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala @@ -995,8 +995,12 @@ class Namer { typer: Typer => end if } + /** Add an implicit Mutable flag to consume methods in Mutable classes. This + * turns the method into an update method. + */ private def normalizeFlags(denot: SymDenotation)(using Context): Unit = - if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) then + if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) + && denot.owner.derivesFrom(defn.Caps_Mutable) then denot.setFlag(Mutable) /** Intentionally left without `using Context` parameter. We need diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 0527c3e149d6..6fbb0a9a0f93 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -63,7 +63,7 @@ type Shared = SharedCapability * During separation checking, exclusive usage of marked capabilities will be enforced. */ @experimental -trait ExclusiveCapability extends Capability, Classifier +trait ExclusiveCapability extends Capability @experimental type Exclusive = ExclusiveCapability @@ -80,7 +80,7 @@ trait Control extends SharedCapability, Classifier /** Marker trait for classes with methods that require an exclusive reference. */ @experimental -trait Mutable extends ExclusiveCapability, Classifier +trait Mutable extends ExclusiveCapability /** Marker trait for classes with reader methods, typically extended by Mutable classes */ @experimental diff --git a/tests/neg-custom-args/captures/classified-inheritance.check b/tests/neg-custom-args/captures/classified-inheritance.check index 629f815c4b06..6f34d52a4b7a 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.check +++ b/tests/neg-custom-args/captures/classified-inheritance.check @@ -1,8 +1,8 @@ -- Error: tests/neg-custom-args/captures/classified-inheritance.scala:5:6 ---------------------------------------------- -5 |class C2 extends caps.Control, caps.Mutable // error +5 |class C2 extends caps.Control, caps.Read // error | ^ - | class C2 inherits two unrelated classifier traits: trait Mutable and trait Control + | class C2 inherits two unrelated classifier traits: trait Read and trait Control -- Error: tests/neg-custom-args/captures/classified-inheritance.scala:10:6 --------------------------------------------- 10 |class C3 extends Matrix, Async // error | ^ - | class C3 inherits two unrelated classifier traits: trait Control and trait Mutable + | class C3 inherits two unrelated classifier traits: trait Control and trait Read diff --git a/tests/neg-custom-args/captures/classified-inheritance.scala b/tests/neg-custom-args/captures/classified-inheritance.scala index 3aef8bd5e35d..78ac5c779271 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.scala +++ b/tests/neg-custom-args/captures/classified-inheritance.scala @@ -2,9 +2,9 @@ import language.experimental.captureChecking class C1 extends caps.Control, caps.SharedCapability // OK -class C2 extends caps.Control, caps.Mutable // error +class C2 extends caps.Control, caps.Read // error trait Async extends caps.Control -class Matrix extends caps.Mutable +class Matrix extends caps.Read class C3 extends Matrix, Async // error diff --git a/tests/neg-custom-args/captures/classifiers-1.scala b/tests/neg-custom-args/captures/classifiers-1.scala index ee49330ec801..ce0ca8890923 100644 --- a/tests/neg-custom-args/captures/classifiers-1.scala +++ b/tests/neg-custom-args/captures/classifiers-1.scala @@ -1,4 +1,4 @@ -class M extends caps.Mutable +class M extends caps.Read class M1(x: Int => Int) extends M // error diff --git a/tests/neg-custom-args/captures/i23726.check b/tests/neg-custom-args/captures/i23726.check index 452de9d23b4f..61f4c66d12a9 100644 --- a/tests/neg-custom-args/captures/i23726.check +++ b/tests/neg-custom-args/captures/i23726.check @@ -14,7 +14,7 @@ | The two sets overlap at : {a} | |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply + | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:16:5 ------------------------------------------------------------- 16 | f3(b) // error | ^ @@ -31,7 +31,7 @@ | The two sets overlap at : {b} | |where: ^ refers to a fresh root capability classified as Mutable in the type of value b - | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply + | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:24:5 ------------------------------------------------------------- 24 | f7(a) // error | ^ @@ -48,4 +48,4 @@ | The two sets overlap at : {a} | |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply + | ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply diff --git a/tests/neg-custom-args/captures/i24310.scala b/tests/neg-custom-args/captures/i24310.scala index ca390f715ae5..741ce05b8e5c 100644 --- a/tests/neg-custom-args/captures/i24310.scala +++ b/tests/neg-custom-args/captures/i24310.scala @@ -11,11 +11,12 @@ class Matrix(val f: () => Int) extends Mutable: update def add(): Unit = () -@main def test = +def test(consume proc: () => Int) = val r: Ref^ = Ref() val m: Matrix^ = Matrix(() => 42) val m2: Matrix^ = Matrix(() => m.run()) val m3: Matrix^ = Matrix(() => r.get()) + val m4: Matrix^ = Matrix(proc) def par(f1: () => Int, f2: () => Int): Unit = println(s"par results: ${f1()} and ${f2()}") diff --git a/tests/neg-custom-args/captures/lazyvals-sep.check b/tests/neg-custom-args/captures/lazyvals-sep.check index 0b9e9b969a27..0d01da2c2f30 100644 --- a/tests/neg-custom-args/captures/lazyvals-sep.check +++ b/tests/neg-custom-args/captures/lazyvals-sep.check @@ -34,7 +34,7 @@ |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 Ref^{TestClass.this.r.rd}. | - |where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper + |where: ^ and cap refer to a fresh root capability created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:77:12 --------------------------------- @@ -48,7 +48,7 @@ |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 Ref^{TestClass.this.r.rd}. | - |where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper + |where: ^ and cap refer to a fresh root capability created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:82:8 ------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index 700c37ee2302..63cb8472fc05 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -5,7 +5,7 @@ | consume parameter or was used as a prefix to a consume method on line 11 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- 20 | val buf3 = buf1.append(4) // error | ^^^^ @@ -13,7 +13,7 @@ | 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 classified as Mutable in the type of value buf1 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 --------------------------------------------------- 28 | val buf3 = buf1.append(4) // error | ^^^^ @@ -21,7 +21,7 @@ | consume parameter or was used as a prefix to a consume method on line 25 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 --------------------------------------------------- 38 | val buf3 = buf1.append(4) // error | ^^^^ @@ -29,11 +29,11 @@ | consume parameter or was used as a prefix to a consume method on line 33 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ---------------------------------------------------- 42 | buf.append(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 classified as Mutable in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 4d13f9916fef..549adb55a351 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -1,15 +1,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/linear-buffer.scala:7:29 --------------------------------- 7 | def bar: BadBuffer[T]^ = this // error | ^^^^ - | Found: BadBuffer[T]^{BadBuffer.this.rd} - | Required: BadBuffer[T]^ + | Found: BadBuffer[T]^{BadBuffer.this.rd} + | Required: BadBuffer[T]^ | - | Note that capability BadBuffer.this.rd is not included in capture set {}. + | Note that capability BadBuffer.this.rd is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^, - | it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}. + | Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^, + | it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}. | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method bar + | where: ^ and cap refer to a fresh root capability in the result type of method bar | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/linear-buffer.scala:5:27 ------------------------------------------------------ @@ -20,11 +20,11 @@ -- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:29 ----------------------------------------------------- 10 | def bar: BadBuffer[T]^ = this // error // error | ^^^^ - | Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition - | of method append with result type BadBuffer[T]^. - | This type hides capabilities {BadBuffer.this} + | Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition + | of method append with result type BadBuffer[T]^. + | This type hides capabilities {BadBuffer.this} | - | where: ^ refers to a fresh root capability classified as Mutable in the result type of method append + | where: ^ refers to a fresh root capability in the result type of method append -- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:13 ----------------------------------------------------- 10 | def bar: BadBuffer[T]^ = this // error // error | ^^^^^^^^^^^^^ @@ -33,11 +33,11 @@ -- Error: tests/neg-custom-args/captures/linear-buffer.scala:22:17 ----------------------------------------------------- 22 | 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 - | and therefore is no longer available. + | 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 + | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf + | 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 | ^^^^ @@ -45,7 +45,7 @@ | 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 classified as Mutable in the type of value buf1 + | 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 | ^^^^ @@ -53,7 +53,7 @@ | consume parameter or was used as a prefix to a consume method on line 34 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | 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 | ^^^^ @@ -61,11 +61,11 @@ | consume parameter or was used as a prefix to a consume method on line 42 | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | 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 | ^^^ | 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 classified as Mutable in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf diff --git a/tests/neg-custom-args/captures/matrix.check b/tests/neg-custom-args/captures/matrix.check index f6d1cf6634bc..6a58b62dc2a3 100644 --- a/tests/neg-custom-args/captures/matrix.check +++ b/tests/neg-custom-args/captures/matrix.check @@ -13,7 +13,7 @@ | Footprint set of third argument : {m2} | The two sets overlap at : {m2} | - |where: cap is a fresh root capability classified as Mutable created in method Test when checking argument to parameter y of method mul + |where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul -- Error: tests/neg-custom-args/captures/matrix.scala:30:11 ------------------------------------------------------------ 30 | mul1(m1, m2, m2) // error: will fail separation checking | ^^ @@ -29,4 +29,4 @@ | Footprint set of third argument : {m2} | The two sets overlap at : {m2} | - |where: cap is a fresh root capability classified as Mutable created in method Test when checking argument to parameter y of method mul1 + |where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul1 diff --git a/tests/neg-custom-args/captures/mut-iterator.check b/tests/neg-custom-args/captures/mut-iterator.check new file mode 100644 index 000000000000..22c1c425cd7b --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator.check @@ -0,0 +1,29 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:9:17 ------------------------------------------------------- +9 | def next() = f(Iterator.this.next()) // error + | ^ + | Read-only method next accesses exclusive capability (f : T => U); + | method next should be declared an update method to allow this. + | + | where: => refers to a fresh root capability in the type of parameter f +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:17:14 ------------------------------------------------------ +17 | current = xs1 // error + | ^^^^^^^^^^^^^ + | Cannot assign to field current of $anon.this + | since the access is in method next, which is not an update method. +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:22:15 ------------------------------------------------------ +22 | def next() = f(it.next()) // error + | ^ + | Read-only method next accesses exclusive capability (f : T => U); + | method next should be declared an update method to allow this. + | + | where: => refers to a fresh root capability in the type of parameter f +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:7:25 ------------------------------------------------------- +7 | def map[U](f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method map's result type Iterator[U]^{cap.rd} hides non-local this of class trait Iterator. + | The access must be in a consume method to allow this. +-- Error: tests/neg-custom-args/captures/mut-iterator.scala:20:55 ------------------------------------------------------ +20 |def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method mappedIterator's result type Iterator[U]^{cap.rd} hides parameters it and f. + | The parameters need to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/mut-iterator.scala b/tests/neg-custom-args/captures/mut-iterator.scala new file mode 100644 index 000000000000..a6e022ead7fe --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator.scala @@ -0,0 +1,32 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + def next(): T + + def map[U](f: T => U): Iterator[U] = new Iterator: // error + def hasNext = Iterator.this.hasNext + def next() = f(Iterator.this.next()) // error +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 // error + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + def hasNext = it.hasNext + def next() = f(it.next()) // error + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + val proc: Int => Int = i => { io.write(i); i * i } + listIterator(List(1, 2, 3)).map(proc) + val roit: Iterator[Int]^{cap.rd} = listIterator(List(1, 2, 3)) + val mapped = roit.map(proc) + mapped.next() diff --git a/tests/neg-custom-args/captures/mut-iterator1.check b/tests/neg-custom-args/captures/mut-iterator1.check new file mode 100644 index 000000000000..2a167a752e41 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator1.check @@ -0,0 +1,5 @@ +-- [E164] Declaration Error: tests/neg-custom-args/captures/mut-iterator1.scala:9:15 ----------------------------------- +9 | update def next() = f(Iterator.this.next()) // error + | ^ + | error overriding method next in trait Iterator of type (): U; + | method next of type (): U is an update method, cannot override a read-only method diff --git a/tests/neg-custom-args/captures/mut-iterator1.scala b/tests/neg-custom-args/captures/mut-iterator1.scala new file mode 100644 index 000000000000..c51575c4b2f7 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator1.scala @@ -0,0 +1,30 @@ +import caps.{Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + def next(): T + + def map[U](f: T => U): Iterator[U] = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) // error +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: + def hasNext = it.hasNext + def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + listIterator(List(1, 2, 3)).map: i => + io.write(i) + i * i diff --git a/tests/neg-custom-args/captures/mut-iterator2.check b/tests/neg-custom-args/captures/mut-iterator2.check new file mode 100644 index 000000000000..4e4febb46ff3 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator2.check @@ -0,0 +1,17 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator2.scala:9:26 ------------------------------------------------------ +9 | update def next() = f(Iterator.this.next()) // error + | ^^^^^^^^^^^^^ + | Read-only method map accesses exclusive capability (Iterator.this : Iterator[T]^); + | method map should be declared an update method to allow this. + | + | where: ^ refers to the universal root capability +-- Error: tests/neg-custom-args/captures/mut-iterator2.scala:7:25 ------------------------------------------------------ +7 | def map[U](f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method map's result type Iterator[U]^{cap.rd} hides non-local this of class trait Iterator. + | The access must be in a consume method to allow this. +-- Error: tests/neg-custom-args/captures/mut-iterator2.scala:20:55 ----------------------------------------------------- +20 |def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + | ^^^^^^^^^^^ + | Separation failure: method mappedIterator's result type Iterator[U]^{cap.rd} hides parameters it and f. + | The parameters need to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/mut-iterator2.scala b/tests/neg-custom-args/captures/mut-iterator2.scala new file mode 100644 index 000000000000..9a2b76018dba --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator2.scala @@ -0,0 +1,30 @@ +import caps.{Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + def map[U](f: T => U): Iterator[U] = new Iterator: // error + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) // error +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U] = new Iterator: // error + def hasNext = it.hasNext + update def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + listIterator(List(1, 2, 3)).map: i => + io.write(i) + i * i diff --git a/tests/neg-custom-args/captures/mut-iterator3.check b/tests/neg-custom-args/captures/mut-iterator3.check new file mode 100644 index 000000000000..e80d8bd541d6 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator3.check @@ -0,0 +1,10 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator3.scala:31:20 ----------------------------------------------------- +31 | val mapped = roit.map(proc) // error + | ^^^^^^^^ + | Cannot call update method map of roit + | since its capture set {roit} is read-only. +-- Error: tests/neg-custom-args/captures/mut-iterator3.scala:32:9 ------------------------------------------------------ +32 | mapped.next() // error + | ^^^^^^^^^^^ + | Cannot call update method next of mapped + | since its capture set {mapped} is read-only. diff --git a/tests/neg-custom-args/captures/mut-iterator3.scala b/tests/neg-custom-args/captures/mut-iterator3.scala new file mode 100644 index 000000000000..5170cebe6f03 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator3.scala @@ -0,0 +1,32 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + consume def map[U](consume f: T => U): Iterator[U] = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](consume it: Iterator[T]^, consume f: T => U): Iterator[U] = new Iterator: + def hasNext = it.hasNext + update def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + def proc: Int => Int = i => { io.write(i); i * i } + listIterator(List(1, 2, 3)).map(proc) + val roit: Iterator[Int]^{cap.rd} = listIterator(List(1, 2, 3)) + val mapped = roit.map(proc) // error + mapped.next() // error diff --git a/tests/neg-custom-args/captures/mut-iterator4.check b/tests/neg-custom-args/captures/mut-iterator4.check new file mode 100644 index 000000000000..9400c630406f --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator4.check @@ -0,0 +1,29 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator4.scala:9:26 ------------------------------------------------------ +9 | update def next() = f(Iterator.this.next()) // error // error + | ^^^^^^^^^^^^^ + | Read-only method map accesses exclusive capability (Iterator.this : Iterator[T]^); + | method map should be declared an update method to allow this. + | + | where: ^ refers to the universal root capability +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-iterator4.scala:9:47 --------------------------------- +9 | update def next() = f(Iterator.this.next()) // error // error + | ^ + |Found: Iterator[U^'s1]^{Iterator.this.rd, f, Iterator.this, cap} + |Required: Iterator[U]^{Iterator.this, f} + | + |Note that capability cap is not included in capture set {Iterator.this, f}. + | + |where: cap is a fresh root capability classified as Mutable created in method map when constructing instance Object with (Iterator[U]^{cap².rd}) {...} + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-iterator4.scala:23:34 -------------------------------- +23 | update def next() = f(it.next()) // error + | ^ + |Found: Iterator[U^'s2]^{it.rd, f, it, cap} + |Required: Iterator[U]^{it, f} + | + |Note that capability cap is not included in capture set {it, f}. + | + |where: cap is a fresh root capability classified as Mutable created in method mappedIterator when constructing instance Object with (Iterator[U]^{cap².rd}) {...} + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/mut-iterator4.scala b/tests/neg-custom-args/captures/mut-iterator4.scala new file mode 100644 index 000000000000..114c08af2001 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator4.scala @@ -0,0 +1,33 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + def map[U](f: T => U): Iterator[U]^{Iterator.this, f} = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) // error // error + +end Iterator + +def listIterator[T](xs: List[T]): Iterator[T]^ = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U]^{it, f} = new Iterator: + def hasNext = it.hasNext + update def next() = f(it.next()) // error + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + def proc: Int => Int = i => { io.write(i); i * i } + listIterator(List(1, 2, 3)).map(proc) + val roit: Iterator[Int]^{cap.rd} = listIterator(List(1, 2, 3)) + val mapped = roit.map(proc) + mapped.next() diff --git a/tests/neg-custom-args/captures/mut-iterator5.check b/tests/neg-custom-args/captures/mut-iterator5.check new file mode 100644 index 000000000000..f9aa93e489e2 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator5.check @@ -0,0 +1,12 @@ +-- Error: tests/neg-custom-args/captures/mut-iterator5.scala:11:23 ----------------------------------------------------- +11 | while hasNext do f(next()) // error + | ^^^^ + | Cannot call update method next of Iterator.this + | since the access is in method stupidForeach, which is not an update method. +-- Error: tests/neg-custom-args/captures/mut-iterator5.scala:16:26 ----------------------------------------------------- +16 | update def next() = Iterator.this.next() // error + | ^^^^^^^^^^^^^ + | Read-only method sneakyForeach accesses exclusive capability (Iterator.this : Iterator[T]^); + | method sneakyForeach should be declared an update method to allow this. + | + | where: ^ refers to the universal root capability diff --git a/tests/neg-custom-args/captures/mut-iterator5.scala b/tests/neg-custom-args/captures/mut-iterator5.scala new file mode 100644 index 000000000000..a2af33c2e1f4 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-iterator5.scala @@ -0,0 +1,33 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + update def foreach[U](f: T => Unit): Unit = + while hasNext do f(next()) + + def stupidForeach[U](f: T => Unit): Unit = + while hasNext do f(next()) // error + + def sneakyForeach(f: T => Unit): Unit = + val it = new Iterator[T]: + def hasNext = Iterator.this.hasNext + update def next() = Iterator.this.next() // error + while it.hasNext do f(it.next()) +end Iterator + +def listIterator[T](xs: List[T]): Iterator[T]^ = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + def proc: Int => Unit = i => io.write(i) + val f = () => listIterator(List(1, 2, 3)).sneakyForeach(proc) diff --git a/tests/neg-custom-args/captures/mutability.check b/tests/neg-custom-args/captures/mutability.check index 90abebcbcb15..c4da68169ce8 100644 --- a/tests/neg-custom-args/captures/mutability.check +++ b/tests/neg-custom-args/captures/mutability.check @@ -11,15 +11,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:10:25 ----------------------------------- 10 | val self2: Ref[T]^ = this // error | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | Note that capability Ref.this.rd is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value self2 + | where: ^ and cap refer to a fresh root capability in the type of value self2 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:11:13 -------------------------------------------------------- @@ -28,7 +28,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of class Ref + | where: ^ refers to a fresh root capability in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:14:12 -------------------------------------------------------- 14 | self3().set(x) // error | ^^^^^^^^^^^ @@ -37,16 +37,16 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:15:31 ----------------------------------- 15 | val self4: () => Ref[T]^ = () => this // error | ^^^^^^^^^^ - | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} - | Required: () => Ref[T]^ + | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} + | Required: () => Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | Note that capability Ref.this.rd is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. | - | where: => refers to a fresh root capability in the type of value self4 - | ^ and cap refer to a fresh root capability classified as Mutable in the type of value self4 + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability in the type of value self4 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:16:15 -------------------------------------------------------- @@ -55,7 +55,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of class Ref + | where: ^ refers to a fresh root capability in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:19:12 -------------------------------------------------------- 19 | self5().set(x) // error | ^^^^^^^^^^^ @@ -64,15 +64,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:20:27 ----------------------------------- 20 | def self6(): Ref[T]^ = this // error | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | Note that capability Ref.this.rd is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method self6 + | where: ^ and cap refer to a fresh root capability in the result type of method self6 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:21:15 -------------------------------------------------------- @@ -81,7 +81,7 @@ | Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^); | method sneakyHide should be declared an update method to allow this. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of class Ref + | where: ^ refers to a fresh root capability in the type of class Ref -- Error: tests/neg-custom-args/captures/mutability.scala:25:25 -------------------------------------------------------- 25 | def set(x: T) = this.x.set(x) // error | ^^^^^^^^^^ @@ -100,16 +100,16 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:42:29 ----------------------------------- 42 | val r5: () => Ref2[Int]^ = () => ref2 // error | ^^^^^^^^^^ - | Found: () ->{ref2.rd} Ref2[Int]^{ref2} - | Required: () => Ref2[Int]^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ | - | Note that capability ref2 is not included in capture set {}. + | Note that capability ref2 is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, - | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. + | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, + | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. | - | where: => refers to a fresh root capability in the type of value r5 - | ^ and cap refer to a fresh root capability classified as Mutable in the type of value r5 + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability in the type of value r5 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutability.scala:45:9 --------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/mutable-inheritance.check b/tests/neg-custom-args/captures/mutable-inheritance.check index 013a1e09926d..84d69eb2824c 100644 --- a/tests/neg-custom-args/captures/mutable-inheritance.check +++ b/tests/neg-custom-args/captures/mutable-inheritance.check @@ -1,9 +1,3 @@ --- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:4:8 ------------------------------------------------- -4 | class A extends E, caps.Mutable // error - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | reference (c : Object^) is not included in the allowed capture set {cap} of the self type of class A - | - | where: cap is a fresh root capability classified as Mutable in the type of class A -- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:7:16 ------------------------------------------------ 7 |class C extends B(??? : Int => Int), caps.Mutable // error | ^^^^^^^^^^^^^^^^^^^ @@ -14,3 +8,8 @@ | ^ | illegal inheritance: class H which extends `Mutable` is not allowed to also extend class G | since class G retains exclusive capabilities but does not extend `Mutable`. +-- Error: tests/neg-custom-args/captures/mutable-inheritance.scala:4:18 ------------------------------------------------ +4 | class A extends E, caps.Mutable // error + | ^ + | illegal inheritance: class A which extends `Mutable` is not allowed to also extend class E + | since class E retains exclusive capabilities but does not extend `Mutable`. diff --git a/tests/neg-custom-args/captures/mutvars.check b/tests/neg-custom-args/captures/mutvars.check index f5c83dbbb333..76cf79f25987 100644 --- a/tests/neg-custom-args/captures/mutvars.check +++ b/tests/neg-custom-args/captures/mutvars.check @@ -11,15 +11,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:9:25 --------------------------------------- 9 | val self2: Ref[T]^ = this // error | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | Note that capability Ref.this.rd is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value self2 + | where: ^ and cap refer to a fresh root capability in the type of value self2 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:13:16 ----------------------------------------------------------- @@ -30,16 +30,16 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:14:31 -------------------------------------- 14 | val self4: () => Ref[T]^ = () => this // error | ^^^^^^^^^^ - | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} - | Required: () => Ref[T]^ + | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} + | Required: () => Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | Note that capability Ref.this.rd is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. | - | where: => refers to a fresh root capability in the type of value self4 - | ^ and cap refer to a fresh root capability classified as Mutable in the type of value self4 + | where: => refers to a fresh root capability in the type of value self4 + | ^ and cap refer to a fresh root capability in the type of value self4 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:18:16 ----------------------------------------------------------- @@ -50,15 +50,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:19:27 -------------------------------------- 19 | def self6(): Ref[T]^ = this // error | ^^^^ - | Found: Ref[T]^{Ref.this.rd} - | Required: Ref[T]^ + | Found: Ref[T]^{Ref.this.rd} + | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. + | Note that capability Ref.this.rd is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, - | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. + | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, + | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method self6 + | where: ^ and cap refer to a fresh root capability in the result type of method self6 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:24:29 ----------------------------------------------------------- @@ -79,16 +79,16 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutvars.scala:41:29 -------------------------------------- 41 | val r5: () => Ref2[Int]^ = () => ref2 // error | ^^^^^^^^^^ - | Found: () ->{ref2.rd} Ref2[Int]^{ref2} - | Required: () => Ref2[Int]^ + | Found: () ->{ref2.rd} Ref2[Int]^{ref2} + | Required: () => Ref2[Int]^ | - | Note that capability ref2 is not included in capture set {}. + | Note that capability ref2 is not included in capture set {}. | - | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, - | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. + | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, + | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. | - | where: => refers to a fresh root capability in the type of value r5 - | ^ and cap refer to a fresh root capability classified as Mutable in the type of value r5 + | where: => refers to a fresh root capability in the type of value r5 + | ^ and cap refer to a fresh root capability in the type of value r5 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/mutvars.scala:44:13 ----------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 079862ca9df6..153fd5458ba6 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -6,14 +6,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 --------------------------- 12 | val t: Ref^{cap} = a // error | ^ - | Found: (a : Ref) - | Required: Ref^ + | Found: (a : Ref) + | Required: Ref^ | - | Note that capability a is not included in capture set {}. + | Note that capability a is not included in capture set {}. | - | 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 {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). | - | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value t + | where: ^ and cap refer to a fresh root capability in the type of value t | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check index 905becd123e4..535cbed775cf 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.check +++ b/tests/neg-custom-args/captures/scope-extrude-mut.check @@ -8,6 +8,6 @@ | because (a1 : A^) in method b is not visible from cap in variable a. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value a1 - | ^² and cap refer to a fresh root capability classified as Mutable in the type of variable a + | ^² and cap refer to a fresh root capability in the type of variable a | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/sep-box.check b/tests/neg-custom-args/captures/sep-box.check index 590c0b01c757..54ab518926cc 100644 --- a/tests/neg-custom-args/captures/sep-box.check +++ b/tests/neg-custom-args/captures/sep-box.check @@ -13,4 +13,4 @@ | Footprint set of second argument : {xs*} | The two sets overlap at : {xs*} | - |where: ^ refers to a fresh root capability classified as Mutable created in method test when checking argument to parameter x of method par + |where: ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check index 5967947783ae..0d1a4df1e98e 100644 --- a/tests/neg-custom-args/captures/sep-consume.check +++ b/tests/neg-custom-args/captures/sep-consume.check @@ -5,7 +5,7 @@ | 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 classified as Mutable in the type of parameter x + | where: ^ refers to a fresh root capability in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 ------------------------------------------------------- 21 | par(rx, () => x.put(42)) // error | ^ @@ -13,7 +13,7 @@ | 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 classified as Mutable in the type of parameter x + | where: ^ refers to a fresh root capability in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 ------------------------------------------------------- 26 | def foo = bad(f) // error | ^ diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check index 2676f3f62362..39b657a201f1 100644 --- a/tests/neg-custom-args/captures/sep-counter.check +++ b/tests/neg-custom-args/captures/sep-counter.check @@ -6,7 +6,7 @@ |Another part, Ref^², captures capabilities {c}. |The two sets overlap at {c}. | - |where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter - | ^² refers to a fresh root capability classified as Mutable in the result type of method mkCounter + |where: ^ refers to a fresh root capability in the result type of method mkCounter + | ^² refers to a fresh root capability in the result type of method mkCounter | cap is a fresh root capability classified as Mutable in the type of value c | cap² is a fresh root capability classified as Mutable created in value c when constructing instance Ref diff --git a/tests/neg-custom-args/captures/sep-curried.check b/tests/neg-custom-args/captures/sep-curried.check index a2b576de8c3a..ea32ef208b88 100644 --- a/tests/neg-custom-args/captures/sep-curried.check +++ b/tests/neg-custom-args/captures/sep-curried.check @@ -24,8 +24,8 @@ | Footprint set of second argument : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test0 when checking argument to parameter x of method foo + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test0 when checking argument to parameter x of method foo -- Error: tests/neg-custom-args/captures/sep-curried.scala:22:44 ------------------------------------------------------- 22 | val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error | ^ @@ -41,8 +41,8 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in value f when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in value f when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:29:6 -------------------------------------------------------- 29 | foo(a)(a) // error | ^ @@ -58,8 +58,8 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test2 when checking argument to parameter x of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test2 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:35:9 -------------------------------------------------------- 35 | foo(a)(a) // error | ^ @@ -75,8 +75,8 @@ | Footprint set of function prefix : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test3 when checking argument to parameter y of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test3 when checking argument to parameter y of method apply -- Error: tests/neg-custom-args/captures/sep-curried.scala:42:4 -------------------------------------------------------- 42 | f(a) // error | ^ @@ -92,5 +92,5 @@ | Footprint set of function prefix : {f, a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value a - | ^² refers to a fresh root capability classified as Mutable created in method test4 when checking argument to parameter y of method apply + |where: ^ refers to a fresh root capability in the type of value a + | ^² refers to a fresh root capability created in method test4 when checking argument to parameter y of method apply diff --git a/tests/neg-custom-args/captures/sep-list.check b/tests/neg-custom-args/captures/sep-list.check index 43ac04df02b0..5ecde5d6d2bd 100644 --- a/tests/neg-custom-args/captures/sep-list.check +++ b/tests/neg-custom-args/captures/sep-list.check @@ -13,4 +13,4 @@ | Footprint set of second argument : {h2, xs*} | The two sets overlap at : {xs*} | - |where: ^ refers to a fresh root capability classified as Mutable created in method test when checking argument to parameter x of method par + |where: ^ refers to a fresh root capability created in method test when checking argument to parameter x of method par diff --git a/tests/neg-custom-args/captures/sep-pairs-unboxed.check b/tests/neg-custom-args/captures/sep-pairs-unboxed.check index 5baf11b03ec4..ff0d2237dd2d 100644 --- a/tests/neg-custom-args/captures/sep-pairs-unboxed.check +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.check @@ -13,8 +13,8 @@ | Footprint set of second argument : {x} | The two sets overlap at : {x} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x - | ^² refers to a fresh root capability classified as Mutable created in method mkPair when checking argument to parameter fst of constructor Pair + |where: ^ refers to a fresh root capability in the type of parameter x + | ^² refers to a fresh root capability created in method mkPair when checking argument to parameter fst of constructor Pair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:35:25 ------------------------------------------------- 35 | val twoCopy = Pair(two.fst, two.fst) // error | ^^^^^^^ @@ -30,8 +30,8 @@ | Footprint set of second argument : {two.fst} | The two sets overlap at : {two.fst} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst - | ^² refers to a fresh root capability classified as Mutable created in value twoCopy when checking argument to parameter fst of constructor Pair + |where: ^ refers to a fresh root capability in the type of value fst + | ^² refers to a fresh root capability created in value twoCopy when checking argument to parameter fst of constructor Pair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:41:29 ------------------------------------------------- 41 | val twisted = PairPair(two.fst, two) // error | ^^^^^^^ @@ -39,7 +39,7 @@ |to constructor PairPair: (fst: Ref^, snd: Pair^): PairPair |corresponds to capture-polymorphic formal parameter fst of type Ref^² |and hides capabilities {two.fst}. - |Some of these overlap with the captures of the second argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). + |Some of these overlap with the captures of the second argument with type Pair{val fst: Ref^{two*}; val snd: Ref^{two*}}^{two}. | | Hidden set of current argument : {two.fst} | Hidden footprint of current argument : {two.fst} @@ -47,8 +47,8 @@ | Footprint set of second argument : {two*} | The two sets overlap at : {cap of a new instance of class Pair} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst - | ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter fst of constructor PairPair + |where: ^ refers to a fresh root capability in the type of value fst + | ^² refers to a fresh root capability created in value twisted when checking argument to parameter fst of constructor PairPair -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:33 ------------------------------------------------- 47 | val twisted = swapped(two, two.snd) // error | ^^^^^^^ @@ -56,7 +56,7 @@ |to method swapped: (@consume x: Pair^, @consume y: Ref^): PairPair^ |corresponds to capture-polymorphic formal parameter y of type Ref^² |and hides capabilities {two.snd}. - |Some of these overlap with the captures of the first argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). + |Some of these overlap with the captures of the first argument with type Pair{val fst: Ref^{two*}; val snd: Ref^{two*}}^{two}. | | Hidden set of current argument : {two.snd} | Hidden footprint of current argument : {two.snd} @@ -64,8 +64,8 @@ | Footprint set of first argument : {two*} | The two sets overlap at : {cap of a new instance of class Pair} | - |where: ^ refers to a fresh root capability classified as Mutable in the type of value snd - | ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter y of method swapped + |where: ^ refers to a fresh root capability in the type of value snd + | ^² refers to a fresh root capability created in value twisted when checking argument to parameter y of method swapped -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:26 ------------------------------------------------- 58 | val twoOther = Pair(two.fst, two.snd) // error // error | ^^^^^^^ diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check index d51870f3eedf..6005eb1a49e6 100644 --- a/tests/neg-custom-args/captures/sep-pairs.check +++ b/tests/neg-custom-args/captures/sep-pairs.check @@ -6,8 +6,8 @@ | Another part, Ref^², captures capabilities {r0}. | The two sets overlap at {r0}. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value r1 - | ^² refers to a fresh root capability classified as Mutable in the type of value r1 + | where: ^ refers to a fresh root capability in the type of value r1 + | ^² refers to a fresh root capability in the type of value r1 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:13:9 ---------------------------------------------------------- 13 |def bad: Pair[Ref^, Ref^] = // error: overlap at r1*, r0 | ^^^^^^^^^^^^^^^^ @@ -16,17 +16,17 @@ | Another part, Ref^², captures capabilities {r1*, r0}. | The two sets overlap at {r1*, r0}. | - | where: ^ refers to a fresh root capability classified as Mutable in the result type of method bad - | ^² refers to a fresh root capability classified as Mutable in the result type of method bad - | cap is a fresh root capability classified as Mutable in the type of value r1 - | cap² is a fresh root capability classified as Mutable in the type of value r1 + | where: ^ refers to a fresh root capability in the result type of method bad + | ^² refers to a fresh root capability in the result type of method bad + | cap is a fresh root capability in the type of value r1 + | cap² is a fresh root capability in the type of value r1 -- Error: tests/neg-custom-args/captures/sep-pairs.scala:43:18 --------------------------------------------------------- 43 | val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error | ^^^^^^^^^^^^^^^^ - | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {fstSame}. - | Another part, Ref^², captures capabilities {sndSame, same.snd*}. - | The two sets overlap at {cap of value same}. + | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. + | One part, Ref^, hides capabilities {fstSame}. + | Another part, Ref^², captures capabilities {sndSame, same.snd*}. + | The two sets overlap at {cap of value same}. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value sameToPair - | ^² refers to a fresh root capability classified as Mutable in the type of value sameToPair + | where: ^ refers to a fresh root capability in the type of value sameToPair + | ^² refers to a fresh root capability in the type of value sameToPair diff --git a/tests/pos-custom-args/captures/mut-iterator.scala b/tests/pos-custom-args/captures/mut-iterator.scala new file mode 100644 index 000000000000..c019f0cc95ff --- /dev/null +++ b/tests/pos-custom-args/captures/mut-iterator.scala @@ -0,0 +1,30 @@ +import caps.{cap, Mutable, SharedCapability} + +trait Iterator[T] extends Mutable: + def hasNext: Boolean + update def next(): T + + consume def map[U](consume f: T => U): Iterator[U] = new Iterator: + def hasNext = Iterator.this.hasNext + update def next() = f(Iterator.this.next()) +end Iterator + +def listIterator[T](xs: List[T]) = new Iterator[T]: + private var current = xs + def hasNext = current.nonEmpty + update def next() = xs.runtimeChecked match + case x :: xs1 => + current = xs1 + x + +def mappedIterator[T, U](consume it: Iterator[T]^, consume f: T => U): Iterator[U] = new Iterator: + def hasNext = it.hasNext + update def next() = f(it.next()) + +class IO extends SharedCapability: + def write(x: Any): Unit = () + +def test(io: IO) = + listIterator(List(1, 2, 3)).map: i => + io.write(i) + i * i diff --git a/tests/pos-custom-args/captures/restrict-try.scala b/tests/pos-custom-args/captures/restrict-try.scala index fc2a09ecb535..b6be00f69fd7 100644 --- a/tests/pos-custom-args/captures/restrict-try.scala +++ b/tests/pos-custom-args/captures/restrict-try.scala @@ -1,11 +1,11 @@ -import caps.{SharedCapability, Control, Mutable} +import caps.{SharedCapability, Control, Read} class Try[+T] case class Ok[T](x: T) extends Try[T] case class Fail(ex: Exception) extends Try[Nothing] -trait Matrix extends Mutable: - update def update(): Unit +trait Matrix extends Read: + def get(): Unit trait Label extends Control: def break(): Unit @@ -19,7 +19,7 @@ def Test(m: Matrix^, l: Label) = val x = Try: val b = () => - m.update() + m.get() l.break() val _: () ->{m, l} Unit = b b From 747f2de251fd7f6c23f525fdfb62c7d611a4f5e9 Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 7 Nov 2025 10:12:42 +0100 Subject: [PATCH 02/12] Use @untrackedCaptures instead of transparent --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- .../src/dotty/tools/dotc/cc/Mutability.scala | 14 +++++++---- .../capture-checking/mutability.md | 25 +++++++++++-------- .../captures/lazyref-mutvar.scala | 6 +++-- ...-mutvars.scala => untracked-mutvars.scala} | 3 ++- 5 files changed, 30 insertions(+), 20 deletions(-) rename tests/pos-custom-args/captures/{transparent-mutvars.scala => untracked-mutvars.scala} (91%) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 1bb4764b9206..f87ddefcc2ae 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1039,7 +1039,7 @@ class CheckCaptures extends Recheck, SymTransformer: recheck(tree.rhs, lhsType.widen) lhsType match case lhsType @ TermRef(qualType, _) - if (qualType ne NoPrefix) && !lhsType.symbol.is(Transparent) => + if (qualType ne NoPrefix) && !lhsType.symbol.hasAnnotation(defn.UntrackedCapturesAnnot) => checkUpdate(qualType, tree.srcPos)(i"Cannot assign to field ${lhsType.name} of ${qualType.showRef}") case _ => defn.UnitType diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala index 6098088f1602..7e510ffe708f 100644 --- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Mutability.scala @@ -46,13 +46,17 @@ object Mutability: end Exclusivity extension (sym: Symbol) - /** An update method is either a method marked with `update` or - * a setter of a non-transparent var. `update` is implicit for `consume` methods - * of Mutable classes. + /** An update method is either a method marked with `update` or a setter + * of a field of a Mutable class that's not annotated with @uncheckedCaptures. + * `update` is implicit for `consume` methods of Mutable classes. */ def isUpdateMethod(using Context): Boolean = sym.isAllOf(Mutable | Method) - && (!sym.isSetter || sym.field.is(Transparent)) + && (if sym.isSetter then + sym.owner.derivesFrom(defn.Caps_Mutable) + && !sym.field.hasAnnotation(defn.UntrackedCapturesAnnot) + else true + ) /** A read-only method is a real method (not an accessor) in a type extending * Mutable that is not an update method. Included are also lazy vals in such types. @@ -79,7 +83,7 @@ object Mutability: tp.derivesFrom(defn.Caps_Mutable) && tp.membersBasedOnFlags(Mutable, EmptyFlags).exists: mbr => if mbr.symbol.is(Method) then mbr.symbol.isUpdateMethod - else !mbr.symbol.is(Transparent) + else !mbr.symbol.hasAnnotation(defn.UntrackedCapturesAnnot) /** OK, except if `tp` extends `Mutable` but `tp`'s capture set is non-exclusive */ private def exclusivity(using Context): Exclusivity = diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 65b29bb2c4ce..23188f73f251 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -283,31 +283,34 @@ ro.set(22) // disallowed, since `ro` is read-only access ``` -## Transparent Vars +## Untracked Vars Sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance: ```scala +import caps.unsafe.untrackedCaptures + class Cache[T](eval: () -> T): - private transparent var x: T = compiletime.uninitialized - private transparent var known = false + @untrackedCaptures private var x: T = compiletime.uninitialized + @untrackedCaptures private var known = false def force: T = if !known then x = eval() known = true x ``` -Here, the mutable field `x` is used to store the result of a pure function `eval`. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is -evaluated at most once. So from a semantic standpoint, it should not be necessary to make `force` an update method, even though it does assign to `x`. +Note that, even though `Cache` has mutable variables, it is not declared as a `Mutable` class. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is evaluated at most once. So from a semantic standpoint, it should not be necessary to make `force` an update method, even though it does assign to `x`. + +We can avoid the need for update methods by annotating mutable fields with `@untrackedCaptures`. Assignments to untracked mutable field are then not checked for read-only restrictions. The `@untrackedCaptures` annotation can be imported from the `scala.caps.unsafe` object. It is up to the developer +to use `@untrackedCaptures` responsibly so that it does not hide visible side effects on mutable state. -We can avoid the need for update methods by declaring mutable fields `transparent`. Assignments to `transparent` mutable field are not checked for read-only restrictions. It is up to the developer -to use `transparent` responsibly so that it does not hide visible side effects on mutable state. +Note that at the moment an assignment to a variable is restricted _only_ if the variable is a field of a `Mutable` class. Fields of other classes and local variables are currently not checked. So the `Cache` class above would in fact +currently compile without the addition of `@untrackedCaptures`. -Note that an assignment to a variable is restricted only if the variable is a field of a `Mutable` class. Fields of other classes and local variables are currently not checked. +But is planned to tighten the rules in the future so that mutable fields that are not annotated with `@untrackedCaptures` can be declared only in classes extending `Mutable`. This means that all assignments to mutable fields would be checked with the read-only restriction, and `@untrackedCapture`s would become essential as an escape hatch. -It is planned to tighten the rules in the future so that non-transparent mutable fields can be declared only in classes extending `Mutable`. This means that all assignments to mutable fields would be checked with the read-only restriction, and `transparent` would become essential as -an escape hatch. +By contrast, it is not planned to check assignments to local mutable variables, which are not fields of some class. So `@untrackedCaptures` is disallowed for such local variables. -By contrast, it is not planned to check assignments to local mutable variables, which are not fields of some class. So `transparent` is disallowed for such local variables. +The `untrackedCaptures` annotation can also be used in some other contexts unrelated to mutable variables. These are described in its [doc comment](https://www.scala-lang.org/api/current/scala/caps/unsafe$$untrackedCaptures.html). ## Read-Only Capsets diff --git a/tests/pos-custom-args/captures/lazyref-mutvar.scala b/tests/pos-custom-args/captures/lazyref-mutvar.scala index 541f8da94595..e071ad4ef0b0 100644 --- a/tests/pos-custom-args/captures/lazyref-mutvar.scala +++ b/tests/pos-custom-args/captures/lazyref-mutvar.scala @@ -1,7 +1,9 @@ import compiletime.uninitialized +import caps.unsafe.untrackedCaptures + class LazyRef[T](val mkElem: () => T): - transparent var elem: T = uninitialized - transparent var evaluated = false + @untrackedCaptures var elem: T = uninitialized + @untrackedCaptures var evaluated = false def get: T = if !evaluated then elem = mkElem() diff --git a/tests/pos-custom-args/captures/transparent-mutvars.scala b/tests/pos-custom-args/captures/untracked-mutvars.scala similarity index 91% rename from tests/pos-custom-args/captures/transparent-mutvars.scala rename to tests/pos-custom-args/captures/untracked-mutvars.scala index 6ccc3517fe85..3810217eac67 100644 --- a/tests/pos-custom-args/captures/transparent-mutvars.scala +++ b/tests/pos-custom-args/captures/untracked-mutvars.scala @@ -1,5 +1,6 @@ +import caps.unsafe.untrackedCaptures class Ref[T](init: T) extends caps.Mutable: - transparent var fld: T = init + @untrackedCaptures var fld: T = init def hide(x: T) = this.fld = x // ok update def hide2(x: T) = this.fld = x // ok From 78507ddd88c20f13d28f429a72e2bc5021f04077 Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 7 Nov 2025 10:35:23 +0100 Subject: [PATCH 03/12] Update doc pages --- .../experimental/capture-checking/classifiers.md | 15 +++++++++------ .../experimental/capture-checking/mutability.md | 11 +++++------ 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/classifiers.md b/docs/_docs/reference/experimental/capture-checking/classifiers.md index bbba42c37da9..0890725b83e0 100644 --- a/docs/_docs/reference/experimental/capture-checking/classifiers.md +++ b/docs/_docs/reference/experimental/capture-checking/classifiers.md @@ -45,10 +45,10 @@ sealed trait Capability trait SharedCapability extends Capability Classifier trait Control extends SharedCapability, Classifier -trait ExclusiveCapability extends Capability, Classifier -trait Mutable extends ExclusiveCapability, Classifier +trait ExclusiveCapability extends Capability +trait Read extends ExclusiveCapability, Classifier ``` -Here is a graph showing the hierarchy of predefined classifier traits: +Here is a graph showing the hierarchy of predefined capability traits. Classifier traits are underlined. ``` Capability / \ @@ -56,14 +56,17 @@ Here is a graph showing the hierarchy of predefined classifier traits: / \ / \ SharedCapability ExclusiveCapability + ---------------- | | | | | | | | - Control Mutable + Control Read + ------- ---- ``` -At the top of the hierarchy, we distinguish between _shared_ and _exclusive_ capabilities in two classifier traits `SharedCapability` and `ExclusiveCapability`. All capability classes we have seen so far are shared. -`ExclusiveCapability` is a base trait for capabilities that allow only un-aliased access to the data they represent, with the rules governed by [separation checking](separation-checking.md). Separation checking is currently an optional extension of capture checking, enabled by a different language import. Since `Capability` is a sealed trait, all capability classes are either shared or exclusive. +At the top of the hierarchy, we distinguish between _shared_ and _exclusive_ capabilities in two traits `SharedCapability` and `ExclusiveCapability`. All capability classes we have seen so far are shared. +`ExclusiveCapability` is a base trait for capabilities that +are checked for anti-aliasing restrictions with the rules governed by [separation checking](separation-checking.md). Separation checking is currently an optional extension of capture checking, enabled by a different language import. Since `Capability` is a sealed trait, all capability classes are either shared or exclusive. `Control` capabilities are shared. This means they cannot directly or indirectly capture exclusive capabilities such as capabilities that control access to mutable state. Typical `Control` capabilities are: diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 23188f73f251..177dc7e18a23 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -31,9 +31,9 @@ A capability is called We introduce a new trait ```scala -trait Mutable extends ExclusiveCapability, Classifier +trait Mutable ``` -It is used as a [classifier](classifiers.md) trait for types that define mutable variables and/or _update methods_. +It is used as a marker trait for types that define mutable variables and/or _update methods_. ## Update Methods @@ -134,10 +134,9 @@ a method that accesses exclusive capabilities. If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated _read-only_ capability. It counts as a shared capability. A read-only capability does not permit access to the mutable fields of a matrix. -A read-only capability can be seen as a classified capability -using a classifier trait `Read` that extends `Mutable`. I.e. -`x.rd` can be seen as being essentially the same as `x.only[Read]`. -(Currently, this precise equivalence is still waiting to be implemented.) +A read-only capability can be seen as a [classified](classifiers.md) capability +using a classifier trait `Read`. I.e. +`x.rd` is a shorthand for `x.only[Read]`. **Implicitly added capture sets** From 9f0adf6a30ef06fbf429be32f7251396cb5584bd Mon Sep 17 00:00:00 2001 From: odersky Date: Sat, 8 Nov 2025 15:19:31 +0100 Subject: [PATCH 04/12] Improvements to read-only handling - Allow to charge read-only set on unboxing (previously it was always the exclusive set that was charged). - Treat also methods outside Mutable types as read-only members. Previously we charged read-only when calling a read-only method of a mutable type, but not when calling an inherited method such as `eq`. - Use the same criterion for read-only everywhere. - Distinguish between read- and write-accesses to mutable fields. --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 7 +- .../dotty/tools/dotc/cc/CheckCaptures.scala | 80 ++++++++++--------- .../src/dotty/tools/dotc/cc/Mutability.scala | 25 +++--- .../tools/dotc/printing/RefinedPrinter.scala | 2 + .../neg-custom-args/captures/var-access.check | 18 +++++ .../neg-custom-args/captures/var-access.scala | 18 +++++ .../captures/mark-free-ro.scala | 13 +++ 7 files changed, 114 insertions(+), 49 deletions(-) create mode 100644 tests/neg-custom-args/captures/var-access.check create mode 100644 tests/neg-custom-args/captures/var-access.scala create mode 100644 tests/pos-custom-args/captures/mark-free-ro.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index ca55fef08758..45177b8c45ba 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -15,7 +15,8 @@ import CaptureSet.VarState import Capabilities.* import StdNames.nme import config.Feature -import dotty.tools.dotc.core.NameKinds.TryOwnerName +import NameKinds.TryOwnerName +import typer.ProtoTypes.WildcardSelectionProto /** Attachment key for capturing type trees */ private val Captures: Key[CaptureSet] = Key() @@ -639,6 +640,10 @@ extension (tp: AnnotatedType) case ann: CaptureAnnotation => ann.boxed case _ => false +/** A prototype that indicates selection */ +class PathSelectionProto(val select: Select, val pt: Type) extends typer.ProtoTypes.WildcardSelectionProto: + def selector(using Context): Symbol = select.symbol + /** Drop retains annotations in the inferred type if CC is not enabled * or transform them into RetainingTypes if CC is enabled. */ diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index f87ddefcc2ae..ec7fb036729d 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -103,9 +103,6 @@ object CheckCaptures: override def toString = "SubstParamsMap" end SubstParamsMap - /** A prototype that indicates selection with an immutable value */ - class PathSelectionProto(val select: Select, val pt: Type)(using Context) extends WildcardSelectionProto - /** Check that a @retains annotation only mentions references that can be tracked. * This check is performed at Typer. */ @@ -598,7 +595,10 @@ class CheckCaptures extends Recheck, SymTransformer: if !isOfNestedMethod(env) then val nextEnv = nextEnvToCharge(env) if nextEnv != null && !nextEnv.owner.isStaticOwner then - if env.owner.isReadOnlyMethodOrLazyVal && nextEnv.owner != env.owner then + if nextEnv.owner != env.owner + && env.owner.isReadOnlyMember + && env.owner.owner.derivesFrom(defn.Caps_Mutable) + then checkReadOnlyMethod(included, env.owner) recur(included, nextEnv, env) // Under deferredReaches, don't propagate out of methods inside terms. @@ -705,29 +705,23 @@ class CheckCaptures extends Recheck, SymTransformer: * where `b` is a read-only method, we charge `x.a.b.rd` for tree `x.a.b` * instead of just charging `x`. */ - private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = - pt match - case pt: PathSelectionProto if ref.isTracked => - // if `ref` is not tracked then the selection could not give anything new - // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. - if pt.select.symbol.isReadOnlyMethodOrLazyVal then - markFree(ref.readOnly, tree) - else - val sel = ref.select(pt.select.symbol).asInstanceOf[TermRef] - markPathFree(sel, pt.pt, pt.select) - case _ => - markFree(ref.adjustReadOnly(pt), tree) + private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = pt match + case pt: PathSelectionProto + if ref.isTracked && !pt.selector.isOneOf(MethodOrLazyOrMutable) => + // if `ref` is not tracked then the selection could not give anything new + // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. + val sel = ref.select(pt.selector).asInstanceOf[TermRef] + markPathFree(sel, pt.pt, pt.select) + case _ => + markFree(ref.adjustReadOnly(pt), tree) /** The expected type for the qualifier of a selection. If the selection * could be part of a capability path or is a a read-only method, we return * a PathSelectionProto. */ override def selectionProto(tree: Select, pt: Type)(using Context): Type = - val sym = tree.symbol - if !sym.isOneOf(MethodOrLazyOrMutable) && !sym.isStatic - || sym.isReadOnlyMethodOrLazyVal - then PathSelectionProto(tree, pt) - else super.selectionProto(tree, pt) + if tree.symbol.isStatic then super.selectionProto(tree, pt) + else PathSelectionProto(tree, pt) /** A specialized implementation of the selection rule. * @@ -1131,21 +1125,30 @@ class CheckCaptures extends Recheck, SymTransformer: try if sym.is(Module) then sym.info // Modules are checked by checking the module class else - if sym.is(Mutable) && !sym.hasAnnotation(defn.UncheckedCapturesAnnot) then - val addendum = setup.capturedBy.get(sym) match - case Some(encl) => - val enclStr = - if encl.isAnonymousFunction then - val location = setup.anonFunCallee.get(encl) match - case Some(meth) if meth.exists => i" argument in a call to $meth" - case _ => "" - s"an anonymous function$location" - else encl.show - i"\n\nNote that $sym does not count as local since it is captured by $enclStr" - case _ => - "" - disallowBadRootsIn( - tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos) + if sym.is(Mutable) then + if !sym.hasAnnotation(defn.UncheckedCapturesAnnot) then + val addendum = setup.capturedBy.get(sym) match + case Some(encl) => + val enclStr = + if encl.isAnonymousFunction then + val location = setup.anonFunCallee.get(encl) match + case Some(meth) if meth.exists => i" argument in a call to $meth" + case _ => "" + s"an anonymous function$location" + else encl.show + i"\n\nNote that $sym does not count as local since it is captured by $enclStr" + case _ => + "" + disallowBadRootsIn( + tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos) + if sepChecksEnabled && false + && sym.owner.isClass + && !sym.owner.derivesFrom(defn.Caps_Mutable) + && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) then + report.error( + em"""Mutable $sym is defined in a class that does not extend `Mutable`. + |The variable needs to be annotated with `untrackedCaptures` to allow this.""", + tree.namePos) // Lazy vals need their own environment to track captures from their RHS, // similar to how methods work @@ -1793,7 +1796,10 @@ class CheckCaptures extends Recheck, SymTransformer: if needsAdaptation && !insertBox then // we are unboxing val criticalSet = // the set with which we unbox - if covariant then captures // covariant: we box with captures of actual type plus captures leaked by inner adapation + if covariant then + if expected.expectsReadOnly && actual.derivesFromMutable + then captures.readOnly + else captures else expected.captureSet // contravarant: we unbox with captures of epected type //debugShowEnvs() markFree(criticalSet, tree) diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala index 7e510ffe708f..3d1a9e75b3fd 100644 --- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Mutability.scala @@ -8,6 +8,7 @@ import Capabilities.* import util.SrcPos import config.Printers.capt import ast.tpd.Tree +import typer.ProtoTypes.LhsProto /** Handling mutability and read-only access */ @@ -58,12 +59,9 @@ object Mutability: else true ) - /** A read-only method is a real method (not an accessor) in a type extending - * Mutable that is not an update method. Included are also lazy vals in such types. - */ - def isReadOnlyMethodOrLazyVal(using Context): Boolean = - sym.isOneOf(MethodOrLazy, butNot = Mutable | Accessor) - && sym.owner.derivesFrom(defn.Caps_Mutable) + /** A read-only member is a lazy val or a method that is not an update method. */ + def isReadOnlyMember(using Context): Boolean = + sym.isOneOf(MethodOrLazy) && !sym.isUpdateMethod private def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity = import Exclusivity.* @@ -104,19 +102,25 @@ object Mutability: case _ => tp.exclusivity + def expectsReadOnly(using Context): Boolean = tp match + case tp: PathSelectionProto => + tp.selector.isReadOnlyMember || tp.selector.isMutableVar && tp.pt != LhsProto + case _ => tp.isValueType && !tp.isMutableType + extension (cs: CaptureSet) private def exclusivity(tp: Type)(using Context): Exclusivity = if cs.isExclusive then Exclusivity.OK else Exclusivity.ReadOnly(tp) extension (ref: TermRef | ThisType) /** Map `ref` to `ref.readOnly` if its type extends Mutble, and one of the - * following is true: it appears in a non-exclusive context, or the expected - * type is a value type that is not a mutable type. + * following is true: + * - it appears in a non-exclusive context, + * - 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 = if ref.derivesFromMutable - && (pt.isValueType && !pt.isMutableType - || ref.exclusivityInContext != Exclusivity.OK) + && (pt.expectsReadOnly || ref.exclusivityInContext != Exclusivity.OK) then ref.readOnly else ref @@ -148,7 +152,6 @@ object Mutability: && expected.isValueType && (!expected.derivesFromMutable || expected.captureSet.isAlwaysReadOnly) && !expected.isSingleton - && actual.isBoxedCapturing == expected.isBoxedCapturing then refs.readOnly else refs actual.derivedCapturingType(parent1, refs1) diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala index b8de2c7a9115..44aa7c19b6d5 100644 --- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala @@ -333,6 +333,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { case tp: LazyRef if !printDebug => try toText(tp.ref) catch case ex: Throwable => "..." + case sel: cc.PathSelectionProto => + "?.{ " ~ toText(sel.select.symbol) ~ "}" case AnySelectionProto => "a type that can be selected or applied" case tp: SelectionProto => diff --git a/tests/neg-custom-args/captures/var-access.check b/tests/neg-custom-args/captures/var-access.check new file mode 100644 index 000000000000..63028ba807cc --- /dev/null +++ b/tests/neg-custom-args/captures/var-access.check @@ -0,0 +1,18 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/var-access.scala:9:21 ------------------------------------ +9 | val _: () -> Int = f // error + | ^ + | Found: (f : () ->{a.rd} Int) + | Required: () -> Int + | + | Note that capability a.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/var-access.scala:12:22 ----------------------------------- +12 | val _: () -> Unit = g // error + | ^ + | Found: (g : () ->{a} Unit) + | Required: () -> Unit + | + | Note that capability a is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/var-access.scala b/tests/neg-custom-args/captures/var-access.scala new file mode 100644 index 000000000000..c3d5a2cab50c --- /dev/null +++ b/tests/neg-custom-args/captures/var-access.scala @@ -0,0 +1,18 @@ +import caps.* +class A extends Mutable: + var x: Int = 0 + +def test = + val a = A() + val f = () => a.x + val _: () ->{a.rd} Int = f + val _: () -> Int = f // error + val g = () => a.x += 1 + val _: () ->{a} Unit = g + val _: () -> Unit = g // error + + + + + + diff --git a/tests/pos-custom-args/captures/mark-free-ro.scala b/tests/pos-custom-args/captures/mark-free-ro.scala new file mode 100644 index 000000000000..625b6ba7813c --- /dev/null +++ b/tests/pos-custom-args/captures/mark-free-ro.scala @@ -0,0 +1,13 @@ +import caps.{cap, Mutable} +import caps.unsafe.untrackedCaptures + +class Test extends Mutable: + var ctxStack: Array[FreshCtx^] = new Array(10) + + class FreshCtx(level: Int) extends Mutable: + this: FreshCtx^ => + def detached: Boolean = + val c: FreshCtx^{cap.rd} = ctxStack(level) + (c eq this) + def detached2 = + ctxStack(level) eq this From d40f1f907e82ce71dd5dcf210917c621f10d82d0 Mon Sep 17 00:00:00 2001 From: odersky Date: Sat, 8 Nov 2025 20:06:43 +0100 Subject: [PATCH 05/12] Also drop read-only versions of shared capabilities from separation checking We do get sometimes capabilities like `async.rd` where `async` is shared. It does not look straightforward to prevent that, so instead we count async.rd as shared if async is. --- .../src/dotty/tools/dotc/cc/SepCheck.scala | 4 ++-- tests/pos-custom-args/captures/ro-array.scala | 22 +++++++++++++++++++ 2 files changed, 24 insertions(+), 2 deletions(-) create mode 100644 tests/pos-custom-args/captures/ro-array.scala diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index b98f07080181..a40e7699c953 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -638,7 +638,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val badParams = mutable.ListBuffer[Symbol]() def currentOwner = role.dclSym.orElse(ctx.owner) for hiddenRef <- refsToCheck.deduct(explicitRefs(tpe)) do - if !hiddenRef.isKnownClassifiedAs(defn.Caps_SharedCapability) then + if !hiddenRef.stripReadOnly.isKnownClassifiedAs(defn.Caps_SharedCapability) then hiddenRef.pathRoot match case ref: TermRef if ref.symbol != role.dclSym => val refSym = ref.symbol @@ -675,7 +675,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: role match case _: TypeRole.Argument | _: TypeRole.Qualifier => for ref <- refsToCheck do - if !ref.isKnownClassifiedAs(defn.Caps_SharedCapability) then + if !ref.stripReadOnly.isKnownClassifiedAs(defn.Caps_SharedCapability) then consumed.put(ref, pos) case _ => end checkConsumedRefs diff --git a/tests/pos-custom-args/captures/ro-array.scala b/tests/pos-custom-args/captures/ro-array.scala new file mode 100644 index 000000000000..002410e2afd4 --- /dev/null +++ b/tests/pos-custom-args/captures/ro-array.scala @@ -0,0 +1,22 @@ +import caps.* +object Test + +class Arr[T: reflect.ClassTag](a: Async, len: Int) extends Mutable: + private val arr: Array[T] = new Array[T](len) + def get(i: Int): T = arr(i) + update def set(i: Int, x: T): Unit = arr(i) = x + +class Async extends SharedCapability + +def f[T](x: T): T & Pure = x.asInstanceOf[T & Pure] + +def test = + def x(async: Async): Arr[String]^{cap.rd} = + val y = Arr[String](async, 10) + for i <- 0 to 10 do + y.set(i, "A") + val z = f(y) + y + + + From cf54d1dace6902b45f3f03817e916d47026e34af Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 10 Nov 2025 10:58:01 +0100 Subject: [PATCH 06/12] Don't drop empty capture sets of capability classes We need a way to distinguish C^{} and C^{cap} when printing. We print C^{cap} as C is C is a capability class. --- compiler/src/dotty/tools/dotc/cc/CapturingType.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala index de694b38f11e..d267a3b12a76 100644 --- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala +++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala @@ -34,7 +34,8 @@ object CapturingType: */ def apply(parent: Type, refs: CaptureSet, boxed: Boolean = false)(using Context): Type = assert(!boxed || !parent.derivesFrom(defn.Caps_CapSet)) - if refs.isAlwaysEmpty && !refs.keepAlways then parent + if refs.isAlwaysEmpty && !refs.keepAlways && !parent.derivesFromCapability then + parent else parent match case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed => apply(parent1, refs ++ refs1, boxed) From d1d47003221e45d92be8ff17b38cc4987f5e96b9 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 10 Nov 2025 11:31:57 +0100 Subject: [PATCH 07/12] Fix wrong parens in compareCapturing test This fix removed quite a few spurious error notes. --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 4 ++-- tests/neg-custom-args/captures/lazyvals-sep.check | 4 ---- tests/neg-custom-args/captures/linear-buffer.check | 2 -- tests/neg-custom-args/captures/mutability.check | 8 -------- tests/neg-custom-args/captures/mutvars.check | 8 -------- tests/neg-custom-args/captures/ro-mut-conformance.check | 2 -- 6 files changed, 2 insertions(+), 26 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 77fdc24a01cc..5c578570eb5f 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2913,8 +2913,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling errorNotes = (level, CaptureSet.MutAdaptFailure(cs, tp1, tp2)) :: rest case _ => subc - && (tp1.isBoxedCapturing == tp2.isBoxedCapturing) - || refs1.subCaptures(CaptureSet.empty, makeVarState()) + && (tp1.isBoxedCapturing == tp2.isBoxedCapturing + || refs1.subCaptures(CaptureSet.empty, makeVarState())) protected def logUndoAction(action: () => Unit) = undoLog += action diff --git a/tests/neg-custom-args/captures/lazyvals-sep.check b/tests/neg-custom-args/captures/lazyvals-sep.check index 0d01da2c2f30..e859829e1f3b 100644 --- a/tests/neg-custom-args/captures/lazyvals-sep.check +++ b/tests/neg-custom-args/captures/lazyvals-sep.check @@ -29,8 +29,6 @@ |Found: Ref^{TestClass.this.r.rd} |Required: Ref^ | - |Note that capability TestClass.this.r.rd is not included in capture set {}. - | |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 Ref^{TestClass.this.r.rd}. | @@ -43,8 +41,6 @@ |Found: Ref^{TestClass.this.r.rd} |Required: Ref^ | - |Note that capability TestClass.this.r.rd is not included in capture set {}. - | |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 Ref^{TestClass.this.r.rd}. | diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 549adb55a351..928e0926612d 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -4,8 +4,6 @@ | Found: BadBuffer[T]^{BadBuffer.this.rd} | Required: BadBuffer[T]^ | - | Note that capability BadBuffer.this.rd is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^, | it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}. | diff --git a/tests/neg-custom-args/captures/mutability.check b/tests/neg-custom-args/captures/mutability.check index c4da68169ce8..57a5825940cf 100644 --- a/tests/neg-custom-args/captures/mutability.check +++ b/tests/neg-custom-args/captures/mutability.check @@ -14,8 +14,6 @@ | Found: Ref[T]^{Ref.this.rd} | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | @@ -40,8 +38,6 @@ | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} | Required: () => Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. | @@ -67,8 +63,6 @@ | Found: Ref[T]^{Ref.this.rd} | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | @@ -103,8 +97,6 @@ | Found: () ->{ref2.rd} Ref2[Int]^{ref2} | Required: () => Ref2[Int]^ | - | Note that capability ref2 is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. | diff --git a/tests/neg-custom-args/captures/mutvars.check b/tests/neg-custom-args/captures/mutvars.check index 76cf79f25987..f033b604e261 100644 --- a/tests/neg-custom-args/captures/mutvars.check +++ b/tests/neg-custom-args/captures/mutvars.check @@ -14,8 +14,6 @@ | Found: Ref[T]^{Ref.this.rd} | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | @@ -33,8 +31,6 @@ | Found: () ->{Ref.this.rd} Ref[T^'s1]^{Ref.this.rd} | Required: () => Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, | it cannot subsume a read-only capture set of the mutable type Ref[T^'s1]^{Ref.this.rd}. | @@ -53,8 +49,6 @@ | Found: Ref[T]^{Ref.this.rd} | Required: Ref[T]^ | - | Note that capability Ref.this.rd is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref[T]^, | it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}. | @@ -82,8 +76,6 @@ | Found: () ->{ref2.rd} Ref2[Int]^{ref2} | Required: () => Ref2[Int]^ | - | Note that capability ref2 is not included in capture set {}. - | | Note that {cap} is an exclusive capture set of the mutable type Ref2[Int]^, | it cannot subsume a read-only capture set of the mutable type Ref2[Int]^{ref2}. | diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 153fd5458ba6..169f8f3ef5b9 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -9,8 +9,6 @@ | Found: (a : Ref) | Required: Ref^ | - | Note that capability a is not included in capture set {}. - | | 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). | From 410a777274aca9e77238dd86a571db8c11aaebc1 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 10 Nov 2025 15:11:15 +0100 Subject: [PATCH 08/12] Update mutatibility status only in open VarStates --- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 2 +- tests/neg-custom-args/captures/linear-buffer.check | 7 ++++++- tests/neg-custom-args/captures/linear-buffer.scala | 2 +- tests/neg-custom-args/captures/mutability.check | 14 ++++++++++++-- tests/neg-custom-args/captures/mutability.scala | 4 ++-- tests/neg-custom-args/captures/mutvars.check | 14 ++++++++++++-- tests/neg-custom-args/captures/mutvars.scala | 4 ++-- .../captures/ro-mut-conformance.check | 10 +++++++++- .../captures/ro-mut-conformance.scala | 2 +- .../pos-custom-args/captures/consume-shared.scala | 9 +++++++++ 10 files changed, 55 insertions(+), 13 deletions(-) create mode 100644 tests/pos-custom-args/captures/consume-shared.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 6ee57a058799..0003316ed9ba 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/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") diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 928e0926612d..65c7fe81b135 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/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 | ^^^^ diff --git a/tests/neg-custom-args/captures/linear-buffer.scala b/tests/neg-custom-args/captures/linear-buffer.scala index 9c2f3075bc12..f85d9ef52dba 100644 --- a/tests/neg-custom-args/captures/linear-buffer.scala +++ b/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 diff --git a/tests/neg-custom-args/captures/mutability.check b/tests/neg-custom-args/captures/mutability.check index 57a5825940cf..2b498c823f57 100644 --- a/tests/neg-custom-args/captures/mutability.check +++ b/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. diff --git a/tests/neg-custom-args/captures/mutability.scala b/tests/neg-custom-args/captures/mutability.scala index 220c584d745e..cc419241982c 100644 --- a/tests/neg-custom-args/captures/mutability.scala +++ b/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: diff --git a/tests/neg-custom-args/captures/mutvars.check b/tests/neg-custom-args/captures/mutvars.check index f033b604e261..7f7a1ee83681 100644 --- a/tests/neg-custom-args/captures/mutvars.check +++ b/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. diff --git a/tests/neg-custom-args/captures/mutvars.scala b/tests/neg-custom-args/captures/mutvars.scala index b670b034e7fa..e77667729e8c 100644 --- a/tests/neg-custom-args/captures/mutvars.scala +++ b/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: diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 169f8f3ef5b9..3434539b10a4 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -4,7 +4,7 @@ | 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^ @@ -12,6 +12,14 @@ | 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. diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.scala b/tests/neg-custom-args/captures/ro-mut-conformance.scala index 4b3f34af47f3..019deaf0165b 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.scala +++ b/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) \ No newline at end of file diff --git a/tests/pos-custom-args/captures/consume-shared.scala b/tests/pos-custom-args/captures/consume-shared.scala new file mode 100644 index 000000000000..27c751ca84f4 --- /dev/null +++ b/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) From a737c80681df36e651b643634893851e999ca421 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 11 Nov 2025 13:54:26 +0100 Subject: [PATCH 09/12] Treat empty capture set on a Mutable type specially Needed to invalidate the relation C^{} <: C^ for Mutable types C --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 22 ++++++++++++++----- .../dotty/tools/dotc/cc/CapturingType.scala | 7 +++--- .../dotty/tools/dotc/cc/CheckCaptures.scala | 3 +++ .../dotty/tools/dotc/core/TypeComparer.scala | 3 ++- .../captures/mut-widen-empty.check | 12 ++++++++++ .../captures/mut-widen-empty.scala | 14 ++++++++++++ 6 files changed, 51 insertions(+), 10 deletions(-) create mode 100644 tests/neg-custom-args/captures/mut-widen-empty.check create mode 100644 tests/neg-custom-args/captures/mut-widen-empty.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 0003316ed9ba..1924540f678f 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -67,7 +67,7 @@ sealed abstract class CaptureSet extends Showable: * - take mutability from the set's sources (for DerivedVars) * - compute mutability on demand based on mutability of elements (for Consts) */ - def associateWithMutable()(using Context): Unit + def associateWithMutable()(using Context): CaptureSet /** Is this capture set constant (i.e. not an unsolved capture variable)? * Solved capture variables count as constant. @@ -566,9 +566,16 @@ object CaptureSet: val emptyRefs: Refs = SimpleIdentitySet.empty /** The empty capture set `{}` */ - @sharable // sharable since the set is empty, so setMutable is a no-op + @sharable // sharable since the set is empty, so mutability won't be set val empty: CaptureSet.Const = Const(emptyRefs) + /** The empty capture set `{}` of a Mutable type, with Reader status */ + @sharable // sharable since the set is empty, so mutability won't be set + val emptyOfMutable: CaptureSet.Const = + val cs = Const(emptyRefs) + cs.mutability = Mutability.Reader + cs + /** The universal capture set `{cap}` */ def universal(using Context): Const = Const(SimpleIdentitySet(GlobalCap)) @@ -623,9 +630,11 @@ object CaptureSet: private var isComplete = true - def associateWithMutable()(using Context): Unit = - if !elems.isEmpty then + def associateWithMutable()(using Context): CaptureSet = + if elems.isEmpty then emptyOfMutable + else isComplete = false // delay computation of Mutability status + this override def mutability(using Context): Mutability = if !isComplete then @@ -718,8 +727,9 @@ object CaptureSet: */ var deps: Deps = SimpleIdentitySet.empty - def associateWithMutable()(using Context): Unit = + def associateWithMutable()(using Context): CaptureSet = mutability = Mutable + this def isConst(using Context) = solved >= ccState.iterationId def isAlwaysEmpty(using Context) = isConst && elems.isEmpty @@ -1036,7 +1046,7 @@ object CaptureSet: addAsDependentTo(source) /** Mutability is same as in source, except for readOnly */ - override def associateWithMutable()(using Context): Unit = () + override def associateWithMutable()(using Context): CaptureSet = this override def mutableToReader(origin: CaptureSet)(using Context): Boolean = super.mutableToReader(origin) diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala index d267a3b12a76..879ffc368280 100644 --- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala +++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala @@ -40,9 +40,10 @@ object CapturingType: case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed => apply(parent1, refs ++ refs1, boxed) case _ => - if parent.derivesFromMutable then refs.associateWithMutable() - refs.adoptClassifier(parent.inheritedClassifier) - AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot)) + val refs1 = + if parent.derivesFromMutable then refs.associateWithMutable() else refs + refs1.adoptClassifier(parent.inheritedClassifier) + AnnotatedType(parent, CaptureAnnotation(refs1, boxed)(defn.RetainsAnnot)) /** An extractor for CapturingTypes. Capturing types are recognized if * - the annotation is a CaptureAnnotation and we are not past CheckCapturingPhase, or diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index ec7fb036729d..693966049bbb 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1484,6 +1484,9 @@ class CheckCaptures extends Recheck, SymTransformer: else trace.force(i"rechecking $tree with pt = $pt", recheckr, show = true): super.recheck(tree, pt) + catch case ex: AssertionError => + println(i"error while rechecking $tree against $pt") + throw ex finally curEnv = saved if tree.isTerm && !pt.isBoxedCapturing && pt != LhsProto then markFree(res.boxedCaptureSet, tree) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 5c578570eb5f..09bce2358582 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -862,7 +862,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling def compareCapturing: Boolean = val refs1 = tp1.captureSet try - if refs1.isAlwaysEmpty then recur(tp1, parent2) + if refs1.isAlwaysEmpty && refs1.mutability == CaptureSet.Mutability.Ignored then + recur(tp1, parent2) else // The singletonOK branch is because we sometimes have a larger capture set in a singleton // than in its underlying type. An example is `f: () -> () ->{x} T`, which might be diff --git a/tests/neg-custom-args/captures/mut-widen-empty.check b/tests/neg-custom-args/captures/mut-widen-empty.check new file mode 100644 index 000000000000..70a5622af1e6 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-widen-empty.check @@ -0,0 +1,12 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-widen-empty.scala:12:24 ------------------------------ +12 | val c: Arr[String]^ = b // error + | ^ + | Found: (b : Arr[String]^{}) + | Required: Arr[String]^ + | + | Note that {cap} is an exclusive capture set of the mutable type Arr[String]^, + | it cannot subsume a read-only capture set of the mutable type Arr[String]^{}. + | + | where: ^ and cap refer to a fresh root capability in the type of value c + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/mut-widen-empty.scala b/tests/neg-custom-args/captures/mut-widen-empty.scala new file mode 100644 index 000000000000..9e10c040a046 --- /dev/null +++ b/tests/neg-custom-args/captures/mut-widen-empty.scala @@ -0,0 +1,14 @@ +import caps.* + +class Arr[T: reflect.ClassTag](len: Int) extends Mutable: + private val arr: Array[T] = new Array[T](len) + def get(i: Int): T = arr(i) + update def update(i: Int, x: T): Unit = arr(i) = x + + +def test2 = + val a = Arr[String](2) + val b: Arr[String]^{} = ??? + val c: Arr[String]^ = b // error + c(2) = "a" // boom! + From 3674c7f77473ab08befc1a4fb4209881ad52f54d Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 11 Nov 2025 14:44:08 +0100 Subject: [PATCH 10/12] Classify SharedCapabilities as non-exclusive --- .../src/dotty/tools/dotc/cc/Capability.scala | 6 +++-- .../captures/mutable-capturing-sharable.scala | 22 +++++++++++++++++++ 2 files changed, 26 insertions(+), 2 deletions(-) create mode 100644 tests/pos-custom-args/captures/mutable-capturing-sharable.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index f58c16042ab3..31a870db9e4c 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -434,10 +434,12 @@ object Capabilities: /** An exclusive capability is a capability that derives * indirectly from a maximal capability without going through - * a read-only capability first. + * a read-only capability or a capability classified as SharedCapability first. */ final def isExclusive(using Context): Boolean = - !isReadOnly && (isTerminalCapability || captureSetOfInfo.isExclusive) + !isReadOnly + && !classifier.isSubClass(defn.Caps_SharedCapability) + && (isTerminalCapability || captureSetOfInfo.isExclusive) /** Similar to isExlusive, but also includes capabilties with capture * set variables in their info whose status is still open. diff --git a/tests/pos-custom-args/captures/mutable-capturing-sharable.scala b/tests/pos-custom-args/captures/mutable-capturing-sharable.scala new file mode 100644 index 000000000000..d3b6650f90bc --- /dev/null +++ b/tests/pos-custom-args/captures/mutable-capturing-sharable.scala @@ -0,0 +1,22 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.* +class Logger extends SharedCapability: + def log(msg: String): Unit = () +class TracedRef(logger: Logger^{cap.only[SharedCapability]}) extends Mutable: + private var _data: Int = 0 + update def set(newValue: Int): Unit = + logger.log("set") + _data = newValue + def get: Int = + logger.log("get") // error, but should it be allowed? + _data + +class TracedRef2(logger: Logger) extends Mutable: + private var _data: Int = 0 + update def set(newValue: Int): Unit = + logger.log("set") + _data = newValue + def get: Int = + logger.log("get") // error, but should it be allowed? + _data From 3371325a8374c80970890dea13143f9d15bde66c Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 11 Nov 2025 16:02:49 +0100 Subject: [PATCH 11/12] Disallow inheriting both SharedCapability and Mutable --- compiler/src/dotty/tools/dotc/cc/Capability.scala | 2 +- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- compiler/src/dotty/tools/dotc/cc/Setup.scala | 4 +++- .../captures/classified-inheritance2.check | 4 ++++ .../captures/classified-inheritance2.scala | 12 ++++++++++++ 5 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 tests/neg-custom-args/captures/classified-inheritance2.check create mode 100644 tests/neg-custom-args/captures/classified-inheritance2.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 31a870db9e4c..e0abaf100d0e 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -438,7 +438,7 @@ object Capabilities: */ final def isExclusive(using Context): Boolean = !isReadOnly - && !classifier.isSubClass(defn.Caps_SharedCapability) + && !classifier.derivesFrom(defn.Caps_SharedCapability) && (isTerminalCapability || captureSetOfInfo.isExclusive) /** Similar to isExlusive, but also includes capabilties with capture diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 693966049bbb..36b8948ba6b2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -702,7 +702,7 @@ class CheckCaptures extends Recheck, SymTransformer: * type `pt` to `ref`. Expand the marked tree accordingly to take account of * the added path. Example: * If we have `x` and the expected type says we select that with `.a.b` - * where `b` is a read-only method, we charge `x.a.b.rd` for tree `x.a.b` + * where `b` is a read-only method, we charge `x.a.rd` for tree `x.a.b` * instead of just charging `x`. */ private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = pt match diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 9c5ab335d99b..a944295d3cb7 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -952,10 +952,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: case c :: cs1 => for c1 <- cs1 do if !c.derivesFrom(c1) && !c1.derivesFrom(c) then - report.error(i"$cls inherits two unrelated classifier traits: $c and $c1", cls.srcPos) + report.error(em"$cls inherits two unrelated classifier traits: $c and $c1", cls.srcPos) recur(cs1) case Nil => recur(cls.baseClasses.filter(_.isClassifiedCapabilityClass).distinct) + if cls.derivesFrom(defn.Caps_SharedCapability) && cls.derivesFrom(defn.Caps_Mutable) then + report.error(em"$cls cannot inheit from both SharaedCapability and Mutable", cls.srcPos) // ------ Checks to run after main capture checking -------------------------- diff --git a/tests/neg-custom-args/captures/classified-inheritance2.check b/tests/neg-custom-args/captures/classified-inheritance2.check new file mode 100644 index 000000000000..49d079ee3840 --- /dev/null +++ b/tests/neg-custom-args/captures/classified-inheritance2.check @@ -0,0 +1,4 @@ +-- Error: tests/neg-custom-args/captures/classified-inheritance2.scala:4:6 --------------------------------------------- +4 |class Logger extends SharedCapability, Mutable: // error (1) does this make sense? + | ^ + | class Logger cannot inheit from both SharaedCapability and Mutable diff --git a/tests/neg-custom-args/captures/classified-inheritance2.scala b/tests/neg-custom-args/captures/classified-inheritance2.scala new file mode 100644 index 000000000000..9281d44594af --- /dev/null +++ b/tests/neg-custom-args/captures/classified-inheritance2.scala @@ -0,0 +1,12 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.* +class Logger extends SharedCapability, Mutable: // error (1) does this make sense? + private var _state: Int = 0 + update def log(msg: String): Unit = () + +def onlyShared(x: Object^{cap.only[SharedCapability]}): Unit = () + +def main(): Unit = + onlyShared(Logger()) // even if we allow (1), why would this type check? + val t: Logger^{} = Logger() // and this type checks too, thus the above line I guess \ No newline at end of file From bdecf4be86473d3e7bf9a2ebba7034dfe55a6586 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 13 Nov 2025 10:02:42 +0100 Subject: [PATCH 12/12] Explain read-only consumes - New section in separation checking doc page - Slight generalization of expectsReadOnly - Lots of tests variations of #24373 --- .../src/dotty/tools/dotc/cc/Mutability.scala | 7 ++- .../capture-checking/separation-checking.md | 32 ++++++++++++ tests/neg-custom-args/captures/i24373.check | 24 +++++++++ tests/neg-custom-args/captures/i24373.scala | 52 +++++++++++++++++++ tests/neg-custom-args/captures/i24373a.check | 44 ++++++++++++++++ tests/neg-custom-args/captures/i24373a.scala | 34 ++++++++++++ tests/neg-custom-args/captures/i24373b.check | 5 ++ .../captures/linear-buffer.check | 34 +++++++----- .../captures/linear-buffer.scala | 12 +++++ tests/neg/i24375.scala | 2 + tests/pos-custom-args/captures/i24373b.scala | 13 +++++ .../captures/mutable-hiding-shared.scala | 19 +++++++ 12 files changed, 262 insertions(+), 16 deletions(-) create mode 100644 tests/neg-custom-args/captures/i24373.check create mode 100644 tests/neg-custom-args/captures/i24373.scala create mode 100644 tests/neg-custom-args/captures/i24373a.check create mode 100644 tests/neg-custom-args/captures/i24373a.scala create mode 100644 tests/neg-custom-args/captures/i24373b.check create mode 100644 tests/neg/i24375.scala create mode 100644 tests/pos-custom-args/captures/i24373b.scala create mode 100644 tests/pos-custom-args/captures/mutable-hiding-shared.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala index 3d1a9e75b3fd..200862e0668a 100644 --- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala +++ b/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`. diff --git a/docs/_docs/reference/experimental/capture-checking/separation-checking.md b/docs/_docs/reference/experimental/capture-checking/separation-checking.md index 7fcb35658679..79a6457779e8 100644 --- a/docs/_docs/reference/experimental/capture-checking/separation-checking.md +++ b/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 therefor 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. diff --git a/tests/neg-custom-args/captures/i24373.check b/tests/neg-custom-args/captures/i24373.check new file mode 100644 index 000000000000..9a2dcbc646f4 --- /dev/null +++ b/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 diff --git a/tests/neg-custom-args/captures/i24373.scala b/tests/neg-custom-args/captures/i24373.scala new file mode 100644 index 000000000000..16f6d7258692 --- /dev/null +++ b/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 + + + diff --git a/tests/neg-custom-args/captures/i24373a.check b/tests/neg-custom-args/captures/i24373a.check new file mode 100644 index 000000000000..5c6c12a746f2 --- /dev/null +++ b/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 diff --git a/tests/neg-custom-args/captures/i24373a.scala b/tests/neg-custom-args/captures/i24373a.scala new file mode 100644 index 000000000000..ea739fb9c436 --- /dev/null +++ b/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 + + + + diff --git a/tests/neg-custom-args/captures/i24373b.check b/tests/neg-custom-args/captures/i24373b.check new file mode 100644 index 000000000000..7191630acd2d --- /dev/null +++ b/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`. diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 65c7fe81b135..8cda7660cd5b 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/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. diff --git a/tests/neg-custom-args/captures/linear-buffer.scala b/tests/neg-custom-args/captures/linear-buffer.scala index f85d9ef52dba..204620b55f7c 100644 --- a/tests/neg-custom-args/captures/linear-buffer.scala +++ b/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 + diff --git a/tests/neg/i24375.scala b/tests/neg/i24375.scala new file mode 100644 index 000000000000..d26113158af2 --- /dev/null +++ b/tests/neg/i24375.scala @@ -0,0 +1,2 @@ +def foo(f: (x: Int) ?=> Int) = f(using 0) +@main def Main = println(foo(x)) \ No newline at end of file diff --git a/tests/pos-custom-args/captures/i24373b.scala b/tests/pos-custom-args/captures/i24373b.scala new file mode 100644 index 000000000000..342f48d36f76 --- /dev/null +++ b/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 + diff --git a/tests/pos-custom-args/captures/mutable-hiding-shared.scala b/tests/pos-custom-args/captures/mutable-hiding-shared.scala new file mode 100644 index 000000000000..fad7bbe0389c --- /dev/null +++ b/tests/pos-custom-args/captures/mutable-hiding-shared.scala @@ -0,0 +1,19 @@ +import caps.* + +class Logger extends SharedCapability: + def log(msg: String): Unit = println(msg) + +class Ref(init: Int)(using l: Logger) extends Mutable: + self: Ref^ => + private var current = init + def get(): Int = + l.log("get") + current + update def set(x: Int) = + l.log("set $x") + current = x + +def test = + given l: Logger = Logger() + val r: Ref^{cap.rd} = Ref(3) + r.get()