Widen unsafe reach capabilities instead of erroring

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

@@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
 import transform.{Recheck, PreRecheck, CapturedVars}
 import Recheck.*
 import scala.collection.mutable
-import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
+import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult, universal}
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.trace
@@ -254,39 +254,50 @@ class CheckCaptures extends Recheck, SymTransformer:
     def showRef(ref: CaptureRef)(using Context): String =
         ctx.printer.toTextCaptureRef(ref).show
 
-    // Uses 4-space indent as a trial
-    def checkReachCapsIsolated(tpe: Type, pos: SrcPos)(using Context): Unit =
-
-        object checker extends TypeTraverser:
-            var refVariances: Map[Boolean, Int] = Map.empty
-            var seenReach: CaptureRef | Null = null
-            def traverse(tp: Type) =
-                tp.dealias match
-                case CapturingType(parent, refs) =>
-                    traverse(parent)
-                    for ref <- refs.elems do
-                        if ref.isReach && !ref.stripReach.isInstanceOf[TermParamRef]
-                            || ref.isRootCapability
-                        then
-                            val isReach = ref.isReach
-                            def register() =
-                                refVariances = refVariances.updated(isReach, variance)
-                                seenReach = ref
-                            refVariances.get(isReach) match
-                                case None => register()
-                                case Some(v) => if v != 0 && variance == 0 then register()
-                case _ =>
-                    traverseChildren(tp)
+    enum ReachCapsStatus:
+      /** Everything good. No covariant reach caps or reach caps
+        * without the presence of contravariant universal caps. */
+      case Safe
+      /** Covariant reach caps and contravariant root caps co-exist.
+        * But all reach caps occurrences are covariant.
+        * In this case we could undo reach refinement by widening reach caps. */
+      case UnsafeAllCov(reach: CaptureRef)
+      /** Same as the previous case except that invariant occurrence of reach caps exists.
+        * In this case undoing reach refinement is impossible. */
+      case Unsafe(reach: CaptureRef)
+
+    def checkReachCapsIsolated(tpe: Type)(using Context): ReachCapsStatus =
+      object checker extends TypeTraverser:
+        var reachVariance: Int = -1
+        var seenInvReach: Boolean = false
+        var capVariance: Int = 1
+        var seenReach: CaptureRef | Null = null
+        def traverse(tp: Type) =
+          tp.dealias match
+            case CapturingType(parent, refs) =>
+              traverse(parent)
+              for ref <- refs.elems do
+                if ref.isReach && !ref.stripReach.isInstanceOf[TermParamRef]
+                  || ref.isRootCapability
+                then
+                  val isReach = ref.isReach
+                  if isReach then
+                    reachVariance = variance.max(reachVariance)
+                    if variance >= 0 then
+                      seenReach = ref
+                    if variance == 0 then
+                      seenInvReach = true
+                  else
+                    capVariance = variance.min(capVariance)
+            case _ =>
+              traverseChildren(tp)
 
-        checker.traverse(tpe)
-        if checker.refVariances.size == 2
-            && checker.refVariances(true) >= 0
-            && checker.refVariances(false) <= 0
-        then
-            report.error(
-                em"""Reach capability ${showRef(checker.seenReach.nn)} and universal capability cap cannot both
-                    |appear in the type $tpe of this expression""",
-                pos)
+      checker.traverse(tpe)
+      if checker.reachVariance >= 0 && checker.capVariance <= 0 then
+        if checker.seenInvReach then ReachCapsStatus.Unsafe(checker.seenReach.nn)
+        else ReachCapsStatus.UnsafeAllCov(checker.seenReach.nn)
+      else
+        ReachCapsStatus.Safe
     end checkReachCapsIsolated
 
     /** The current environment */
@@ -839,7 +850,6 @@ class CheckCaptures extends Recheck, SymTransformer:
           tree.tpe
         finally curEnv = saved
       if tree.isTerm then
-        checkReachCapsIsolated(res.widen, tree.srcPos)
         if !pt.isBoxedCapturing then
           markFree(res.boxedCaptureSet, tree.srcPos)
       res
@@ -877,6 +887,12 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     private inline val debugSuccesses = false
 
