Revise separation checks

 - Compute dependencies of later arguments to earlier ones
 - Don't add to initial footprint references implied by a dependency
 - Don't add to overlap references implied by a dependency
 - Make error diagnostics better structured and clearer

Author: odersky

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

@@ -80,6 +80,11 @@ sealed abstract class CaptureSet extends Showable:
     assert(!isConst)
     asInstanceOf[Var]
 
+  /** Convert to Const with current elements unconditionally */
+  def toConst: Const = this match
+    case c: Const => c
+    case v: Var => Const(v.elems)
+
   /** Does this capture set contain the root reference `cap` as element? */
   final def isUniversal(using Context) =
     elems.exists(_.isCap)
@@ -270,6 +275,9 @@ sealed abstract class CaptureSet extends Showable:
     else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
     else Union(this, that)
 
+  def ++ (that: CaptureSet.Const)(using Context): CaptureSet.Const =
+    Const(this.elems ++ that.elems)
+
   /** The smallest superset (via <:<) of this capture set that also contains `ref`.
    */
   def + (ref: CaptureRef)(using Context): CaptureSet =

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

@@ -89,6 +89,7 @@ object CheckCaptures:
           tp
         case _ =>
           mapOver(tp)
+    override def toString = "SubstParamsMap"
   end SubstParamsMap
 
   /** Used for substituting parameters in a special case: when all actual arguments
@@ -108,6 +109,7 @@ object CheckCaptures:
         tp
       case _ =>
         mapOver(tp)
+    override def toString = "SubstParamsBiMap"
 
     lazy val inverse = new BiTypeMap:
       def apply(tp: Type): Type = tp match
@@ -124,6 +126,7 @@ object CheckCaptures:
           tp
         case _ =>
           mapOver(tp)
+      override def toString = "SubstParamsBiMap.inverse"
       def inverse = thisMap
   end SubstParamsBiMap
 

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

@@ -16,12 +16,12 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   import checker.*
 
   extension (cs: CaptureSet)
-    def footprint(using Context): CaptureSet =
+    def footprint(using Context): CaptureSet.Const =
       def recur(elems: CaptureSet.Refs, newElems: List[CaptureRef]): CaptureSet.Refs = newElems match
         case newElem :: newElems1 =>
           val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
             !superElem.isMaxCapability && !elems.contains(superElem)
-          recur(superElems ++ elems, superElems.toList ++ newElems1)
+          recur(elems ++ superElems, newElems1 ++ superElems.toList)
         case Nil => elems
       val elems: CaptureSet.Refs = cs.elems.filter(!_.isMaxCapability)
       CaptureSet(recur(elems, elems.toList))
@@ -56,12 +56,23 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     recur(cs)
   end hidden
 
-  def captures(arg: Tree)(using Context): CaptureSet =
+  /** The captures of an argument or prefix widened to the formal parameter, if
+   *  the latter contains a cap.
+   */
+  def formalCaptures(arg: Tree)(using Context): CaptureSet.Const =
     val argType = arg.nuType
-    if argType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet
+    (if argType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet)
+      .toConst
+
+   /** The captures of an argument of prefix. No widening takes place */
+  def actualCaptures(arg: Tree)(using Context): CaptureSet.Const =
+    val argType = arg.actualType.orElse(arg.nuType)
+    (if arg.nuType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet)
+      .toConst
 
   private def sepError(fn: Tree, args: List[Tree], argIdx: Int,
-      overlap: Refs, hiddenInArg: CaptureSet, footprints: List[(CaptureSet, Int)])(using Context): Unit =
+      overlap: Refs, hiddenInArg: CaptureSet, footprints: List[(CaptureSet, Int)],
+      deps: collection.Map[Tree, List[Tree]])(using Context): Unit =
     val arg = args(argIdx)
     def paramName(mt: Type, idx: Int): Option[Name] = mt match
       case mt @ MethodType(pnames) =>
@@ -73,11 +84,11 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       case _ => ""
     def whatStr = if overlap.size == 1 then "this capability is" else "these capabilities are"
     def funStr =
-      if fn.symbol.exists then i"${fn.symbol}"
-      else "the function"
+      if fn.symbol.exists then i"${fn.symbol}: ${fn.symbol.info}"
+      else i"a function of type ${fn.nuType.widen}"
     val clashIdx = footprints
       .collect:
-        case (fp, idx) if !hiddenInArg.footprint.overlapWith(fp).isEmpty => idx
+        case (fp, idx) if !hiddenInArg.overlapWith(fp).isEmpty => idx
       .head
     def whereStr = clashIdx match
       case 0 => "function prefix"
