Revised scheme: Make freeze a method with consume parameter

Author: odersky

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

@@ -800,21 +800,6 @@ class CheckCaptures extends Recheck, SymTransformer:
       capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType")
       super.recheckFinish(argType, tree, pt)
 
-    /** 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
-          case t @ CapturingType(parent, _)
-          if parent.derivesFromMutable && variance > 0 =>
-            t.derivedCapturingType(apply(parent), CaptureSet.emptyOfStateful)
-          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 freeze.
      *  More work is done in `recheckApplication`, `recheckArg` and `instantiate` below.
@@ -827,7 +812,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         val arg :: Nil = tree.args: @unchecked
         withDiscardedUses(recheck(arg, pt))
       else if meth == defn.Caps_freeze then
-        applyFreeze(tree)
+        freeze(super.recheckApply(tree, pt), tree.srcPos)
       else
         val res = super.recheckApply(tree, pt)
         includeCallCaptures(meth, res, tree)

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

@@ -7,6 +7,7 @@ import Symbols.*, Types.*, Flags.*, Contexts.*, Names.*, Decorators.*
 import Capabilities.*
 import util.SrcPos
 import config.Printers.capt
+import config.Feature
 import ast.tpd.Tree
 import typer.ProtoTypes.LhsProto
 
@@ -249,4 +250,22 @@ object Mutability:
       case improved =>
         improved
 
+  /** Apply `caps.freeze(...)`. Strip all capture sets of covariant Mutable
+   *  types, turning them into `CaptureSet.emptyOfMutable`. Only Mutable types
+   *  that contribute to the overall capture set are considered, since that is the
+   *  set analyzed by consume/use checking. That means that double-flip covariant
+   *  and boxed capture sets are not dropped.
+   */
+  def freeze(tp: Type, pos: SrcPos)(using Context): Type = tp.widen match
+    case tpw @ CapturingType(parent, refs)
+    if parent.derivesFromMutable && !tpw.isBoxed =>
+      if !Feature.enabled(Feature.separationChecking) then
+        report.warning(
+          em"""freeze is safe only if separation checking is enabled.
+              |You can enable separation checking with the language import
+              |
+              |   import language.experimental.separationChecking""",
+          pos)
+      tpw.derivedCapturingType(parent, CaptureSet.emptyOfStateful)
+    case _ => tp
 end Mutability

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

@@ -445,34 +445,3 @@ The subcapturing theory for sets is then as before, with the following additiona
  - `{x, ...}.reader = {x.rd, ...}.reader`
  - `{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 `{}`.
-

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

@@ -235,3 +235,36 @@ val c = b += 3
 ```
 This code is equivalent to functional append with `+`, and is at the same time more efficient since it re-uses the storage of the argument buffer.
 
+## 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] =
+  val a = Arr[String](2)
+  a(0) = "hello"
+  a(1) = "world"
+  freeze(a)
+```
+The `freeze` method is defined in `caps` like this:
+```scala
+def freeze[T](consume x: Mutable^): x.type = x
+```
+It consumes a value of `Mutable` type with arbitrary capture set. The actual signature of
+`consume` declares that `x.type` is returned, but the actual return type after capture checking is special. Instead of `x.type` it is the underlying `Mutable` type with its top-level capture set
+mapped to `{}`. Applications of `freeze` are safe only if separation checking is enabled.
+

library/src/scala/caps/package.scala

@@ -151,12 +151,6 @@ 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 freeze[T](op: -> T): T = op
-
 @experimental
 object internal:
 
@@ -197,6 +191,12 @@ object internal:
 
 end internal
 
+/** 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 freeze[T](@internal.consume x: Mutable^): x.type = x
+
 @experimental
 object unsafe:
   /** Two usages:

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

@@ -1,22 +1,7 @@
--- [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^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:11:17 ---------------------------------------
+11 |  val b = freeze((a, a)) // error
+   |                 ^^^^^^
+   |                 Found:    (Arr[String], Arr[String])
+   |                 Required: scala.caps.Mutable^
    |
    | longer explanation available when compiling with `-explain`

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

@@ -8,16 +8,5 @@ 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 b = freeze((a, a)) // error
 

tests/neg-custom-args/captures/sep-consume.check

@@ -1,3 +1,8 @@
+-- Error: tests/neg-custom-args/captures/sep-consume.scala:30:49 -------------------------------------------------------
+30 |def test4(consume p: Pair[Ref^, Ref^]): Ref^ = p.fst // error
+   |                                               ^^^^^
+   |                          Local reach capability p.fst* leaks into capture scope of method test4.
+   |                          You could try to abstract the capabilities referred to by p.fst* in a capset variable.
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:19:2 --------------------------------------------------------
 19 |  x.put(42)  // error
    |  ^

tests/neg-custom-args/captures/sep-consume.scala

@@ -27,6 +27,8 @@ def test3(consume x: Ref^): Unit =
   foo()
   foo()
 
+def test4(consume p: Pair[Ref^, Ref^]): Ref^ = p.fst // error
+
 /*
 def test4(consume @use p: Pair[Ref^, Ref^]): Unit =
   val x: Ref^{p.fst*} = p.fst

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

@@ -15,12 +15,11 @@ def test2 =
     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
+def test3 =
+  val a = Arr[String](2)
+  a(0) = "1"
+  a(1) = "2"
+  val b = freeze(a)
+  val _: Arr[String]^{} = b
+  b
+