Level checking: distinguish between certain capset vars with same owner

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

@@ -655,8 +655,15 @@ object CaptureSet:
   inline val debugVars = false
   inline val debugTarget = 1745
 
-  /** The subclass of captureset variables with given initial elements */
-  class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
+  /** The subclass of captureset variables with given initial elements
+   *  @param initialOwner  the initial owner. This is the real owner, except that
+   *                       it can be change in HiddenSets. Used for level checking
+   *                       if different from NoSymbol.
+   *  @param initialElems  the initial elements
+   *  @param nestedOK      relevant only if owner != NoSymbol. If true the set accepts
+   *                       elements that are directly owned by owner.
+   */
+  class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
 
     override def owner = initialOwner
 
@@ -682,7 +689,7 @@ object CaptureSet:
     protected var myElems: Refs = initialElems
 
     if debugVars && id == debugTarget then
-      println(i"###INIT ELEMS of $id to $initialElems")
+      println(i"###INIT ELEMS of $id of class $getClass in $initialOwner, $nestedOK to $initialElems")
       assert(false)
 
     def elems: Refs = myElems
@@ -828,15 +835,16 @@ object CaptureSet:
 
     def levelOK(elem: Capability)(using Context): Boolean = elem match
       case elem @ ResultCap(binder) =>
-        rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(binder.resType))
+        rootLimit == null && isPartOf(binder.resType)
       case GlobalCap =>
         rootLimit == null
       case elem: ParamRef =>
-        this.isInstanceOf[BiMapped] || isPartOf(elem.binder.resType)
+        isPartOf(elem.binder.resType)
       case _ =>
         if owner.exists then
           val elemVis = elem.visibility
           !elemVis.isProperlyContainedIn(owner)
+          || nestedOK && elemVis.owner == owner
         else true
 
     def addDependent(cs: CaptureSet)(using Context, VarState): Boolean =
@@ -950,6 +958,9 @@ object CaptureSet:
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
   extends Var(owner, initialElems):
 
+    override def levelOK(elem: Capability)(using Context): Boolean =
+      true
+
     // For debugging: A trace where a set was created. Note that logically it would make more
     // sense to place this variable in Mapped, but that runs afoul of the initialization checker.
     // val stack = if debugSets && this.isInstanceOf[Mapped] then (new Throwable).getStackTrace().take(20) else null
@@ -995,6 +1006,10 @@ object CaptureSet:
     (val source: Var, val bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
   extends DerivedVar(source.owner, initialElems):
 
+    if debugVars && id == debugTarget then
+      println(i"variable $id is derived from $source")
+      assert(false)
+
     override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
       if origin eq source then
         val mappedElem = bimap.mapCapability(elem)

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

@@ -430,7 +430,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
         if sym.isTerm || !sym.owner.isStaticOwner
-        then CaptureSet.Var(sym)
+        then CaptureSet.Var(sym, nestedOK = false)
         else CaptureSet.empty)
 
 // ---- Record Uses with MarkFree ----------------------------------------------------

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

@@ -495,7 +495,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     def transformResultType(tpt: TypeTree, sym: Symbol)(using Context): Unit =
       // First step: Transform the type and record it as knownType of tpt.
       try
-        transformTT(tpt, sym, boxed = false)
+        inContext(ctx.addMode(Mode.CCPreciseOwner)):
+          transformTT(tpt, sym, boxed = false)
       catch case ex: IllegalCaptureRef =>
         capt.println(i"fail while transforming result type $tpt of $sym")
         throw ex
@@ -851,7 +852,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
   /** Add a capture set variable to `tp` if necessary. */
   private def addVar(tp: Type, owner: Symbol)(using Context): Type =
-    decorate(tp, CaptureSet.Var(owner, _))
+    decorate(tp, CaptureSet.Var(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner)))
 
   /** A map that adds <fluid> capture sets at all contra- and invariant positions
    *  in a type where a capture set would be needed. This is used to make types

compiler/src/dotty/tools/dotc/core/Mode.scala

@@ -141,6 +141,15 @@ object Mode {
    */
   val InPackageClauseName: Mode = newMode(19, "InPackageClauseName")
 
