Give some explanation of a capture set was under-approximated

Author: odersky

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

@@ -244,7 +244,8 @@ extension (tp: Type)
    *  the two capture sets are combined.
    */
   def capturing(cs: CaptureSet)(using Context): Type =
-    if cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, frozen = true).isOK
+    if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, frozen = true).isOK)
+        && !cs.keepAlways
     then tp
     else tp match
       case CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs)

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

@@ -88,6 +88,8 @@ sealed abstract class CaptureSet extends Showable:
   final def isUnboxable(using Context) =
     elems.exists(elem => elem.isRootCapability || Existential.isExistentialVar(elem))
 
+  final def keepAlways: Boolean = this.isInstanceOf[EmptyWithProvenance]
+
   /** Try to include an element in this capture set.
    *  @param elem    The element to be added
    *  @param origin  The set that originated the request, or `empty` if the request came from outside.
@@ -219,7 +221,8 @@ sealed abstract class CaptureSet extends Showable:
    *  `this` and `that`
    */
   def ++ (that: CaptureSet)(using Context): CaptureSet =
-    if this.subCaptures(that, frozen = true).isOK then that
+    if this.subCaptures(that, frozen = true).isOK then
+      if that.isAlwaysEmpty && this.keepAlways then this else that
     else if that.subCaptures(this, frozen = true).isOK then this
     else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
     else Union(this, that)
@@ -294,7 +297,7 @@ sealed abstract class CaptureSet extends Showable:
     case _ =>
       val mapped = mapRefs(elems, tm, tm.variance)
       if isConst then
-        if mapped.isConst && mapped.elems == elems then this
+        if mapped.isConst && mapped.elems == elems && !mapped.keepAlways then this
         else mapped
       else Mapped(asVar, tm, tm.variance, mapped)
 
@@ -398,6 +401,12 @@ object CaptureSet:
     override def toString = elems.toString
   end Const
 
+  case class EmptyWithProvenance(ref: CaptureRef, mapped: Type) extends Const(SimpleIdentitySet.empty):
+    override def optionalInfo(using Context): String =
+      if ctx.settings.YccDebug.value
+      then i" under-approximating the result of mapping $ref to $mapped"
+      else ""
+
   /** A special capture set that gets added to the types of symbols that were not
    *  themselves capture checked, in order to admit arbitrary corresponding capture
    *  sets in subcapturing comparisons. Similar to platform types for explicit
@@ -863,7 +872,7 @@ object CaptureSet:
       || upper.isConst && upper.elems.size == 1 && upper.elems.contains(r1)
       || r.derivesFrom(defn.Caps_CapSet)
     if variance > 0 || isExact then upper
-    else if variance < 0 then CaptureSet.empty
+    else if variance < 0 then CaptureSet.EmptyWithProvenance(r, r1)
     else upper.maybe
 
   /** Apply `f` to each element in `xs`, and join result sets with `++` */

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

@@ -33,7 +33,7 @@ object CapturingType:
    *  boxing status is the same or if A is boxed.
    */
   def apply(parent: Type, refs: CaptureSet, boxed: Boolean = false)(using Context): Type =
-    if refs.isAlwaysEmpty then parent
+    if refs.isAlwaysEmpty && !refs.keepAlways then parent
     else parent match
       case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed =>
         apply(parent1, refs ++ refs1, boxed)

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

@@ -990,6 +990,25 @@ class CheckCaptures extends Recheck, SymTransformer:
               |
               |Note that ${msg.toString}"""
 
+    private def addApproxAddenda(using Context) =
+      new TypeAccumulator[Addenda]:
+        def apply(add: Addenda, t: Type) = t match
+          case CapturingType(t, CaptureSet.EmptyWithProvenance(ref, mapped)) =>
+            /* val (origCore, kind) = original match
+              case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) =>
+                (parent, " deep")
+              case _ =>
+                (original, "")*/
+            add ++ new Addenda:
+              override def toAdd(using Context): List[String] =
+                i"""
+                   |
+                   |Note that a capability $ref in a capture set appearing in contravariant position
+                   |was mapped to $mapped which is not a capability. Therefore, it was under-approximated to the empty set."""
+                :: Nil
+          case _ =>
+            foldOver(add, t)
+
     /** Massage `actual` and `expected` types before checking conformance.
      *  Massaging is done by the methods following this one:
      *   - align dependent function types and add outer references in the expected type
@@ -1015,7 +1034,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       else
         capt.println(i"conforms failed for ${tree}: $actual vs $expected")
         err.typeMismatch(tree.withType(actualBoxed), expected1,
-            addenda ++ CaptureSet.levelErrors ++ boxErrorAddenda(boxErrors))
+            addApproxAddenda(
+              addenda ++ CaptureSet.levelErrors ++ boxErrorAddenda(boxErrors),
+              expected1))
         actual
     end checkConformsExpr
 

tests/neg-custom-args/captures/class-contra.check

@@ -1,7 +1,10 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:39 ---------------------------------
 12 |  def fun(x: K{val f: T^{a}}) = x.setf(a) // error
    |                                       ^
-   |                                       Found:    (a : T^{x, y})
-   |                                       Required: T
+   |   Found:    (a : T^{x, y})
+   |   Required: T^{}
+   |
+   |   Note that a capability (K.this.f : T^) in a capture set appearing in contravariant position
+   |   was mapped to (x.f : T^{a}) which is not a capability. Therefore, it was under-approximated to the empty set.
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/explain-under-approx.check

@@ -0,0 +1,20 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:12:10 -------------------------
+12 |  col.add(Future(() => 25)) // error
+   |          ^^^^^^^^^^^^^^^^
+   |       Found:    Future[Int]{val a: (async : Async^)}^{async}
+   |       Required: Future[Int]^{}
+   |
+   |       Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
+   |       was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:15:11 -------------------------
+15 |  col1.add(Future(() => 25)) // error
+   |           ^^^^^^^^^^^^^^^^
+   |      Found:    Future[Int]{val a: (async : Async^)}^{async}
+   |      Required: Future[Int]^{}
+   |
+   |      Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
+   |      was mapped to col1.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/explain-under-approx.scala

@@ -0,0 +1,17 @@
+trait Async extends caps.Capability
+
+class Future[+T](x: () => T)(using val a: Async)
+
+class Collector[T](val futs: Seq[Future[T]^]):
+  def add(fut: Future[T]^{futs*}) = ???
+
+def main() =
+  given async: Async = ???
+  val futs = (1 to 20).map(x => Future(() => x))
+  val col = Collector(futs)
+  col.add(Future(() => 25)) // error
+  val col1: Collector[Int] { val futs: Seq[Future[Int]^{async}] }
+    = Collector(futs)
+  col1.add(Future(() => 25)) // error
+
+