@@ -90,62 +101,98 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       else args(clashIdx - 1)
     def clashType =
       clashTree.actualType.orElse(clashTree.nuType)
-    def clashCaptures = captures(clashTree)
-    def clashHidden = CaptureSet(hidden(clashCaptures))
-    def hiddenCaptures = CaptureSet(hidden(captures(arg)))
-    def clashFootprint = clashCaptures.footprint ++ clashHidden.footprint
+    def clashCaptures = actualCaptures(clashTree)
+    def clashHidden = CaptureSet(hidden(formalCaptures(clashTree)))
+    def hiddenCaptures = CaptureSet(hidden(formalCaptures(arg)))
+    def clashFootprint = clashCaptures.footprint
     def hiddenFootprint = hiddenCaptures.footprint
+    def declaredFootprint = CaptureSet(deps(arg).map(actualCaptures(_).elems).foldLeft(emptySet)(_ ++ _)).footprint
+    def footprintOverlap = CaptureSet(hiddenFootprint.overlapWith(clashFootprint) -- declaredFootprint.elems)
     def clashHiddenStr =
       if clashTree.needsSepCheck then
-        i"\n  Hidden set of $whereStr       : $clashHidden"
+        i"\n  Hidden set of $whereStr         : $clashHidden"
       else ""
     report.error(
-      em"""Separation failure: argument of type ${arg.actualType} to capture-polymorphic parameter
-          |${formalName}of type ${arg.nuType} captures ${CaptureSet(overlap)}, and $whatStr also passed
-          |separately in the ${whereStr.trim} with type $clashType to $funStr.
+      em"""Separation failure: argument of type  ${arg.actualType}
+          |to $funStr
+          |corresponds to capture-polymorphic formal parameter ${formalName}of type  ${arg.nuType}
+          |and captures ${CaptureSet(overlap)}, but $whatStr also passed separately
+          |in the ${whereStr.trim} with type  $clashType.
           |
-          |  Capture set of $whereStr      : $clashCaptures$clashHiddenStr
-          |  Hidden set of current argument      : $hiddenCaptures
-          |  Footprint of $whereStr        : $clashFootprint
-          |  Hidden footprint of current argument: $hiddenFootprint
-          |  Overlap of footprints               : ${CaptureSet(hiddenFootprint.overlapWith(clashFootprint))}""",
+          |  Capture set of $whereStr        : $clashCaptures
+          |  Hidden set of current argument        : $hiddenCaptures
+          |  Footprint of $whereStr          : $clashFootprint
+          |  Hidden footprint of current argument  : $hiddenFootprint
+          |  Declared footprint of current argument: $declaredFootprint
+          |  Undeclared overlap of footprints      : $footprintOverlap""",
       arg.srcPos)
   end sepError
 
-  private def checkApply(fn: Tree, args: List[Tree])(using Context): Unit =
-    val fnCaptures =
-      if true then
-        fn.nuType.deepCaptureSet
-      else methPart(fn) match
-        case Select(qual, _) => qual.nuType.deepCaptureSet
-        case _ => CaptureSet.empty
-    val argCaptures = args.map(captures)
-    capt.println(i"check separate $fn($args), fnCaptures = $fnCaptures, argCaptures = $argCaptures")
+  private def checkApply(fn: Tree, args: List[Tree], deps: collection.Map[Tree, List[Tree]])(using Context): Unit =
+    val fnCaptures = methPart(fn) match
+      case Select(qual, _) => qual.nuType.captureSet
+      case _ => CaptureSet.empty
+    capt.println(i"check separate $fn($args), fnCaptures = $fnCaptures, argCaptures = ${args.map(formalCaptures)}, deps = ${deps.toList}")
     var footprint = fnCaptures.footprint
     val footprints = mutable.ListBuffer[(CaptureSet, Int)]((footprint, 0))
     val indexedArgs = args.zipWithIndex
+
+    def subtractDeps(elems: Refs, arg: Tree): Refs =
+      deps(arg).foldLeft(elems): (elems, dep) =>
+        elems -- actualCaptures(dep).footprint.elems
+
     for (arg, idx) <- indexedArgs do
       if !arg.needsSepCheck then
-        footprint = footprint ++ captures(arg)
+        footprint = footprint ++ CaptureSet(subtractDeps(actualCaptures(arg).footprint.elems, arg))
         footprints += ((footprint, idx + 1))
     for (arg, idx) <- indexedArgs do
       if arg.needsSepCheck then