+  /** When creating capset Vars in cc.Setup, mark the variable to be in
+   *  the result type of the context's owner, so that nested vals cannot
+   *  be included in it.
+   *  Reuses the value of InPackageClauseName to save Mode bits.
+   *  This is OK since InPackageClauseName is only set and tested during Typer,
+   *  and CCPreciseOwner only has an effect during phase CheckCaptures.
+   */
+  val CCPreciseOwner = InPackageClauseName
+
   /** We are in the IDE */
   val Interactive: Mode = newMode(20, "Interactive")
 

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

@@ -22,14 +22,14 @@ def main() =
   val untrustedLogger: Logger^ = ???
   val untrustedChannel: Channel[String]^ = ???
 
-  runSecure: () => // error (???, arose after changing level checking)
+  runSecure: () =>
     trustedLogger.log("Hello from trusted code") // ok
 
-  runSecure: () => // error (???, arose after changing level checking)
+  runSecure: () =>
     trustedChannel.send("I can send")
     trustedLogger.log(trustedChannel.recv()) // ok
 
-  runSecure: () => // error (???, arose after changing level checking)
+  runSecure: () =>
     "I am pure"                             // ok
 
   runSecure: () => // error

tests/neg-custom-args/captures/capset-members4.scala

@@ -11,8 +11,8 @@ def test =
     type C^ >: {z,x} <: {x,y,z}
 
   val foo: Foo = ???
-  onlyWithZ[{foo.C}] // error
-  onlyWithZ[{z}]     // error
-  onlyWithZ[{x,z}]   // error
-  onlyWithZ[{x,y,z}] // error
+  onlyWithZ[{foo.C}] // ok
+  onlyWithZ[{z}]     // ok
+  onlyWithZ[{x,z}]   // ok
+  onlyWithZ[{x,y,z}] // ok
   onlyWithZ[{x,y}]   // error

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

@@ -5,8 +5,8 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:22:46 ------------------------------------------------------------
 22 |    val boxed1 : ((C^) => Unit) -> Unit = box1(c)  // error
    |                                          ^^^^^^^
-   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
-   |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
+   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
+   |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
    |
    |where:    =>  refers to the universal root capability
    |          ^   refers to the universal root capability
@@ -15,8 +15,8 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:29:35 ------------------------------------------------------------
 29 |    val boxed2 : Observe[C^] = box2(c)  // error
    |                               ^^^^^^^
-   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
-   |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
+   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
+   |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
    |
    |where:    =>  refers to the universal root capability
    |          ^   refers to the universal root capability

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

@@ -19,18 +19,18 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:19:2 ----------------------------------------
 19 |  c // error
    |  ^
-   |  Found:    A^{io}
+   |  Found:    A^{c}
    |  Required: A
    |
-   |  Note that capability io is not included in capture set {}.
+   |  Note that capability c is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:27:2 ----------------------------------------
 27 |  c  // error
    |  ^
-   |  Found:    A^{io}
+   |  Found:    A^{c}
    |  Required: A
    |
