From 113b08acb7ee1460519d6c4fab5d0e6a156a0810 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 18 May 2023 02:19:57 +0200
Subject: [PATCH] Avoid using `Range`s 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.
---
 .../dotty/tools/dotc/cc/CheckCaptures.scala   | 27 +++++++++------
 .../captures/cc-subst-param-exact.scala       | 33 +++++++++++++++++++
 2 files changed, 50 insertions(+), 10 deletions(-)
 create mode 100644 tests/neg-custom-args/captures/cc-subst-param-exact.scala

diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
index 6ec360eca938..5ecd29119e3a 100644
--- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
+++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -72,16 +72,23 @@ object CheckCaptures:
    */
   final class SubstParamsMap(from: BindingType, to: List[Type])(using Context)
   extends ApproximatingTypeMap, IdempotentCaptRefMap:
-    def apply(tp: Type): Type = tp match
-      case tp: ParamRef =>
-        if tp.binder == from then to(tp.paramNum) else tp
-      case tp: NamedType =>
-        if tp.prefix `eq` NoPrefix then tp
-        else tp.derivedSelect(apply(tp.prefix))
-      case _: ThisType =>
-        tp
-      case _ =>
-        mapOver(tp)
+    /** This SubstParamsMap is exact if `to` only contains `CaptureRef`s. */
+    private val isExactSubstitution: Boolean = to.forall(_.isInstanceOf[CaptureRef])
+
+    /** As long as this substitution is exact, there is no need to create `Range`s when mapping invariant positions. */
+    override protected def needsRangeIfInvariant(refs: CaptureSet): Boolean = !isExactSubstitution
+
+    def apply(tp: Type): Type =
+      tp match
+        case tp: ParamRef =>
+          if tp.binder == from then to(tp.paramNum) else tp
+        case tp: NamedType =>
+          if tp.prefix `eq` NoPrefix then tp
+          else tp.derivedSelect(apply(tp.prefix))
+        case _: ThisType =>
+          tp
+        case _ =>
+          mapOver(tp)
 
   /** Check that a @retains annotation only mentions references that can be tracked.
    *  This check is performed at Typer.
diff --git a/tests/neg-custom-args/captures/cc-subst-param-exact.scala b/tests/neg-custom-args/captures/cc-subst-param-exact.scala
new file mode 100644
index 000000000000..35e4acb95fdc
--- /dev/null
+++ b/tests/neg-custom-args/captures/cc-subst-param-exact.scala
@@ -0,0 +1,33 @@
+import language.experimental.captureChecking
+import caps.*
+
+trait Ref[T] { def set(x: T): T }
+def test() = {
+
+  def swap[T](x: Ref[T]^)(y: Ref[T]^{x}): Unit = ???
+  def foo[T](x: Ref[T]^): Unit =
+    swap(x)(x)
+
+  def bar[T](x: () => Ref[T]^)(y: Ref[T]^{x}): Unit =
+    swap(x())(y)  // error
+
+  def baz[T](x: Ref[T]^)(y: Ref[T]^{x}): Unit =
+    swap(x)(y)
+}
+
+trait IO
+type Op = () -> Unit
+def test2(c: IO^, f: Op^{c}) = {
+  def run(io: IO^)(op: Op^{io}): Unit = op()
+  run(c)(f)
+
+  def bad(getIO: () => IO^, g: Op^{getIO}): Unit =
+    run(getIO())(g)  // error
+}
+
+def test3() = {
+  def run(io: IO^)(op: Op^{io}): Unit = ???
+  val myIO: IO^ = ???
+  val myOp: Op^{myIO} = ???
+  run(myIO)(myOp)
+}