SepCheck: Record span capture sets instead of deep capture sets

Author: odersky

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

@@ -157,8 +157,8 @@ extension (tp: Type)
    *  a singleton capability `x` or a reach capability `x*`, the deep capture
    *  set can be narrowed to`{x*}`.
    */
-  def deepCaptureSet(includeTypevars: Boolean)(using Context): CaptureSet =
-    val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing, includeTypevars)
+  def deepCaptureSet(includeTypevars: Boolean, includeBoxed: Boolean = true)(using Context): CaptureSet =
+    val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing, includeTypevars, includeBoxed)
     if dcs.isAlwaysEmpty then tp.captureSet
     else tp match
       case tp: ObjectCapability if tp.isTrackableRef => tp.reach.singletonCaptureSet
@@ -167,6 +167,9 @@ extension (tp: Type)
   def deepCaptureSet(using Context): CaptureSet =
     deepCaptureSet(includeTypevars = false)
 
+  def spanCaptureSet(using Context): CaptureSet =
+    deepCaptureSet(includeTypevars = false, includeBoxed = false)
+
   /** A type capturing `ref` */
   def capturing(ref: Capability)(using Context): Type =
     if tp.captureSet.accountsFor(ref) then tp
@@ -362,7 +365,7 @@ extension (tp: Type)
    */
   def derivesFromCapTraitDeeply(cls: ClassSymbol)(using Context): Boolean =
     val accumulate = new DeepTypeAccumulator[Boolean]:
-      def capturingCase(acc: Boolean, parent: Type, refs: CaptureSet) =
+      def capturingCase(acc: Boolean, parent: Type, refs: CaptureSet, boxed: Boolean) =
         this(acc, parent)
         && (parent.derivesFromCapTrait(cls)
             || refs.isConst && refs.elems.forall(_.derivesFromCapTrait(cls)))
@@ -734,15 +737,15 @@ object ContainsParam:
 abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
   val seen = util.HashSet[Symbol]()
 
-  protected def capturingCase(acc: T, parent: Type, refs: CaptureSet): T
+  protected def capturingCase(acc: T, parent: Type, refs: CaptureSet, boxed: Boolean): T
 
   protected def abstractTypeCase(acc: T, t: TypeRef, upperBound: Type): T
 
   def apply(acc: T, t: Type) =
     if variance < 0 then acc
     else t.dealias match
       case t @ CapturingType(parent, cs) =>
-        capturingCase(acc, parent, cs)
+        capturingCase(acc, parent, cs, t.isBoxed)
       case t: TypeRef if t.symbol.isAbstractOrParamType && !seen.contains(t.symbol) =>
         seen += t.symbol
         abstractTypeCase(acc, t, t.info.bounds.hi)

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

@@ -957,7 +957,7 @@ object CaptureSet:
   /** Variables created in types of inferred type trees */
   class ProperVar(override val owner: Symbol, initialElems: Refs, nestedOK: Boolean)(using /*@constructorOnly*/ ictx: Context)
   extends Var(owner, initialElems, nestedOK)
-  
+
   /** A variable that is derived from some other variable via a map or filter. */
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
   extends Var(owner, initialElems):
@@ -1619,13 +1619,17 @@ object CaptureSet:
   /** The deep capture set of a type is the union of all covariant occurrences of
    *  capture sets. Nested existential sets are approximated with `cap`.
    */
-  def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false)(using Context): CaptureSet =
+  def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false, includeBoxed: Boolean = true)(using Context): CaptureSet =
     val collect = new DeepTypeAccumulator[CaptureSet]:
-      def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet) =
-        this(acc, parent) ++ refs
+
+      def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet, boxed: Boolean) =
+        if includeBoxed || !boxed then this(acc, parent) ++ refs
+        else this(acc, parent)
+
       def abstractTypeCase(acc: CaptureSet, t: TypeRef, upperBound: Type) =
         if includeTypevars && upperBound.isExactlyAny then fresh(Origin.DeepCS(t))
         else this(acc, upperBound)
+
     collect(CaptureSet.empty, tp)
 
   type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[Capability]]

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

@@ -312,8 +312,12 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   private def formalCaptures(arg: Tree)(using Context): Refs =
     arg.formalType.orElse(arg.nuType).deepCaptureSet.elems
 
-   /** The deep capture set if the type of `tree` */
+   /** The span capture set if the type of `tree` */
   private def captures(tree: Tree)(using Context): Refs =
+   tree.nuType.spanCaptureSet.elems
+
+   /** The deep capture set if the type of `tree` */
+  private def deepCaptures(tree: Tree)(using Context): Refs =
    tree.nuType.deepCaptureSet.elems
 
   // ---- Error reporting TODO Once these are stabilized, move to messages -----" +
@@ -376,7 +380,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       if clashIdx == 0 && !isShowableMethod then "" // we already mentioned the type in `funStr`
       else i" with type  ${clashing.nuType}"
     val hiddenSet = formalCaptures(polyArg).hiddenSet
-    val clashSet = captures(clashing)
+    val clashSet = deepCaptures(clashing)
     report.error(
       em"""Separation failure: argument of type  ${polyArg.nuType}
           |to $funStr

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

@@ -1,11 +1,3 @@
--- Error: tests/neg-custom-args/captures/sepchecks2.scala:10:10 --------------------------------------------------------
-10 |  println(c) // error
-   |          ^
-   |          Separation failure: Illegal access to {c} which is hidden by the previous definition
-   |          of value xs with type List[() => Unit].
-   |          This type hides capabilities  {c}
-   |
-   |          where:    => refers to a fresh root capability in the type of value xs
 -- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:7 ---------------------------------------------------------
 13 |  foo((() => println(c)) :: Nil, c) // error
    |       ^^^^^^^^^^^^^^^^^^^^^^^^

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

@@ -7,7 +7,7 @@ def bar(x: (Object^, Object^)): Unit = ???
 
 def Test(consume c: Object^) =
   val xs: List[() => Unit] = (() => println(c)) :: Nil
-  println(c) // error
+  println(c)
 
 def Test2(c: Object^, d: Object^): Unit =
   foo((() => println(c)) :: Nil, c) // error

tests/neg-custom-args/captures/unsound-reach-6.check

@@ -26,7 +26,3 @@
    |              ^^
    |              Local reach capability ys* leaks into capture scope of method test.
    |              You could try to abstract the capabilities referred to by ys* in a capset variable.
--- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
-19 |    val z = f(ys)  // error consume failure
-   |              ^^
-   |Separation failure: argument to consume parameter with type List[() ->{io} Unit] refers to non-local parameter io

tests/neg-custom-args/captures/unsound-reach-6.scala

@@ -16,7 +16,7 @@ def test(io: IO^)(ys: List[() ->{io} Unit]) =
 def test(io: IO^) =
   def ys: List[() ->{io} Unit] = ???
   val x = () =>
-    val z = f(ys)  // error consume failure
+    val z = f(ys)  // ok, was error consume failure
     z()
   val _: () -> Unit = x // error
   ()