-   |  Note that capability io is not included in capture set {}.
+   |  Note that capability c is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`

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

@@ -10,18 +10,18 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:24:2 -----------------------------------------
 24 |  x  // error
    |  ^
-   |  Found:    test.runnable.Transform{val fun: Any ->{a} Any}^{a}
+   |  Found:    test.runnable.Transform{val fun: Any ->{f} Any}^{x}
    |  Required: test.runnable.Transform
    |
-   |  Note that capability a is not included in capture set {}.
+   |  Note that capability x is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:31:2 -----------------------------------------
 31 |  x  // error
    |  ^
-   |  Found:    test.runnable.Transform{val fun: Any ->{a} Any}^{a}
+   |  Found:    test.runnable.Transform{val fun: Any ->{f} Any}^{x}
    |  Required: test.runnable.Transform
    |
-   |  Note that capability a is not included in capture set {}.
+   |  Note that capability x is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/real-try.check

@@ -39,12 +39,10 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/real-try.scala:33:8 --------------------------------------
 33 |    Cell(() => foo(1)) // error
    |    ^^^^^^^^^^^^^^^^^^
-   |  Found:    Cell[() => Unit]
-   |  Required: Cell[() ->'s5 Unit]^'s6
+   |    Found:    Cell[() ->{canThrow$4} Unit]
+   |    Required: Cell[() ->'s5 Unit]^'s6
    |
-   |  Note that capability cap cannot be included in outer capture set 's5 of value b.
-   |
-   |  where:    =>  refers to a fresh root capability classified as Control in the type of given instance canThrow$4
-   |            cap is a fresh root capability classified as Control in the type of given instance canThrow$4
+   |    Note that capability canThrow$4, defined in method try$4
+   |    cannot be included in outer capture set 's5 of value b.
    |
    | longer explanation available when compiling with `-explain`

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

@@ -2,9 +2,9 @@
 12 |  def mkCounter(): Pair[Ref^, Ref^] =  // error
    |                   ^^^^^^^^^^^^^^^^
    | Separation failure in method mkCounter's result type Pair[Ref^, Ref^²].
-   | One part,  Ref^, hides capabilities  {cap}.
-   | Another part,  Ref^²,  captures capabilities  {cap}.
-   | The two sets overlap at  cap of method mkCounter.
+   | One part,  Ref^, hides capabilities  {c, cap}.
+   | Another part,  Ref^²,  captures capabilities  {c, cap}.
+   | The two sets overlap at  {c}.
    |
    | where:    ^   refers to a fresh root capability classified as Mutable in the result type of method mkCounter
    |           ^²  refers to a fresh root capability classified as Mutable in the result type of method mkCounter

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

@@ -12,9 +12,9 @@
 13 |def bad: Pair[Ref^, Ref^] =  // error: overlap at r1*, r0
    |         ^^^^^^^^^^^^^^^^
    |         Separation failure in method bad's result type Pair[Ref^, Ref^²].
-   |         One part,  Ref^, hides capabilities  {cap, cap², r0}.
-   |         Another part,  Ref^²,  captures capabilities  {cap, cap², r0}.
-   |         The two sets overlap at  {r0}.
+   |         One part,  Ref^, hides capabilities  {r1*, cap, cap², r0}.
+   |         Another part,  Ref^²,  captures capabilities  {r1*, cap, cap², r0}.
+   |         The two sets overlap at  {r1*, r0}.
    |
    |         where:    ^    refers to a fresh root capability classified as Mutable in the result type of method bad
    |                   ^²   refers to a fresh root capability classified as Mutable in the result type of method bad

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

@@ -28,16 +28,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:36:10 -----------------------------------------
 36 |  local { cap3 => // error
    |          ^
-   |Found:    (cap3: CC^) ->'s1 String => String
-   |Required: CC^ -> String =>² String
+   |          Found:    (cap3: CC^) ->'s1 String ->{cap3} String
+   |          Required: CC^ -> String ->{cap3²} String
    |
-   |Note that capability cap cannot be included in outer capture set {cap²}.
+   |          Note that capability cap3 cannot be included in outer capture set {cap3²}.
    |
-   |where:    =>   refers to a root capability associated with the result type of (cap3: CC^): String => String
-   |          =>²  refers to a fresh root capability created in method test of parameter parameter cap3² of method $anonfun
-   |          ^    refers to the universal root capability
-   |          cap  is a root capability associated with the result type of (cap3: CC^): String =>² String
-   |          cap² is a fresh root capability created in method test of parameter parameter cap3² of method $anonfun
+   |          where:    ^     refers to the universal root capability
+   |                    cap3  is a reference to a value parameter
+   |                    cap3² is a parameter in an anonymous function in method test
 37 |    def g(x: String): String = if cap3 == cap3 then "" else "a"
 38 |    g
    |

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

@@ -0,0 +1,9 @@
+import language.experimental.captureChecking
+import caps.*
+def test1() =
+  val z: Any^ = ???
+  def onlyWithZ[C^](using c: Contains[C, z.type]) = ???
+  onlyWithZ[{z}]     // error, but should be ok
+def test2(z: Any^) =
+  def onlyWithZ[C^](using c: Contains[C, z.type]) = ???
+  onlyWithZ[{z}]     // ok