Do not go inside boxes for freezing

Author: Linyxus

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 = // () ?-> <?>

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

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))