From 7b32bb75128a46ad3ba25b0e1952744f57a9ac91 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 12 Nov 2025 13:24:37 +0100 Subject: [PATCH 1/6] Add caps.freeze wrapper --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 38 +++++++++++++++---- .../dotty/tools/dotc/core/Definitions.scala | 3 +- .../capture-checking/mutability.md | 31 +++++++++++++++ library/src/scala/caps/package.scala | 7 ++++ .../neg-custom-args/captures/immutable.check | 22 +++++++++++ .../neg-custom-args/captures/immutable.scala | 23 +++++++++++ .../captures/immutable-cycle.scala | 15 ++++++++ .../captures/immutable-cycle.scala | 15 ++++++++ .../pos-custom-args/captures/immutable.scala | 26 +++++++++++++ .../stdlibExperimentalDefinitions.scala | 1 + 10 files changed, 172 insertions(+), 9 deletions(-) create mode 100644 tests/neg-custom-args/captures/immutable.check create mode 100644 tests/neg-custom-args/captures/immutable.scala create mode 100644 tests/pending/pos-custom-args/captures/immutable-cycle.scala create mode 100644 tests/pos-custom-args/captures/immutable-cycle.scala create mode 100644 tests/pos-custom-args/captures/immutable.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 083d467a96a2..09ee0bf903f9 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -790,22 +790,44 @@ class CheckCaptures extends Recheck, SymTransformer: selType }//.showing(i"recheck sel $tree, $qualType = $result") - /** Recheck applications, with special handling of unsafeAssumePure. + /** Recheck `caps.unsafe.unsafeAssumePure(...)` */ + def applyAssumePure(tree: Apply, pt: Type)(using Context): Type = + val arg :: Nil = tree.args: @unchecked + val argType0 = recheck(arg, pt.stripCapturing.capturing(FreshCap(Origin.UnsafeAssumePure))) + val argType = + if argType0.captureSet.isAlwaysEmpty then argType0 + else argType0.widen.stripCapturing + capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType") + super.recheckFinish(argType, tree, pt) + + /** Recheck `caps.immutable(...)` */ + def applyImmutable(tree: Apply)(using Context): Type = + val arg :: Nil = tree.args: @unchecked + def imm = new TypeMap: + def apply(t: Type) = t match + case t @ CapturingType(parent, _) + if parent.derivesFromMutable && variance > 0 => + t.derivedCapturingType(apply(parent), CaptureSet.emptyOfMutable) + case _ => + mapOver(t) + val opProto = // () ?-> + defn.FunctionType(0, isContextual = true).appliedTo(WildcardType) + recheck(arg, opProto).stripCapturing match + case defn.ContextFunctionType(Nil, resType) => imm(resType) + + /** Recheck applications, with special handling of unsafeAssumePure, + * unsafeDiscardUses, and immutable. * More work is done in `recheckApplication`, `recheckArg` and `instantiate` below. */ override def recheckApply(tree: Apply, pt: Type)(using Context): Type = val meth = tree.fun.symbol if meth == defn.Caps_unsafeAssumePure then - val arg :: Nil = tree.args: @unchecked - val argType0 = recheck(arg, pt.stripCapturing.capturing(FreshCap(Origin.UnsafeAssumePure))) - val argType = - if argType0.captureSet.isAlwaysEmpty then argType0 - else argType0.widen.stripCapturing - capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType") - super.recheckFinish(argType, tree, pt) + applyAssumePure(tree, pt) else if meth == defn.Caps_unsafeDiscardUses then val arg :: Nil = tree.args: @unchecked withDiscardedUses(recheck(arg, pt)) + else if meth == defn.Caps_immutable then + applyImmutable(tree) else val res = super.recheckApply(tree, pt) includeCallCaptures(meth, res, tree) diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index d2e4348c96fc..270032942546 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1031,6 +1031,7 @@ class Definitions { @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains") @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains") @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl") + @tu lazy val Caps_immutable: TermSymbol = CapsModule.requiredMethod("immutable") @tu lazy val PureClass: ClassSymbol = requiredClass("scala.caps.Pure") @@ -2100,7 +2101,7 @@ class Definitions { RequiresCapabilityAnnot, captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, ConsumeAnnot, UseAnnot, ReserveAnnot, - CapsUnsafeModule, CapsUnsafeModule.moduleClass, + CapsUnsafeModule, CapsUnsafeModule.moduleClass, Caps_immutable, CapsInternalModule, CapsInternalModule.moduleClass, RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot) diff --git a/docs/_docs/reference/experimental/capture-checking/mutability.md b/docs/_docs/reference/experimental/capture-checking/mutability.md index 177dc7e18a23..bd30a51d7964 100644 --- a/docs/_docs/reference/experimental/capture-checking/mutability.md +++ b/docs/_docs/reference/experimental/capture-checking/mutability.md @@ -339,3 +339,34 @@ The subcapturing theory for sets is then as before, with the following additiona - `{x, ...}.RD = {x.rd, ...}.RD` - `{x.rd, ...} <: {x, ...}` +## The `freeze` Wrapper + +We often want to create a mutable data structure like an array, initialize by assigning to its elements and then return the array as an immutable type that does not +capture any capabilities. This can be achieved using the `freeze` wrapper. + +As an example, consider a class `Arr` which is modelled after `Array` and its immutable counterpart `IArr`: + +```scala +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 +type IArr[T] = Arr[T]^{} +``` + +The `freeze` wrapper allows us to go from an `Arr` to an `IArr`, safely: +```scala +import caps.freeze + +val f: IArr[String] = freeze: + val a = Arr[String](2) + a(0) = "hello" + a(1) = "world" + a +``` +The `freeze` method is defined in `caps` like this: +```scala +def freeze[T](op: -> T): T = op +``` +It takes a pure by-name parameter and returns its result. But the actual return type after capture checking is special. Instead of just `T` as in the declaration above suggests, it's `T` where every covariant occurrence of a `Mutable` type gets its capture set mapped to `{}`. + diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 6fbb0a9a0f93..76ca1607d44f 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -123,6 +123,7 @@ final class reserve extends annotation.StaticAnnotation * environment. */ @experimental +@deprecated(since = "3.8.0") final class use extends annotation.StaticAnnotation /** A trait that used to allow expressing existential types. Replaced by @@ -132,6 +133,12 @@ final class use extends annotation.StaticAnnotation @deprecated sealed trait Exists extends Capability +/** A wrapper that strips all covariant capture sets from Mutable types in the + * result of pure operation `op`, turning them into immutable types. + */ +@experimental +def immutable[T](op: -> T): T = op + @experimental object internal: diff --git a/tests/neg-custom-args/captures/immutable.check b/tests/neg-custom-args/captures/immutable.check new file mode 100644 index 000000000000..f62ffc66626c --- /dev/null +++ b/tests/neg-custom-args/captures/immutable.check @@ -0,0 +1,22 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/immutable.scala:13:20 ------------------------------------ +13 | val b = immutable(a) // error + | ^ + | Found: () ?->{a} Arr[String]^{a} + | Required: () ?-> + | + | Note that capability a is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/immutable.scala:22:4 ------------------------------------- +21 | immutable: +22 | mkExclusive() // error + | ^ + | Capability cap outlives its scope: it leaks into outer capture set 's1 of method test3. + | The leakage occurred when trying to match the following types: + | + | Found: EX^{cap} + | Required: EX^'s1 + | + | where: cap is a root capability associated with the result type of (): EX^ + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/immutable.scala b/tests/neg-custom-args/captures/immutable.scala new file mode 100644 index 000000000000..57c2f22717aa --- /dev/null +++ b/tests/neg-custom-args/captures/immutable.scala @@ -0,0 +1,23 @@ +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) + a(0) = "1" + a(1) = "2" + val b = immutable(a) // error + b + +class EX + +def mkExclusive(): EX^ = ??? + +def test3 = + immutable: + mkExclusive() // error + diff --git a/tests/pending/pos-custom-args/captures/immutable-cycle.scala b/tests/pending/pos-custom-args/captures/immutable-cycle.scala new file mode 100644 index 000000000000..0728851f3225 --- /dev/null +++ b/tests/pending/pos-custom-args/captures/immutable-cycle.scala @@ -0,0 +1,15 @@ +import caps.* + +class Node(val payload: Int) extends Mutable: + var next: Node = ??? + + +type INode = Node^{} + +def cycle(x: Int, y: Int): (INode, INode) = + immutable: + val a = Node(x) + val b = Node(y) + a.next = b + b.next = a + (a, b) diff --git a/tests/pos-custom-args/captures/immutable-cycle.scala b/tests/pos-custom-args/captures/immutable-cycle.scala new file mode 100644 index 000000000000..c23e00cb4a4e --- /dev/null +++ b/tests/pos-custom-args/captures/immutable-cycle.scala @@ -0,0 +1,15 @@ +import caps.* + +class Node[All](val payload: Int) extends Modifiable: + var next: Node = ??? + + +type INode = Node^{} + +def cycle(x: Int, y: Int): (INode, INode) = + immutable: + val a = Node(x) + val b = Node(y) + a.next = b + b.next = a + (a, b) diff --git a/tests/pos-custom-args/captures/immutable.scala b/tests/pos-custom-args/captures/immutable.scala new file mode 100644 index 000000000000..21f6cf40ab61 --- /dev/null +++ b/tests/pos-custom-args/captures/immutable.scala @@ -0,0 +1,26 @@ +import language.experimental.captureChecking +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 = immutable: + val a = Arr[String](2) + a(0) = "1" + a(1) = "2" + a + val _: Arr[String]^{} = a + + val a2 = immutable: + val a = Arr[String](2) + val b = Arr[String](2) + a(0) = "1" + a(1) = "2" + b(0) = "1" + b(1) = "2" + (a, b) + val _: (Arr[String]^{}, Arr[String]^{}) = a2 diff --git a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala index c249721f6a6d..cc9b002623a5 100644 --- a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala +++ b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala @@ -46,6 +46,7 @@ val experimentalDefinitionInLibrary = Set( "scala.caps.unsafe$", "scala.caps.use", "scala.caps.reserve", + "scala.caps.package$package$.freeze", "scala.caps.package$package$.Exclusive", "scala.caps.package$package$.Shared", From 0f9bf5b39f054062f4c0027cf47a88471c59a5d3 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 16 Nov 2025 17:28:42 +0100 Subject: [PATCH 2/6] Rename caps.immutable to caps.freeze --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 10 ++++----- .../dotty/tools/dotc/core/Definitions.scala | 4 ++-- library/src/scala/caps/package.scala | 2 +- tests/neg-custom-args/captures/freeze.check | 22 +++++++++++++++++++ .../{immutable.scala => freeze.scala} | 4 ++-- .../neg-custom-args/captures/immutable.check | 22 ------------------- ...mutable-cycle.scala => freeze-cycle.scala} | 2 +- .../{immutable.scala => freeze.scala} | 4 ++-- .../captures/immutable-cycle.scala | 15 ------------- 9 files changed, 35 insertions(+), 50 deletions(-) create mode 100644 tests/neg-custom-args/captures/freeze.check rename tests/neg-custom-args/captures/{immutable.scala => freeze.scala} (88%) delete mode 100644 tests/neg-custom-args/captures/immutable.check rename tests/pending/pos-custom-args/captures/{immutable-cycle.scala => freeze-cycle.scala} (94%) rename tests/pos-custom-args/captures/{immutable.scala => freeze.scala} (92%) delete mode 100644 tests/pos-custom-args/captures/immutable-cycle.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 09ee0bf903f9..07f9c4096ce1 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -800,8 +800,8 @@ class CheckCaptures extends Recheck, SymTransformer: capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType") super.recheckFinish(argType, tree, pt) - /** Recheck `caps.immutable(...)` */ - def applyImmutable(tree: Apply)(using Context): Type = + /** Recheck `caps.freeze(...)` */ + def applyFreeze(tree: Apply)(using Context): Type = val arg :: Nil = tree.args: @unchecked def imm = new TypeMap: def apply(t: Type) = t match @@ -816,7 +816,7 @@ class CheckCaptures extends Recheck, SymTransformer: case defn.ContextFunctionType(Nil, resType) => imm(resType) /** Recheck applications, with special handling of unsafeAssumePure, - * unsafeDiscardUses, and immutable. + * unsafeDiscardUses, and freeze. * More work is done in `recheckApplication`, `recheckArg` and `instantiate` below. */ override def recheckApply(tree: Apply, pt: Type)(using Context): Type = @@ -826,8 +826,8 @@ class CheckCaptures extends Recheck, SymTransformer: else if meth == defn.Caps_unsafeDiscardUses then val arg :: Nil = tree.args: @unchecked withDiscardedUses(recheck(arg, pt)) - else if meth == defn.Caps_immutable then - applyImmutable(tree) + else if meth == defn.Caps_freeze then + applyFreeze(tree) else val res = super.recheckApply(tree, pt) includeCallCaptures(meth, res, tree) diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index 270032942546..74383308e182 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1031,7 +1031,7 @@ class Definitions { @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains") @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains") @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl") - @tu lazy val Caps_immutable: TermSymbol = CapsModule.requiredMethod("immutable") + @tu lazy val Caps_freeze: TermSymbol = CapsModule.requiredMethod("freeze") @tu lazy val PureClass: ClassSymbol = requiredClass("scala.caps.Pure") @@ -2101,7 +2101,7 @@ class Definitions { RequiresCapabilityAnnot, captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, ConsumeAnnot, UseAnnot, ReserveAnnot, - CapsUnsafeModule, CapsUnsafeModule.moduleClass, Caps_immutable, + CapsUnsafeModule, CapsUnsafeModule.moduleClass, Caps_freeze, CapsInternalModule, CapsInternalModule.moduleClass, RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot) diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 76ca1607d44f..fc6c722df6b9 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -137,7 +137,7 @@ sealed trait Exists extends Capability * result of pure operation `op`, turning them into immutable types. */ @experimental -def immutable[T](op: -> T): T = op +def freeze[T](op: -> T): T = op @experimental object internal: diff --git a/tests/neg-custom-args/captures/freeze.check b/tests/neg-custom-args/captures/freeze.check new file mode 100644 index 000000000000..f4bc6447b80c --- /dev/null +++ b/tests/neg-custom-args/captures/freeze.check @@ -0,0 +1,22 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:13:17 --------------------------------------- +13 | val b = freeze(a) // error + | ^ + | Found: () ?->{a} Arr[String]^{a} + | Required: () ?-> + | + | Note that capability a is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:22:4 ---------------------------------------- +21 | freeze: +22 | mkExclusive() // error + | ^ + | Capability cap outlives its scope: it leaks into outer capture set 's1 of method test3. + | The leakage occurred when trying to match the following types: + | + | Found: EX^{cap} + | Required: EX^'s1 + | + | where: cap is a root capability associated with the result type of (): EX^ + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/immutable.scala b/tests/neg-custom-args/captures/freeze.scala similarity index 88% rename from tests/neg-custom-args/captures/immutable.scala rename to tests/neg-custom-args/captures/freeze.scala index 57c2f22717aa..aa8c26038f38 100644 --- a/tests/neg-custom-args/captures/immutable.scala +++ b/tests/neg-custom-args/captures/freeze.scala @@ -10,7 +10,7 @@ def test2 = val a = Arr[String](2) a(0) = "1" a(1) = "2" - val b = immutable(a) // error + val b = freeze(a) // error b class EX @@ -18,6 +18,6 @@ class EX def mkExclusive(): EX^ = ??? def test3 = - immutable: + freeze: mkExclusive() // error diff --git a/tests/neg-custom-args/captures/immutable.check b/tests/neg-custom-args/captures/immutable.check deleted file mode 100644 index f62ffc66626c..000000000000 --- a/tests/neg-custom-args/captures/immutable.check +++ /dev/null @@ -1,22 +0,0 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/immutable.scala:13:20 ------------------------------------ -13 | val b = immutable(a) // error - | ^ - | Found: () ?->{a} Arr[String]^{a} - | Required: () ?-> - | - | Note that capability a is not included in capture set {}. - | - | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/immutable.scala:22:4 ------------------------------------- -21 | immutable: -22 | mkExclusive() // error - | ^ - | Capability cap outlives its scope: it leaks into outer capture set 's1 of method test3. - | The leakage occurred when trying to match the following types: - | - | Found: EX^{cap} - | Required: EX^'s1 - | - | where: cap is a root capability associated with the result type of (): EX^ - | - | longer explanation available when compiling with `-explain` diff --git a/tests/pending/pos-custom-args/captures/immutable-cycle.scala b/tests/pending/pos-custom-args/captures/freeze-cycle.scala similarity index 94% rename from tests/pending/pos-custom-args/captures/immutable-cycle.scala rename to tests/pending/pos-custom-args/captures/freeze-cycle.scala index 0728851f3225..043b59173ccb 100644 --- a/tests/pending/pos-custom-args/captures/immutable-cycle.scala +++ b/tests/pending/pos-custom-args/captures/freeze-cycle.scala @@ -7,7 +7,7 @@ class Node(val payload: Int) extends Mutable: type INode = Node^{} def cycle(x: Int, y: Int): (INode, INode) = - immutable: + freeze: val a = Node(x) val b = Node(y) a.next = b diff --git a/tests/pos-custom-args/captures/immutable.scala b/tests/pos-custom-args/captures/freeze.scala similarity index 92% rename from tests/pos-custom-args/captures/immutable.scala rename to tests/pos-custom-args/captures/freeze.scala index 21f6cf40ab61..7221921c05b1 100644 --- a/tests/pos-custom-args/captures/immutable.scala +++ b/tests/pos-custom-args/captures/freeze.scala @@ -8,14 +8,14 @@ class Arr[T: reflect.ClassTag](len: Int) extends Mutable: def test2 = - val a = immutable: + val a = freeze: val a = Arr[String](2) a(0) = "1" a(1) = "2" a val _: Arr[String]^{} = a - val a2 = immutable: + val a2 = freeze: val a = Arr[String](2) val b = Arr[String](2) a(0) = "1" diff --git a/tests/pos-custom-args/captures/immutable-cycle.scala b/tests/pos-custom-args/captures/immutable-cycle.scala deleted file mode 100644 index c23e00cb4a4e..000000000000 --- a/tests/pos-custom-args/captures/immutable-cycle.scala +++ /dev/null @@ -1,15 +0,0 @@ -import caps.* - -class Node[All](val payload: Int) extends Modifiable: - var next: Node = ??? - - -type INode = Node^{} - -def cycle(x: Int, y: Int): (INode, INode) = - immutable: - val a = Node(x) - val b = Node(y) - a.next = b - b.next = a - (a, b) From 9e1aae3a2b8a6b65732e8be4b385b0b65ddeebcb Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 16 Nov 2025 23:20:17 +0100 Subject: [PATCH 3/6] Do not go inside boxes for freezing --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 24 ++++++++++-- .../captures/freeze-boxes.check | 35 ++++++++++++++++++ .../captures/freeze-boxes.scala | 37 +++++++++++++++++++ 3 files changed, 92 insertions(+), 4 deletions(-) create mode 100644 tests/neg-custom-args/captures/freeze-boxes.check create mode 100644 tests/neg-custom-args/captures/freeze-boxes.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 07f9c4096ce1..a45e35ec6b7d 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -800,14 +800,30 @@ class CheckCaptures extends Recheck, SymTransformer: capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType") super.recheckFinish(argType, tree, pt) - /** Recheck `caps.freeze(...)` */ + /** Recheck `caps.freeze(...)`. + * + * Capture-check the body of a `freeze` operation and transforms its + * result to be immutable. + * + * `freeze` takes an operation of type `-> T`, where `T` is generic. + * It leverages the fact that the operation is pure, therefore the returned + * mutable types in `T` must be freshly created. It is thus safe to freeze the + * mutable parts in `T` into its immutable version. */ def applyFreeze(tree: Apply)(using Context): Type = val arg :: Nil = tree.args: @unchecked def imm = new TypeMap: def apply(t: Type) = t match - case t @ CapturingType(parent, _) - if parent.derivesFromMutable && variance > 0 => - t.derivedCapturingType(apply(parent), CaptureSet.emptyOfMutable) + case t @ CapturingType(parent, refs) => + // If the capturing type is boxed, we skip it. Since it could capture + // existing values of a mutable type without charging anything to the + // operation passed to `freeze`. + val boxed = t.isBoxed + val parent1 = if boxed then parent else apply(parent) + val refs1 = + if !boxed && parent.derivesFromMutable && variance > 0 then + CaptureSet.emptyOfMutable + else refs + t.derivedCapturingType(parent1, refs1) case _ => mapOver(t) val opProto = // () ?-> diff --git a/tests/neg-custom-args/captures/freeze-boxes.check b/tests/neg-custom-args/captures/freeze-boxes.check new file mode 100644 index 000000000000..ee8660ac3a66 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-boxes.check @@ -0,0 +1,35 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-boxes.scala:22:4 ---------------------------------- +21 | val xs: Box[Ref^{}] = freeze: +22 | Box(a) // error + | ^ + | Found: Box[Ref^{a.rd}]^'s1 + | Required: Box[Ref^{}] + | + | 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/freeze-boxes.scala:36:4 ---------------------------------- +36 | a // error, sanity check + | ^ + | Found: () ?->{a} Ref^{a} + | Required: () ?-> + | + | Note that capability a is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:31:6 ------------------------------------------------------- +31 | par(() => a.set(42), () => println(b.get)) // error + | ^^^^^^^^^^^^^^^ + |Separation failure: argument of type () ->{a} Unit + |to method par: (op1: () => Unit, op2: () => Unit): Unit + |corresponds to capture-polymorphic formal parameter op1 of type () => Unit + |and hides capabilities {a}. + |Some of these overlap with the captures of the second argument with type () ->{b.rd} Unit. + | + | Hidden set of current argument : {a} + | Hidden footprint of current argument : {a} + | Capture set of second argument : {b.rd} + | Footprint set of second argument : {b.rd, a.rd} + | The two sets overlap at : {a} + | + |where: => refers to a fresh root capability created in method test2 when checking argument to parameter op1 of method par diff --git a/tests/neg-custom-args/captures/freeze-boxes.scala b/tests/neg-custom-args/captures/freeze-boxes.scala new file mode 100644 index 000000000000..99b0dcd876eb --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-boxes.scala @@ -0,0 +1,37 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.{Mutable, freeze} + +// A mutable ref and its immutable version +class Ref extends Mutable: + private var data: Int = 0 + def get: Int = data + update def set(x: Int): Unit = data = x +def allocRef(): Ref^ = Ref() +type IRef = Ref^{} + +// Boxes +case class Box[+T](unbox: T) + +// Parallelism +def par(op1: () => Unit, op2: () => Unit): Unit = () + +def test1(): Unit = + val a = allocRef() + val xs: Box[Ref^{}] = freeze: + Box(a) // error + val b = xs.unbox + par(() => a.set(42), () => println(b.get)) + +def test2(): Unit = + val a = allocRef() + val xs = freeze: + Box(a) + val b = xs.unbox + par(() => a.set(42), () => println(b.get)) // error + +def test3(): Unit = + val a = allocRef() + val b = freeze: + a // error, sanity check + par(() => a.set(42), () => println(b.get)) From b0704f5f2ed781f7cc1dfa1d00aa61182042c2b3 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 16 Nov 2025 23:44:45 +0100 Subject: [PATCH 4/6] Tweak test files: tuple elements are indeed boxed --- .../captures/freeze-tuple.check | 33 +++++++++++++++++++ .../captures/freeze-tuple.scala | 23 +++++++++++++ tests/neg-custom-args/captures/freeze.check | 33 +++++++++---------- tests/neg-custom-args/captures/freeze.scala | 29 ++++++++-------- tests/pos-custom-args/captures/freeze.scala | 26 --------------- 5 files changed, 87 insertions(+), 57 deletions(-) create mode 100644 tests/neg-custom-args/captures/freeze-tuple.check create mode 100644 tests/neg-custom-args/captures/freeze-tuple.scala delete mode 100644 tests/pos-custom-args/captures/freeze.scala diff --git a/tests/neg-custom-args/captures/freeze-tuple.check b/tests/neg-custom-args/captures/freeze-tuple.check new file mode 100644 index 000000000000..1fc47d2fd758 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-tuple.check @@ -0,0 +1,33 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:15:4 ---------------------------------- +14 | val (a, b) = freeze: +15 | val t1 = allocRef() // error + | ^ + | Capability cap outlives its scope: it leaks into outer capture set 's1 which is owned by value x1. + | The leakage occurred when trying to match the following types: + | + | Found: (Ref^{cap}, Ref^{cap²})^'s2 + | Required: (Ref^'s1, Ref^'s3)^'s4 + | + | where: cap and cap² refer to a root capability associated with the result type of (): (Ref^, Ref^²)^'s2 +16 | val t2 = allocRef() +17 | (t1, t2) + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:22:16 --------------------------------- +22 | val (a: Ref^{}, b: Ref^{}) = freeze: // error // error + | ^ + | Found: Ref^{a0.rd} + | Required: Ref^{} + | + | Note that capability a0.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:22:27 --------------------------------- +22 | val (a: Ref^{}, b: Ref^{}) = freeze: // error // error + | ^ + | Found: Ref^{b0.rd} + | Required: Ref^{} + | + | Note that capability b0.rd is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/freeze-tuple.scala b/tests/neg-custom-args/captures/freeze-tuple.scala new file mode 100644 index 000000000000..bd3b7cd034c7 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-tuple.scala @@ -0,0 +1,23 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.{Mutable, freeze} + +// A mutable ref and its immutable version +class Ref extends Mutable: + private var data: Int = 0 + def get: Int = data + update def set(x: Int): Unit = data = x +def allocRef(): Ref^ = Ref() +type IRef = Ref^{} + +def test1(): Unit = + val (a, b) = freeze: + val t1 = allocRef() // error + val t2 = allocRef() + (t1, t2) + +def test2(): Unit = + val a0 = allocRef() + val b0 = allocRef() + val (a: Ref^{}, b: Ref^{}) = freeze: // error // error + (a0, b0) diff --git a/tests/neg-custom-args/captures/freeze.check b/tests/neg-custom-args/captures/freeze.check index f4bc6447b80c..0be68f99acba 100644 --- a/tests/neg-custom-args/captures/freeze.check +++ b/tests/neg-custom-args/captures/freeze.check @@ -1,22 +1,19 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:13:17 --------------------------------------- -13 | val b = freeze(a) // error - | ^ - | Found: () ?->{a} Arr[String]^{a} - | Required: () ?-> +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:19:4 ---------------------------------------- +18 | val a2 = freeze: +19 | val a = Arr[String](2) // error + | ^ + |Capability cap outlives its scope: it leaks into outer capture set 's1 of value a2. + |The leakage occurred when trying to match the following types: | - | Note that capability a is not included in capture set {}. + |Found: (Arr[String]^{cap}, Arr[String]^{cap²})^'s2 + |Required: (Arr[String]^'s1, Arr[String]^'s3)^'s4 | - | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:22:4 ---------------------------------------- -21 | freeze: -22 | mkExclusive() // error - | ^ - | Capability cap outlives its scope: it leaks into outer capture set 's1 of method test3. - | The leakage occurred when trying to match the following types: - | - | Found: EX^{cap} - | Required: EX^'s1 - | - | where: cap is a root capability associated with the result type of (): EX^ + |where: cap and cap² refer to a root capability associated with the result type of (): (Arr[String]^, Arr[String]^²)^'s2 +20 | val b = Arr[String](2) +21 | a(0) = "1" +22 | a(1) = "2" +23 | b(0) = "1" +24 | b(1) = "2" +25 | (a, b) | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/freeze.scala b/tests/neg-custom-args/captures/freeze.scala index aa8c26038f38..48f20edd2557 100644 --- a/tests/neg-custom-args/captures/freeze.scala +++ b/tests/neg-custom-args/captures/freeze.scala @@ -1,3 +1,4 @@ +import language.experimental.captureChecking import caps.* class Arr[T: reflect.ClassTag](len: Int) extends Mutable: @@ -7,17 +8,19 @@ class Arr[T: reflect.ClassTag](len: Int) extends Mutable: def test2 = - val a = Arr[String](2) - a(0) = "1" - a(1) = "2" - val b = freeze(a) // error - b - -class EX - -def mkExclusive(): EX^ = ??? - -def test3 = - freeze: - mkExclusive() // error + val a = freeze: + val a = Arr[String](2) + a(0) = "1" + a(1) = "2" + a + val _: Arr[String]^{} = a + val a2 = freeze: + val a = Arr[String](2) // error + val b = Arr[String](2) + a(0) = "1" + a(1) = "2" + b(0) = "1" + b(1) = "2" + (a, b) + val _: (Arr[String]^{}, Arr[String]^{}) = a2 diff --git a/tests/pos-custom-args/captures/freeze.scala b/tests/pos-custom-args/captures/freeze.scala deleted file mode 100644 index 7221921c05b1..000000000000 --- a/tests/pos-custom-args/captures/freeze.scala +++ /dev/null @@ -1,26 +0,0 @@ -import language.experimental.captureChecking -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 = freeze: - val a = Arr[String](2) - a(0) = "1" - a(1) = "2" - a - val _: Arr[String]^{} = a - - val a2 = freeze: - val a = Arr[String](2) - val b = Arr[String](2) - a(0) = "1" - a(1) = "2" - b(0) = "1" - b(1) = "2" - (a, b) - val _: (Arr[String]^{}, Arr[String]^{}) = a2 From d61f989b47dfa368fbc278fa54a6bbd728661532 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 16 Nov 2025 23:54:34 +0100 Subject: [PATCH 5/6] Ignore double-flip occurrences for freezing --- .../src/dotty/tools/dotc/cc/CheckCaptures.scala | 4 ++++ .../captures/freeze-double-flip.check | 13 +++++++++++++ .../captures/freeze-double-flip.scala | 16 ++++++++++++++++ 3 files changed, 33 insertions(+) create mode 100644 tests/neg-custom-args/captures/freeze-double-flip.check create mode 100644 tests/neg-custom-args/captures/freeze-double-flip.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index a45e35ec6b7d..0803fc62578a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -813,6 +813,10 @@ class CheckCaptures extends Recheck, SymTransformer: val arg :: Nil = tree.args: @unchecked def imm = new TypeMap: def apply(t: Type) = t match + case t if variance <= 0 => + // Skip double-flip occurrences of mutable types. + // Example: tests/neg-custom-args/captures/freeze-double-flip.scala. + t case t @ CapturingType(parent, refs) => // If the capturing type is boxed, we skip it. Since it could capture // existing values of a mutable type without charging anything to the diff --git a/tests/neg-custom-args/captures/freeze-double-flip.check b/tests/neg-custom-args/captures/freeze-double-flip.check new file mode 100644 index 000000000000..4203080b61b1 --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-double-flip.check @@ -0,0 +1,13 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-double-flip.scala:16:48 --------------------------- +16 | val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x) // error + | ^^^^^^ + |Found: (x: Ref^'s1) ->'s2 Ref^{x.rd} + |Required: Ref^ => Ref^{cap.rd} + | + |Note that capability x.rd is not included in capture set {cap.rd}. + | + |where: => refers to a fresh root capability created in anonymous function of type (x: Ref^): Ref^{} when checking argument to parameter x$0 of method apply + | ^ refers to the universal root capability + | cap is a fresh root capability created in anonymous function of type (x: Ref^): Ref^{} when checking argument to parameter x$0 of method apply + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/freeze-double-flip.scala b/tests/neg-custom-args/captures/freeze-double-flip.scala new file mode 100644 index 000000000000..9e8a5b10787e --- /dev/null +++ b/tests/neg-custom-args/captures/freeze-double-flip.scala @@ -0,0 +1,16 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.{Mutable, freeze} + +// A mutable ref and its immutable version +class Ref extends Mutable: + private var data: Int = 0 + def get: Int = data + update def set(x: Int): Unit = data = x +def allocRef(): Ref^ = Ref() +type IRef = Ref^{} + +def test1(): Unit = + val magic = freeze: + (x: Ref^) => (op: Ref^ => IRef) => op(x) + val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x) // error From 05e1e4b221fd1fb8d64daa98591f1edaaee88b29 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 17 Nov 2025 15:35:07 +0100 Subject: [PATCH 6/6] Update MimaFilters --- project/MiMaFilters.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/project/MiMaFilters.scala b/project/MiMaFilters.scala index e45558f044b3..575a20af629a 100644 --- a/project/MiMaFilters.scala +++ b/project/MiMaFilters.scala @@ -32,6 +32,7 @@ object MiMaFilters { ProblemFilters.exclude[MissingClassProblem]("scala.caps.Classifier"), ProblemFilters.exclude[MissingClassProblem]("scala.caps.SharedCapability"), ProblemFilters.exclude[MissingClassProblem]("scala.caps.Control"), + ProblemFilters.exclude[DirectMissingMethodProblem]("scala.caps.package#package.freeze"), ), )