-        val ac = captures(arg)
+        val ac = formalCaptures(arg)
         val hiddenInArg = CaptureSet(hidden(ac)).footprint
         //println(i"check sep $arg: $ac, footprint so far = $footprint, hidden = $hiddenInArg")
-        val overlap = hiddenInArg.footprint.overlapWith(footprint)
+        val overlap = subtractDeps(hiddenInArg.overlapWith(footprint), arg)
         if !overlap.isEmpty then
-          sepError(fn, args, idx, overlap, hiddenInArg, footprints.toList)
-        footprint = footprint ++ hiddenInArg.footprint ++ ac.footprint
+          sepError(fn, args, idx, overlap, hiddenInArg, footprints.toList, deps)
+        footprint ++= actualCaptures(arg).footprint
         footprints += ((footprint, idx + 1))
   end checkApply
 
+  private def collectMethodTypes(tp: Type): List[TermLambda] = tp match
+    case tp: MethodType => tp :: collectMethodTypes(tp.resType)
+    case tp: PolyType => collectMethodTypes(tp.resType)
+    case _ => Nil
+
+  private def dependencies(fn: Tree, argss: List[List[Tree]])(using Context): collection.Map[Tree, List[Tree]] =
+    val mtpe =
+      if fn.symbol.exists then fn.symbol.info
+      else fn.tpe.widen // happens for PolyFunction applies
+    val mtps = collectMethodTypes(mtpe)
+    assert(mtps.hasSameLengthAs(argss), i"diff for $fn: ${fn.symbol} /// $mtps /// $argss")
+    val mtpsWithArgs = mtps.zip(argss)
+    val argMap = mtpsWithArgs.toMap
+    val deps = mutable.HashMap[Tree, List[Tree]]().withDefaultValue(Nil)
+    for
+      (mt, args) <- mtpsWithArgs
+      (formal, arg) <- mt.paramInfos.zip(args)
+      dep <- formal.captureSet.elems.toList
+    do
+      val referred = dep match
+        case dep: TermParamRef =>
+          argMap(dep.binder)(dep.paramNum) :: Nil
+        case dep: ThisType if dep.cls == fn.symbol.owner =>
+          val Select(qual, _) = fn: @unchecked
+          qual :: Nil
+        case _ =>
+          Nil
+      deps(arg) ++= referred
+    deps
+
   private def traverseApply(tree: Tree, argss: List[List[Tree]])(using Context): Unit = tree match
     case Apply(fn, args) => traverseApply(fn, args :: argss)
     case TypeApply(fn, args) => traverseApply(fn, argss) // skip type arguments
     case _ =>
       if argss.nestedExists(_.needsSepCheck) then
-        checkApply(tree, argss.flatten)
+        checkApply(tree, argss.flatten, dependencies(tree, argss))
 
   def traverse(tree: Tree)(using Context): Unit =
     tree match

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

@@ -132,8 +132,9 @@ object Synthetics:
       val (pt: PolyType) = info: @unchecked
       val (mt: MethodType) = pt.resType: @unchecked
       val (enclThis: ThisType) = owner.thisType: @unchecked
+      val paramCaptures = CaptureSet(enclThis, defn.captureRoot.termRef)
       pt.derivedLambdaType(resType = MethodType(mt.paramNames)(
-        mt1 => mt.paramInfos.map(_.capturing(CaptureSet.universal)),
+        mt1 => mt.paramInfos.map(_.capturing(paramCaptures)),
         mt1 => CapturingType(mt.resType, CaptureSet(enclThis, mt1.paramRefs.head))))
 
     def transformCurriedTupledCaptures(info: Type, owner: Symbol) =
@@ -148,7 +149,10 @@ object Synthetics:
       ExprType(mapFinalResult(et.resType, CapturingType(_, CaptureSet(enclThis))))
 
     def transformCompareCaptures =
