Freshen all explicit arguments of type applications

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

@@ -158,7 +158,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       def mappedInfo =
         if toBeUpdated.contains(sym)
         then symd.info // don't transform symbols that will anyway be updated
-        else transformExplicitType(symd.info, sym, freshen = true)
+        else transformExplicitType(symd.info, sym)
       if Synthetics.needsTransform(symd) then
         Synthetics.transform(symd, mappedInfo)
       else if isPreCC(sym) then
@@ -340,7 +340,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
    *   5. Schedule deferred well-formed tests for types with retains annotations.
    *   6. Perform normalizeCaptures
    */
-  private def transformExplicitType(tp: Type, sym: Symbol, freshen: Boolean, tptToCheck: Tree = EmptyTree)(using Context): Type =
+  private def transformExplicitType(tp: Type, sym: Symbol, tptToCheck: Tree = EmptyTree)(using Context): Type =
 
     def fail(msg: Message) =
       if !tptToCheck.isEmpty then report.error(msg, tptToCheck.srcPos)
@@ -474,9 +474,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     val tp3 =
       if sym.isType then stripImpliedCaptureSet(tp2)
       else tp2
-    if freshen then
-      capToFresh(tp3, Origin.InDecl(sym))
-    else tp3
+    capToFresh(tp3, Origin.InDecl(sym))
   end transformExplicitType
 
   /** Update info of `sym` for CheckCaptures phase only */
@@ -501,7 +499,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, tptToCheck = tree)
         if boxed then transformed = transformed.boxDeeply
         tree.setNuType(
           if sym.hasAnnotation(defn.UncheckedCapturesAnnot) then makeUnchecked(transformed)
@@ -725,7 +723,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
             // Compute new parent types
             val ps1 = inContext(ctx.withOwner(cls)):
-              ps.mapConserve(transformExplicitType(_, NoSymbol, freshen = false))
+              ps.mapConserve(transformExplicitType(_, NoSymbol))
 
             // Install new types and if it is a module class also update module object
             if (selfInfo1 ne selfInfo) || (ps1 ne ps) then

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/hk-param.scala

@@ -1,6 +1,6 @@
 /** Concrete collection type: View */
 trait View[+A] extends Itable[A], ILike[A, [X] =>> View[X]^]: // error
-  override def fromIterable[B](c: Itable[B]^): View[B]^{c} = ???
+  override def fromIterable[B](c: Itable[B]^): View[B]^{c} = ??? // error
 
 trait IPolyTransforms[+A, +C[A]] extends Any:
   def fromIterable[B](coll: Itable[B]^): C[B]

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

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

@@ -1,35 +1,49 @@
--- Error: tests/neg-custom-args/captures/i16114.scala:18:13 ------------------------------------------------------------
-18 |      expect[Cap^] {  // error
-   |             ^^^^
-   |             Type variable T of method expect cannot be instantiated to Cap^ since
-   |             that type captures the root capability `cap`.
-   |
-   |             where:    ^ refers to the universal root capability
--- Error: tests/neg-custom-args/captures/i16114.scala:24:13 ------------------------------------------------------------
-24 |      expect[Cap^] { // error
-   |             ^^^^
-   |             Type variable T of method expect cannot be instantiated to Cap^ since
-   |             that type captures the root capability `cap`.
-   |
-   |             where:    ^ refers to the universal root capability
--- Error: tests/neg-custom-args/captures/i16114.scala:30:13 ------------------------------------------------------------
-30 |      expect[Cap^] {  // error
-   |             ^^^^
-   |             Type variable T of method expect cannot be instantiated to Cap^ since
-   |             that type captures the root capability `cap`.
-   |
-   |             where:    ^ refers to the universal root capability
--- Error: tests/neg-custom-args/captures/i16114.scala:36:13 ------------------------------------------------------------
-36 |      expect[Cap^](io) // error
-   |             ^^^^
-   |             Type variable T of method expect cannot be instantiated to Cap^ since
-   |             that type captures the root capability `cap`.
-   |
-   |             where:    ^ refers to the universal root capability
--- Error: tests/neg-custom-args/captures/i16114.scala:39:13 ------------------------------------------------------------
-39 |      expect[Cap^] { // error
-   |             ^^^^
-   |             Type variable T of method expect cannot be instantiated to Cap^ since
-   |             that type captures the root capability `cap`.
-   |
-   |             where:    ^ refers to the universal root capability
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:17:32 ---------------------------------------
+17 |    val op1: Unit ->{io} Unit = (x: Unit) => // error
+   |                                ^
+   |                                Found:    (x: Unit) ->{io, fs} Unit
+   |                                Required: Unit ->{io} Unit
+   |
+   |                                Note that capability fs is not included in capture set {io}.
+18 |      expect[Cap^] {
+19 |        io.use()
+20 |        fs
+21 |      }
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:23:32 ---------------------------------------
+23 |    val op2: Unit ->{fs} Unit = (x: Unit) => // error
+   |                                ^
+   |                                Found:    (x: Unit) ->{fs, io} Unit
+   |                                Required: Unit ->{fs} Unit
+   |
+   |                                Note that capability io is not included in capture set {fs}.
+24 |      expect[Cap^] {
+25 |        fs.use()
+26 |        io
+27 |      }
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:35:30 ---------------------------------------
+35 |    val op4: Unit ->{} Unit = (x: Unit) =>  // error
+   |                              ^
+   |                              Found:    (x: Unit) ->{io} Unit
+   |                              Required: Unit -> Unit
+   |
+   |                              Note that capability io is not included in capture set {}.
+36 |      expect[Cap^](io)
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16114.scala:38:27 ---------------------------------------
+38 |    val op: Unit -> Unit = (x: Unit) => // error
+   |                           ^
+   |                           Found:    (x: Unit) ->{io} Unit
+   |                           Required: Unit -> Unit
+   |
+   |                           Note that capability io is not included in capture set {}.
+39 |      expect[Cap^] {
+40 |        io.use()
+41 |        io
+42 |      }
+   |
+   | longer explanation available when compiling with `-explain`

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

@@ -14,29 +14,29 @@ def withCap[T](op: Cap^ => T): T = {
 
 def main(fs: Cap^): Unit = {
   def badOp(io: Cap^): Unit ->{} Unit = {
-    val op1: Unit ->{io} Unit = (x: Unit) =>
-      expect[Cap^] {  // error
+    val op1: Unit ->{io} Unit = (x: Unit) => // error
+      expect[Cap^] {
         io.use()
         fs
       }
 
-    val op2: Unit ->{fs} Unit = (x: Unit) =>
-      expect[Cap^] { // error
+    val op2: Unit ->{fs} Unit = (x: Unit) => // error
+      expect[Cap^] {
         fs.use()
         io
       }
 
-    val op3: Unit ->{io} Unit = (x: Unit) =>
-      expect[Cap^] {  // error
+    val op3: Unit ->{io} Unit = (x: Unit) => // ok
+      expect[Cap^] {
         io.use()
         io
       }
 
-    val op4: Unit ->{} Unit = (x: Unit) =>  // o k
-      expect[Cap^](io) // error
+    val op4: Unit ->{} Unit = (x: Unit) =>  // error
+      expect[Cap^](io)
 
-    val op: Unit -> Unit = (x: Unit) =>
-      expect[Cap^] { // error
+    val op: Unit -> Unit = (x: Unit) => // error
+      expect[Cap^] {
         io.use()
         io
       }