diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index e41f32cab672..1a19b374a225 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/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. */ diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index a1c5a56369e9..4e7d8067c3cd 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/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` diff --git a/tests/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check new file mode 100644 index 000000000000..009fe6ebe402 --- /dev/null +++ b/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` diff --git a/tests/neg-custom-args/captures/widen-reach.scala b/tests/neg-custom-args/captures/widen-reach.scala new file mode 100644 index 000000000000..5fa05687b1dc --- /dev/null +++ b/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 diff --git a/tests/neg/unsound-reach-2.scala b/tests/neg/unsound-reach-2.scala index 083cec6ee5b2..f25e89e18eac 100644 --- a/tests/neg/unsound-reach-2.scala +++ b/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 diff --git a/tests/neg/unsound-reach-4.check b/tests/neg/unsound-reach-4.check index 47256baf408a..ec3b7ab4ea54 100644 --- a/tests/neg/unsound-reach-4.check +++ b/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` diff --git a/tests/neg/unsound-reach.check b/tests/neg/unsound-reach.check index 8cabbe1571a0..f613fa6bf6a5 100644 --- a/tests/neg/unsound-reach.check +++ b/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` diff --git a/tests/neg-custom-args/captures/i15749a.scala b/tests/pos-custom-args/captures/i15749a.scala similarity index 100% rename from tests/neg-custom-args/captures/i15749a.scala rename to tests/pos-custom-args/captures/i15749a.scala