Skip to content

Commit 113b08a

Browse files
committed
Avoid using Ranges in exact substitutions
This improves the completeness of capture checking in the following case: ```scala def run(io: IO^)(op: Op^{io}): Unit = ??? val myIO: IO^ = ??? val myOp: Op^{myIO} = ??? run(myIO)(myOp) ``` The last line previously won't work because when substitute the parameter `io` to `myIO` in the type `(op: Op^{io}): Unit` the type `Op^{io}` get approximated into `Nothing` contravariantly. This is an overshot since the substitution [io := myIO] is exact (or precise) and the approximation (or avoidance) is unnecessary. This commit resolves this issue by checking whether the `to` only contains `CaptureRef` in `SubstParamsMap`. If this condition is met, then it is an exact substitution and we can apply it on the capture set without approximations.
1 parent 51d69e8 commit 113b08a

File tree

2 files changed

+50
-10
lines changed

2 files changed

+50
-10
lines changed

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

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -72,16 +72,23 @@ object CheckCaptures:
7272
*/
7373
final class SubstParamsMap(from: BindingType, to: List[Type])(using Context)
7474
extends ApproximatingTypeMap, IdempotentCaptRefMap:
75-
def apply(tp: Type): Type = tp match
76-
case tp: ParamRef =>
77-
if tp.binder == from then to(tp.paramNum) else tp
78-
case tp: NamedType =>
79-
if tp.prefix `eq` NoPrefix then tp
80-
else tp.derivedSelect(apply(tp.prefix))
81-
case _: ThisType =>
82-
tp
83-
case _ =>
84-
mapOver(tp)
75+
/** This SubstParamsMap is exact if `to` only contains `CaptureRef`s. */
76+
private val isExactSubstitution: Boolean = to.forall(_.isInstanceOf[CaptureRef])
77+
78+
/** As long as this substitution is exact, there is no need to create `Range`s when mapping invariant positions. */
79+
override protected def needsRangeIfInvariant(refs: CaptureSet): Boolean = !isExactSubstitution
80+
81+
def apply(tp: Type): Type =
82+
tp match
83+
case tp: ParamRef =>
84+
if tp.binder == from then to(tp.paramNum) else tp
85+
case tp: NamedType =>
86+
if tp.prefix `eq` NoPrefix then tp
87+
else tp.derivedSelect(apply(tp.prefix))
88+
case _: ThisType =>
89+
tp
90+
case _ =>
91+
mapOver(tp)
8592

8693
/** Check that a @retains annotation only mentions references that can be tracked.
8794
* This check is performed at Typer.
Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
import language.experimental.captureChecking
2+
import caps.*
3+
4+
trait Ref[T] { def set(x: T): T }
5+
def test() = {
6+
7+
def swap[T](x: Ref[T]^)(y: Ref[T]^{x}): Unit = ???
8+
def foo[T](x: Ref[T]^): Unit =
9+
swap(x)(x)
10+
11+
def bar[T](x: () => Ref[T]^)(y: Ref[T]^{x}): Unit =
12+
swap(x())(y) // error
13+
14+
def baz[T](x: Ref[T]^)(y: Ref[T]^{x}): Unit =
15+
swap(x)(y)
16+
}
17+
18+
trait IO
19+
type Op = () -> Unit
20+
def test2(c: IO^, f: Op^{c}) = {
21+
def run(io: IO^)(op: Op^{io}): Unit = op()
22+
run(c)(f)
23+
24+
def bad(getIO: () => IO^, g: Op^{getIO}): Unit =
25+
run(getIO())(g) // error
26+
}
27+
28+
def test3() = {
29+
def run(io: IO^)(op: Op^{io}): Unit = ???
30+
val myIO: IO^ = ???
31+
val myOp: Op^{myIO} = ???
32+
run(myIO)(myOp)
33+
}

0 commit comments

Comments
 (0)