Freshen all explicit arguments of type applications

Previously, we did not do that, which means that explicit arguments in TypeApply's
could not contain `^`.

This precaution shoul dnot longer be needed with level checking.

Author: odersky

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

@@ -501,7 +501,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         var transformed =
           if tree.isInferred
           then transformInferredType(tree.tpe)
-          else transformExplicitType(tree.tpe, sym, freshen = !boxed, tptToCheck = tree)
+          else transformExplicitType(tree.tpe, sym, freshen = true, tptToCheck = tree)
         if boxed then transformed = transformed.boxDeeply
         tree.setNuType(
           if sym.hasAnnotation(defn.UncheckedCapturesAnnot) then makeUnchecked(transformed)

tests/neg-custom-args/captures/boundary-homebrew.check

@@ -0,0 +1,16 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary-homebrew.scala:19:19 ----------------------------
+19 |    boundary[Int]: l2 ?=>  // error
+   |                   ^
+   |Capability cap outlives its scope: it leaks into outer capture set 's1 of parameter l1.
+   |The leakage occurred when trying to match the following types:
+   |
+   |Found:    (l2: boundary.Label[Int]^'s2) ?->{l1} Int
+   |Required: (boundary.Label[Int]^) ?=> Int
+   |
+   |where:    ?=> refers to a fresh root capability created in anonymous function of type (using l1²: boundary.Label[boundary.Label[Int]^]^): boundary.Label[Int]^ when checking argument to parameter body of method apply
+   |          ^   refers to the universal root capability
+   |          cap is a fresh root capability created in anonymous function of type (using l2: boundary.Label[Int]^'s2): Int of parameter parameter l2² of method $anonfun
+20 |      boundary.break(l2)(using l1)
+21 |      15
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/boundary-homebrew.scala

@@ -0,0 +1,22 @@
+import language.experimental.captureChecking
+import caps.*
+
+object boundary:
+  class Label[-T]
+  case class Break[T](private[boundary] label: Label[T]^{}, result: T) extends Throwable
+
+  def apply[T](body: Label[T]^ ?=> T): T =
+    val label = Label()
+    try
+      body(using label)
+    catch
+      case Break[T @unchecked](l, res) if l eq label => res
+
+  def break[T](value: T)(using l: Label[T]) = throw Break(unsafe.unsafeAssumePure(l), value)
+
+def test =
+  boundary[boundary.Label[Int]^]: l1 ?=>
+    boundary[Int]: l2 ?=>  // error
+      boundary.break(l2)(using l1)
+      15
+    ???

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

@@ -11,7 +11,7 @@ object test {
     f[Tree^](t) // error
     f[Tree](t)  // error
     val c1 = C(t) // error
-    val c2 = C[Tree^](t) // error
+    val c2 = C[Tree^](t) // error // error
     val c3 = C[Tree](t)  // error
 
     val foo: C[Tree^] = ???

tests/neg-custom-args/captures/capt-test.scala

@@ -20,7 +20,7 @@ def handle[E <: Exception,  R <: Top](op: (CT[E] @retains[caps.cap.type]) => R)(
   catch case ex: E => handler(ex)
 
 def test: Unit =
-  val b = handle[Exception, () => Nothing] { // error
+  val b = handle[Exception, () => Nothing] {
     (x: CanThrow[Exception]) => () => raise(new Exception)(using x)  // error
   } {
     (ex: Exception) => ???

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

@@ -43,46 +43,50 @@
    |                                        Note that capability x is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/capt1.scala:36:16 -------------------------------------------------------------
-36 |  val z2 = h[() -> Cap](() => x) // error // error
-   |             ^^^^^^^^^
-   |             Type variable X of method h cannot be instantiated to () -> C^ since
-   |             the part C^ of that type captures the root capability `cap`.
-   |
-   |             where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:36:24 ----------------------------------------
-36 |  val z2 = h[() -> Cap](() => x) // error // error
+36 |  val z2 = h[() -> Cap](() => x) // error
    |                        ^^^^^^^
-   |Found:    () ->'s2 C^
-   |Required: () -> C^²
+   |                      Found:    () ->'s2 C^
+   |                      Required: () -> C^²
    |
-   |Note that capability cap is not included in capture set {cap²}
-   |because cap is not visible from cap² in value z2.
+   |                      Note that capability cap is not included in capture set {cap²}
+   |                      because cap is not visible from cap² in value z2.
    |
-   |where:    ^ and cap   refer to a root capability associated with the result type of (): C^
-   |          ^² and cap² refer to a fresh root capability created in value z2 when checking argument to parameter a of method h
+   |                      where:    ^ and cap   refer to a root capability associated with the result type of (): C^
+   |                                ^² and cap² refer to a fresh root capability created in value z2
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:37:5 -----------------------------------------
 37 |    (() => C()) // error
    |     ^^^^^^^^^
-   |Found:    () ->'s3 C^
-   |Required: () -> C^²
+   |     Found:    () ->'s3 C^
+   |     Required: () -> C^²
    |
-   |Note that capability cap is not included in capture set {cap²}
-   |because cap is not visible from cap² in value z2.
+   |     Note that capability cap is not included in capture set {cap²}
+   |     because cap is not visible from cap² in value z2.
    |
-   |where:    ^ and cap   refer to a root capability associated with the result type of (): C^
-   |          ^² and cap² refer to a fresh root capability created in value z2 when checking argument to parameter b of method h
+   |     where:    ^ and cap   refer to a root capability associated with the result type of (): C^
+   |               ^² and cap² refer to a fresh root capability created in value z2
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/capt1.scala:38:13 -------------------------------------------------------------
+-- Error: tests/neg-custom-args/captures/capt1.scala:38:51 -------------------------------------------------------------
 38 |  val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C())  // error
-   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |             Type variable X of method h cannot be instantiated to () ->{x} C^ since
-   |             the part C^ of that type captures the root capability `cap`.
-   |
-   |             where:    ^ refers to the universal root capability
+   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |           Separation failure: Illegal access to {x} which is hidden by the previous definition
+   |           of value z2 with type () ->{} C^.
+   |           This type hides capabilities  {cap, x}
+   |
+   |           where:    ^   refers to a fresh root capability in the type of value z2
+   |                     cap is a fresh root capability created in value z2
+-- Error: tests/neg-custom-args/captures/capt1.scala:40:25 -------------------------------------------------------------
+40 |  val z1: () => Cap = f1(x) // error
+   |                         ^
+   |                         Separation failure: Illegal access to {x} which is hidden by the previous definition
+   |                         of value z3 with type () ->{x} C^.
+   |                         This type hides capabilities  {cap, x}
+   |
+   |                         where:    ^   refers to a fresh root capability in the type of value z3
+   |                                   cap is a fresh root capability created in value z3
 -- Error: tests/neg-custom-args/captures/capt1.scala:43:7 --------------------------------------------------------------
 43 |    if x == null then  // error: separation
    |       ^

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

@@ -33,11 +33,11 @@ def foo() =
   val x: C @retains[caps.cap.type] = ???
   def h[X](a: X)(b: X) = a
 
-  val z2 = h[() -> Cap](() => x) // error // error
+  val z2 = h[() -> Cap](() => x) // error
     (() => C()) // error
   val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C())  // error
 
-  val z1: () => Cap = f1(x)
+  val z1: () => Cap = f1(x) // error
 
   val z4 =
     if x == null then  // error: separation

tests/neg-custom-args/captures/class-level-attack.check

@@ -1,10 +1,3 @@
--- Error: tests/neg-custom-args/captures/class-level-attack.scala:12:24 ------------------------------------------------
-12 |  val r: Ref[IO^] = Ref[IO^](io) // error:
-   |                        ^^^
-   |                        Type variable X of constructor Ref cannot be instantiated to IO^ since
-   |                        that type captures the root capability `cap`.
-   |
-   |                        where:    ^ refers to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-level-attack.scala:17:26 ---------------------------
 17 |  def set(x: IO^) = r.put(x)  // error
    |                          ^

tests/neg-custom-args/captures/class-level-attack.scala

@@ -9,7 +9,7 @@ class Ref[X](init: X):
   def put(y: X): Unit = x = y
 
 class C(io: IO^):
-  val r: Ref[IO^] = Ref[IO^](io) // error:
+  val r: Ref[IO^] = Ref[IO^](io)
     //Type variable X of constructor Ref cannot be instantiated to box IO^ since
     //that type captures the root capability `cap`.
     // where: ^ refers to the universal root capability

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

@@ -7,4 +7,4 @@ class Foo:
 def Test: Unit =
   val f = new Foo
   f.withSession(s => s).request // error
-  f.withSession[Session^](t => t) // error // error
+  f.withSession[Session^](t => t) // error