Revise freeze signature to take a Mutable parameter

That way we can also freeze read-only Mutables.

Also: Adapt boxes and double flip tests

Author: Linyxus

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

@@ -262,9 +262,9 @@ val f: IArr[String] =
 ```
 The `freeze` method is defined in `caps` like this:
 ```scala
-def freeze[T](consume x: Mutable^): x.type = x
+def freeze(consume x: Mutable): x.type = x
 ```
-It consumes a value of `Mutable` type with arbitrary capture set. The actual signature of
+It consumes a value of `Mutable` type with arbitrary capture set (since any capture set conforms to the implied `{cap.rd}`). 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

@@ -195,7 +195,7 @@ end internal
  *  result of pure operation `op`, turning them into immutable types.
  */
 @experimental
-def freeze[T](@internal.consume x: Mutable^): x.type = x
+def freeze(@internal.consume x: Mutable): x.type = x
 
 @experimental
 object unsafe:

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

@@ -0,0 +1,44 @@
+-- [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}]^{}
+   |                        Required: Box[Ref^{}]^{cap.rd}
+   |
+   |                        Note that capability a.rd is not included in capture set {}.
+   |
+   |                        where:    cap is a fresh root capability classified as Unscoped in the type of value xs
+   |
+   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:29:7 -------------------------------------------------------
+29 |    Box(a) // error
+   |    ^^^^^^
+   |Separation failure: Illegal access to {cap of value a} which is hidden by the previous definition
+   |of value a with type Ref^.
+   |This type hides capabilities  {cap}
+   |
+   |where:    ^   refers to a fresh root capability classified as Unscoped in the type of value a
+   |          cap is a fresh root capability classified as Unscoped created in value a when instantiating method allocRef's type (): Ref^²
+-- 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
+-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:37:12 ------------------------------------------------------
+37 |  par(() => a.set(42), () => println(b.get)) // error
+   |            ^
+   |      Separation failure: Illegal access to (a : Ref^), which was passed as a consume parameter to method freeze
+   |      on line 36 and therefore is no longer available.
+   |
+   |      where:    ^ refers to a fresh root capability classified as Unscoped in the type of value a

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) extends caps.Mutable
+
+// 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) // error
+  val b = xs.unbox
+  par(() => a.set(42), () => println(b.get))  // error
+
+def test3(): Unit =
+  val a = allocRef()
+  val b = freeze:
+    a
+  par(() => a.set(42), () => println(b.get)) // error

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

@@ -0,0 +1,7 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-double-flip.scala:15:4 ----------------------------
+15 |    (x: Ref^) => (op: Ref^ => IRef) => op(x) // error
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |    Found:    Ref^ -> (Ref^ => IRef) -> IRef
+   |    Required: scala.caps.Mutable
+   |
+   | longer explanation available when compiling with `-explain`

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) // error
+  val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x)

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

@@ -2,6 +2,6 @@
 11 |  val b = freeze((a, a)) // error
    |                 ^^^^^^
    |                 Found:    (Arr[String], Arr[String])
-   |                 Required: scala.caps.Mutable^
+   |                 Required: scala.caps.Mutable
    |
    | longer explanation available when compiling with `-explain`