Plug soundness hole for reach capabilities

To prevent that a reach capability is undermined by passing in a local capability from the outside,
we disallow function arguments where reach capabilities appear in contravariant or invariant positions.

Author: odersky

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

@@ -453,6 +453,31 @@ class CheckCaptures extends Recheck, SymTransformer:
           case appType => appType
     end recheckApply
 
+    // Uses 4-space indent as a trial
+    override def recheckArg(arg: Tree, pt: Type)(using Context) =
+        val argType = recheck(arg, pt)
+
+        def checkOnlyCovariantReachCaps = new TypeTraverser:
+            def traverse(tp: Type) =
+                tp match
+                case CapturingType(parent, refs) =>
+                    traverse(parent)
+                    if variance <= 0 then
+                        for ref <- refs.elems do
+                            if ref.isReach then
+                                val prefix = if variance == 0 then "in" else "contra"
+                                report.error(
+                                    em"""Reach capability ${ctx.printer.toTextCaptureRef(ref).show} is not allowed to appear in ${prefix}variant position
+                                        |in argument type ${argType.widen}""",
+                                    arg.srcPos
+                                )
+                case _ =>
+                    traverseChildren(tp)
+
+        checkOnlyCovariantReachCaps.traverse(argType.widen)
+        argType
+    end recheckArg
+
     private def isDistinct(xs: List[Type]): Boolean = xs match
       case x :: xs1 => xs1.isEmpty || !xs1.contains(x) && isDistinct(xs1)
       case Nil => true

compiler/src/dotty/tools/dotc/transform/Recheck.scala

@@ -311,7 +311,7 @@ abstract class Recheck extends Phase, SymTransformer:
             else fntpe.paramInfos
           def recheckArgs(args: List[Tree], formals: List[Type], prefs: List[ParamRef]): List[Type] = args match
             case arg :: args1 =>
-              val argType = recheck(arg, normalizeByName(formals.head))
+              val argType = recheckArg(arg, normalizeByName(formals.head))
               val formals1 =
                 if fntpe.isParamDependent
                 then formals.tail.map(_.substParam(prefs.head, argType))
@@ -326,6 +326,9 @@ abstract class Recheck extends Phase, SymTransformer:
         case tp =>
           assert(false, i"unexpected type of ${tree.fun}: $tp")
 
+    def recheckArg(arg: Tree, pt: Type)(using Context): Type =
+      recheck(arg, normalizeByName(pt))
+
     def recheckTypeApply(tree: TypeApply, pt: Type)(using Context): Type =
       val funtpe = recheck(tree.fun)
       tree.fun.rememberType(funtpe) // remember type to support later bounds checks

tests/neg-custom-args/captures/i15749a.scala

@@ -19,4 +19,4 @@ def test =
   def forceWrapper[A](mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
     // Γ ⊢ mx: Wrapper[□ {cap} Unit => A]
     // `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not
-    strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // should work
+    strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // error

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

@@ -41,3 +41,8 @@
    |                         Required: File^{id*}
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/reaches.scala:67:10 -----------------------------------------------------------
+67 |  ps.map((x, y) => compose(x, y)) // error
+   |          ^^^^^^^^^^^^^^^^^^^^^^
+   |Reach capability ps* is not allowed to appear in contravariant position
+   |in argument type (x$1: (box (x$0: A^?) ->{ps*} A^?, box (x$0: A^?) ->{ps*} A^?)^?) ->? box (x$0: A^?) ->{ps*} A^?

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

@@ -59,3 +59,11 @@ def attack2 =
   val leaked = usingFile[File^{id*}]: f =>
     val f1: File^{id*} = id(f) // error
     f1
+
+def compose[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
+  z => g(f(z))
+
+def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
+  ps.map((x, y) => compose(x, y)) // error
+    // unfortunately this does not work. x and y have type A ->{ps*} A, and that
+    // type is not allowed to appear contra-variantly in the argument

tests/neg-custom-args/captures/refine-withFile.scala

@@ -5,4 +5,4 @@ val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
 def main(): Unit =
   val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
   val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f  // error
-  val leaked = g[File^{f*}]("test")(f => f)  // boom
+  val leaked = g[File^{f*}]("test")(f => f)  // error

tests/neg/unsound-reach-2.scala

@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+trait Consumer[-T]:
+  def apply(x: T): Unit
+
+trait File:
+  def close(): Unit
+
+def withFile[R](path: String)(op: Consumer[File]): R = ???
+
+trait Foo[+X]:
+  def use(x: File^)(op: Consumer[X]): Unit
+class Bar extends Foo[File^]:
+  def use(x: File^)(op: Consumer[File^]): Unit = op.apply(x)
+
+def bad(): Unit =
+  val backdoor: Foo[File^] = new Bar
+  val boom: Foo[File^{backdoor*}] = backdoor
+
+  var escaped: File^{backdoor*} = null
+  withFile("hello.txt"): f =>
+    boom.use(f):
+      new Consumer[File^{backdoor*}]: // error
+        def apply(f1: File^{backdoor*}) =
+          escaped = f1
+

tests/neg/unsound-reach.check

@@ -0,0 +1,6 @@
+-- Error: tests/neg/unsound-reach.scala:18:17 --------------------------------------------------------------------------
+18 |    boom.use(f): (f1: File^{backdoor*}) => // error
+   |                 ^
+   |                 Reach capability backdoor* is not allowed to appear in contravariant position
+   |                 in argument type (f1: box File^{backdoor*}) ->? Unit
+19 |      escaped = f1

tests/neg/unsound-reach.scala

@@ -0,0 +1,20 @@
+import language.experimental.captureChecking
+trait File:
+  def close(): Unit
+
+def withFile[R](path: String)(op: File^ => R): R = ???
+
+trait Foo[+X]:
+  def use(x: File^)(op: X => Unit): Unit
+class Bar extends Foo[File^]:
+  def use(x: File^)(op: File^ => Unit): Unit = op(x)
+
+def bad(): Unit =
+  val backdoor: Foo[File^] = new Bar
+  val boom: Foo[File^{backdoor*}] = backdoor
+
+  var escaped: File^{backdoor*} = null
+  withFile("hello.txt"): f =>
+    boom.use(f): (f1: File^{backdoor*}) => // error
+      escaped = f1
+

tests/pos-custom-args/captures/reaches.scala

@@ -35,9 +35,6 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
 def compose2[A, B, C](f: A => B, g: B => C): A => C =
   z => g(f(z))
 
-def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
-  ps.map((x, y) => compose1(x, y))
-
 @annotation.capability class IO
 
 def test(io: IO) =