-      MethodType(defn.ObjectType.capturing(CaptureSet.universal) :: Nil, defn.BooleanType)
+      val (enclThis: ThisType) = symd.owner.thisType: @unchecked
+      MethodType(
+        defn.ObjectType.capturing(CaptureSet(defn.captureRoot.termRef, enclThis)) :: Nil,
+        defn.BooleanType)
 
     symd.copySymDenotation(info = symd.name match
       case DefaultGetterName(nme.copy, n) =>

scala2-library-cc/src/scala/collection/IterableOnce.scala

@@ -805,7 +805,7 @@ trait IterableOnceOps[+A, +CC[_], +C] extends Any { this: IterableOnce[A]^ =>
       case  _ => Some(reduceLeft(op))
     }
   private final def reduceLeftOptionIterator[B >: A](op: (B, A) => B): Option[B] = reduceOptionIterator[A, B](iterator)(op)
-  private final def reduceOptionIterator[X >: A, B >: X](it: Iterator[X]^)(op: (B, X) => B): Option[B] = {
+  private final def reduceOptionIterator[X >: A, B >: X](it: Iterator[X]^{this, caps.cap})(op: (B, X) => B): Option[B] = {
     if (it.hasNext) {
       var acc: B = it.next()
       while (it.hasNext)

tests/neg-custom-args/captures/caseclass/Test_2.scala

@@ -5,7 +5,7 @@ def test(c: C) =
   val mixed: () ->{c} Unit = pure
   val x = Ref(impure)
   val _: Ref = x // error
-  val y = x.copy()
+  val y = caps.unsafe.unsafeAssumeSeparate(x.copy()) // TODO remove
   val yc: Ref = y // error
   val y0 = x.copy(pure)
   val yc0: Ref = y0

tests/neg-custom-args/captures/filevar-expanded.check

@@ -1,16 +1,18 @@
 -- Error: tests/neg-custom-args/captures/filevar-expanded.scala:34:19 --------------------------------------------------
 34 |    withFile(io3): f => // error: separation failure
    |                   ^
-   |        Separation failure: argument of type (f: test2.File^{io3}) ->{io3} Unit to capture-polymorphic parameter
-   |        op of type (f: test2.File^{io3}) => Unit captures {io3}, and this capability is also passed
-   |        separately in the first argument with type (io3 : test2.IO^) to method withFile.
+   |                   Separation failure: argument of type  (f: test2.File^{io3}) ->{io3} Unit
+   |                   to method withFile: [T](io2: test2.IO^)(op: (f: test2.File^{io2}) => T): T
+   |                   corresponds to capture-polymorphic formal parameter op of type  (f: test2.File^{io3}) => Unit
+   |                   and captures {io3}, but this capability is also passed separately
+   |                   in the first argument with type  (io3 : test2.IO^).
    |
-   |          Capture set of first argument       : {cap}
-   |          Hidden set of first argument        : {io3}
-   |          Hidden set of current argument      : {io3}
-   |          Footprint of first argument         : {io3}
-   |          Hidden footprint of current argument: {io3}
-   |          Overlap of footprints               : {io3}
+   |                     Capture set of first argument         : {io3}
+   |                     Hidden set of current argument        : {io3}
+   |                     Footprint of first argument           : {io3}
+   |                     Hidden footprint of current argument  : {io3}
+   |                     Declared footprint of current argument: {}
+   |                     Undeclared overlap of footprints      : {io3}
 35 |      val o = Service(io3)
 36 |      o.file = f  // this is a bit dubious. It's legal since we treat class refinements
 37 |                  // as capture set variables that can be made to include refs coming from outside.

tests/neg-custom-args/captures/function-combinators.check

@@ -29,12 +29,15 @@
 -- Error: tests/neg-custom-args/captures/lazyref.scala:24:55 -----------------------------------------------------------
 24 |  val ref4 = (if cap1 == cap2 then ref1 else ref2).map(g) // error: separation failure
    |                                                       ^
-   |Separation failure: argument of type (x: Int) ->{cap2} Int to capture-polymorphic parameter
-   |f of type Int => Int captures {cap2}, and this capability is also passed
-   |separately in the function prefix with type (LazyRef[Int]{val elem: () ->{ref2*} Int} | (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}))^{ref2} to method map.
+   |Separation failure: argument of type  (x: Int) ->{cap2} Int
+   |to method map: [U](f: T => U): LazyRef[U]^{f, LazyRef.this}
+   |corresponds to capture-polymorphic formal parameter f of type  Int => Int
+   |and captures {cap2}, but this capability is also passed separately
+   |in the function prefix with type  (LazyRef[Int]{val elem: () ->{ref2*} Int} | (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}))^{ref2}.
    |
-   |  Capture set of function prefix      : {ref1, ref2}
-   |  Hidden set of current argument      : {cap2}
-   |  Footprint of function prefix        : {cap2, cap1, ref1, ref2}
-   |  Hidden footprint of current argument: {cap2}
-   |  Overlap of footprints               : {cap2}
+   |  Capture set of function prefix        : {ref1, ref2}
+   |  Hidden set of current argument        : {cap2}
+   |  Footprint of function prefix          : {ref1, ref2, cap1, cap2}
+   |  Hidden footprint of current argument  : {cap2}
+   |  Declared footprint of current argument: {}
+   |  Undeclared overlap of footprints      : {cap2}