+    private def widenReachCaps(using Context): TypeMap = new TypeMap with IdempotentCaptRefMap:
+      def apply(tp: Type): Type = tp match
+        case CapturingType(parent, refs) if refs.elems.exists(_.isReach) =>
+          tp.derivedCapturingType(mapOver(parent), universal)
+        case _ => mapOver(tp)
+
     /** 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
@@ -886,7 +902,22 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
       var expected1 = alignDependentFunction(expected, actual.stripCapturing)
-      val actualBoxed = adapt(actual, expected1, tree.srcPos)
+
+      var actual1 = actual
+      var reachWiden: CaptureRef | Null = null
+      checkReachCapsIsolated(actual.widen) match
+        case ReachCapsStatus.Safe =>
+        case ReachCapsStatus.UnsafeAllCov(reach) =>
+          actual1 = widenReachCaps(actual.widen)
+          //println(i"WIDEN $actual --> $actual1")
+          reachWiden = reach
+        case ReachCapsStatus.Unsafe(reach) =>
+          report.error(
+              em"""Reach capability ${showRef(reach)} and universal capability cap cannot both
+                  |appear in the type $actual of this expression""",
+              tree.srcPos)
+
+      val actualBoxed = adapt(actual1, expected1, tree.srcPos)
       //println(i"check conforms $actualBoxed <<< $expected1")
 
       if actualBoxed eq actual then
@@ -900,8 +931,21 @@ class CheckCaptures extends Recheck, SymTransformer:
         actualBoxed
       else
         capt.println(i"conforms failed for ${tree}: $actual vs $expected")
-        err.typeMismatch(tree.withType(actualBoxed), expected1, addenda ++ CaptureSet.levelErrors)
-        actual
+
+        def reachWidenErrors: Addenda = new Addenda:
+          override def toAdd(using Context) =
+            reachWiden match
+              case null => Nil
+              case reach: CaptureRef => List(
+                i"""
+                  |
+                  |Note that the reach capability ${showRef(reach)} and universal capability cap cannot both
+                  |appear in the type $actual of this expression.
+                  |The reach capability therefore needs to be widen to cap."""
+              )
+
+        err.typeMismatch(tree.withType(actualBoxed), expected1, addenda ++ CaptureSet.levelErrors ++ reachWidenErrors)
+        actual1
     end checkConformsExpr
 
     /** Turn `expected` into a dependent function when `actual` is dependent. */

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

@@ -41,8 +41,13 @@
    |                         Required: File^{id*}
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:77:5 ------------------------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:77:8 ---------------------------------------
 77 |  ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and *
-   |  ^^^^^^
-   |  Reach capability cap and universal capability cap cannot both
-   |  appear in the type [B](f: ((box A ->{ps*} A, box A ->{ps*} A)) => B): List[B] of this expression
+   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  Found:    List[box (x$0: A^?) ->{x$1*, x$1²*} A^?]
+   |  Required: List[box A ->{ps*} A]
+   |
+   |  where:    x$1  is a reference to a value parameter
+   |            x$1² is a reference to a value parameter
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/widen-reach.check

@@ -0,0 +1,11 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 ----------------------------------
+14 |  val y3: IO^ -> IO^{x*} = y1.foo  // error
+   |                           ^^^^^^
+   |                           Found:    IO^ ->? IO^
+   |                           Required: IO^ -> IO^{x*}
+   |
+   |                           Note that the reach capability x* and universal capability cap cannot both
+   |                           appear in the type (y1.foo : IO^ -> box IO^{x*}) of this expression.
+   |                           The reach capability therefore needs to be widen to cap.
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/widen-reach.scala

@@ -0,0 +1,14 @@
+import language.experimental.captureChecking
+
+trait IO
+
+trait Foo[+T]:
+  val foo: IO^ -> T
+
+trait Bar extends Foo[IO^]:
+  val foo: IO^ -> IO^ = x => x
+
+def test(x: Foo[IO^]): Unit =
+  val y1: Foo[IO^{x*}] = x
+  val y2: IO^ -> IO^ = y1.foo
+  val y3: IO^ -> IO^{x*} = y1.foo  // error

tests/neg/unsound-reach-2.scala

@@ -18,7 +18,7 @@ def bad(): Unit =
 
   var escaped: File^{backdoor*} = null
   withFile("hello.txt"): f =>
-    boom.use(f): // error
+    boom.use(f):
       new Consumer[File^{backdoor*}]: // error
         def apply(f1: File^{backdoor*}) =
           escaped = f1

tests/neg/unsound-reach-4.check

@@ -1,5 +1,7 @@
--- Error: tests/neg/unsound-reach-4.scala:20:19 ------------------------------------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg/unsound-reach-4.scala:20:22 ---------------------------------------------------
 20 |    escaped = boom.use(f)  // error
-   |              ^^^^^^^^
-   |              Reach capability backdoor* and universal capability cap cannot both
-   |              appear in the type (x: F): box File^{backdoor*} of this expression
+   |              ^^^^^^^^^^^
+   |              Found:    File^{f}
+   |              Required: File^{backdoor*}
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg/unsound-reach.check

@@ -1,5 +1,8 @@
--- Error: tests/neg/unsound-reach.scala:18:13 --------------------------------------------------------------------------
-18 |        boom.use(f): (f1: File^{backdoor*}) => // error
-   |        ^^^^^^^^
-   |        Reach capability backdoor* and universal capability cap cannot both
-   |        appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression
+-- [E007] Type Mismatch Error: tests/neg/unsound-reach.scala:18:17 -----------------------------------------------------
+18 |    boom.use(f): (f1: File^{backdoor*}) => // error
+   |                 ^
+   |                 Found:    (f1: box File^{backdoor*}) ->? Unit
+   |                 Required: (f1: box File^) => Unit
+19 |      escaped = f1
+   |
+   | longer explanation available when compiling with `-explain`