From 676b85fd37e204c7ba2eec773436553036625f2d Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 6 Nov 2025 13:36:27 +0100 Subject: [PATCH 1/3] 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 ca4ab14187c4..887d3de1b7ab 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 6b056d7f944bb5cb957370692b2c43dc8a49acfb Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 7 Nov 2025 10:12:42 +0100 Subject: [PATCH 2/3] 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 887d3de1b7ab..6079d585b9c2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1035,7 +1035,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 25a8a468b996981880bd9c400a3dfa6169f38cbf Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 7 Nov 2025 10:35:23 +0100 Subject: [PATCH 3/3] 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**