Disentangle VAR improvement and reach improvement

Make reach improvement also dependent on migthSubCapture

Author: odersky

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

@@ -401,9 +401,12 @@ extension (tp: Type)
           if variance <= 0 then t
           else t.dealias match
             case t @ CapturingType(p, cs) if cs.containsCapOrFresh =>
-              change = true
               val reachRef = if cs.isReadOnly then ref.reach.readOnly else ref.reach
-              t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet)
+              if reachRef.singletonCaptureSet.mightSubcapture(cs) then
+                change = true
+                t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet)
+              else
+                t
             case t @ AnnotatedType(parent, ann) =>
               // Don't map annotations, which includes capture sets
               t.derivedAnnotatedType(this(parent), ann)

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

@@ -1550,11 +1550,9 @@ class CheckCaptures extends Recheck, SymTransformer:
     private def improveCaptures(widened: Type, prefix: Type)(using Context): Type = prefix match
       case ref: Capability if ref.isTracked =>
         widened match
-          case widened @ CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) =>
-            val improvedCs =
-              if widened.isBoxed then ref.reach.singletonCaptureSet
-              else ref.singletonCaptureSet
-            widened.derivedCapturingType(p, improvedCs)
+          case widened @ CapturingType(p, refs)
+          if ref.singletonCaptureSet.mightSubcapture(refs) && !widened.isBoxed =>
+            widened.derivedCapturingType(p, ref.singletonCaptureSet)
               .showing(i"improve $widened to $result", capt)
           case _ => widened
       case _ => widened

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

@@ -1,12 +1,8 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches2.scala:10:8 --------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches2.scala:10:10 -------------------------------------
 10 |  ps.map((x, y) => compose1(x, y)) // error
-   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |  Found:    List[A^? ->{ps*, cap, cap²} A^?]
-   |  Required: List[A ->{ps*} A]
-   |
-   |  where:    cap  is a fresh root capability created in method mapCompose when computing deep capture set of A
-   |            cap² is a fresh root capability created in method mapCompose when computing deep capture set of A
-   |
-   |  Note that capability cap is not included in capture set {ps*}.
+   |          ^^^^^^^^^^^^^^^^^^^^^^^
+   |          Found:    (x$1: (A^? ->{ps*} A^?, A^? ->{ps*} A^?)^?) ->{ps*} A^? ->{ps*} A^?
+   |          Required: ((A ->{ps*} A, A ->{ps*} A)) -> A^? ->? A^?
+   |          Note that capability ps* is not included in capture set {}.
    |
    | longer explanation available when compiling with `-explain`

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

@@ -1,16 +1,16 @@
 -- Error: tests/neg-custom-args/captures/sep-box.scala:41:9 ------------------------------------------------------------
 41 |  par(h1.value, h2.value) // error
    |      ^^^^^^^^
-   |Separation failure: argument of type  Ref^{h1.value*}
+   |Separation failure: argument of type  Ref^{xs*}
    |to method par: (x: Ref^, y: Ref^): Unit
    |corresponds to capture-polymorphic formal parameter x of type  Ref^
-   |and hides capabilities  {h1.value*}.
-   |Some of these overlap with the captures of the second argument with type  Ref^{h2.value*}.
+   |and hides capabilities  {xs*}.
+   |Some of these overlap with the captures of the second argument with type  Ref^{xs*}.
    |
-   |  Hidden set of current argument        : {h1.value*}
-   |  Hidden footprint of current argument  : {h1.value*, xs*}
-   |  Capture set of second argument        : {h2.value*}
-   |  Footprint set of second argument      : {h2.value*, xs*}
+   |  Hidden set of current argument        : {xs*}
+   |  Hidden footprint of current argument  : {xs*}
+   |  Capture set of second argument        : {xs*}
+   |  Footprint set of second argument      : {xs*}
    |  The two sets overlap at               : {xs*}
    |
    |where:    ^ refers to a fresh root capability classified as Mutable created in method test when checking argument to parameter x of method par