Modify Var rule to plug unsoundness hole

Author: odersky

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

@@ -233,28 +233,34 @@ extension (tp: Type)
     assert(tp.isTrackableRef)
     TermRef(tp, nme.CC_REACH, defn.Any_ccReach)
 
-  /** If `ref` is a trackable capture ref, replace all covariant occurrences of a
-   *  universal capture set in `tp` by `{ref*}`. This implements the new aspect of
-   *  the (Var) rule, which can now be stated as follows:
+  /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
+   *  universal capture set, replace all these occurrences by `{ref*}`. This implements
+   *  the new aspect of the (Var) rule, which can now be stated as follows:
    *
    *     x: T in E
    *     -----------
    *     E |- x: T'
    *
    *  where T' is T with (1) the toplevel capture set replaced by `{x}` and
-   *  (2) all covariant occurrences of cap replaced by `x*`. (1) is standard,
-   *  whereas (2) is new.
+   *  (2) all covariant occurrences of cap replaced by `x*`, provided there
+   *  are no occurrences in `T` at other variances. (1) is standard, whereas
+   *  (2) is new.
    *
    *  Why is this sound? Covariant occurrences of cap must represent capabilities
    *  that are reachable from `x`, so they are included in the meaning of `{x*}`.
    *  At the same time, encapsulation is still maintained since no covariant
    *  occurrences of cap are allowed in instance types of type variables.
    */
   def withReachCaptures(ref: Type)(using Context): Type =
-    val narrowCaps = new TypeMap:
+    object narrowCaps extends TypeMap:
+      var ok = true
       def apply(t: Type) = t.dealias match
-        case t1 @ CapturingType(p, cs) if cs.isUniversal && variance > 0 =>
-          t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
+        case t1 @ CapturingType(p, cs) if cs.isUniversal =>
+          if variance > 0 then
+            t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
+          else
+            ok = false
+            t
         case _ => t match
           case t @ CapturingType(p, cs) =>
             t.derivedCapturingType(apply(p), cs) // don't map capture set variables
@@ -263,8 +269,12 @@ extension (tp: Type)
     ref match
       case ref: CaptureRef if ref.isTrackableRef =>
         val tp1 = narrowCaps(tp)
-        if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
-        tp1
+        if narrowCaps.ok then
+          if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
+          tp1
+        else
+          capt.println(i"cannot narrow $tp of $ref to $tp1")
+          tp
       case _ =>
         tp
 

docs/_docs/internals/cc/alternatives-to-sealed.md

@@ -19,7 +19,8 @@ A capture checking variant
         E |- x: T'
 
    where T' is T with (1) the toplevel capture set replaced by `{x}` and
-   (2) all covariant occurrences of cap replaced by `x*`. (1) is standard,
+   (2) all covariant occurrences of cap replaced by `x*`, provided there
+   are no occurrences in `T` at other variances. (1) is standard,
    whereas (2) is new.
 
 - Why is this sound? Covariant occurrences of cap must represent capabilities that are reachable from `x`, so they are included in the meaning of `{x*}`. At the same time, encapsulation is still maintained since no covariant occurrences of cap are allowed in instance types of

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

@@ -1,12 +1,12 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:22:11 --------------------------------------
-22 |    cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:21:11 --------------------------------------
+21 |    cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
    |           ^^^^^^^^^^^^^^^^^^^^^^^
    |           Found:    List[box () ->{f} Unit]
    |           Required: List[box () ->{xs*} Unit]
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:33:7 ---------------------------------------
-33 |      (() => f.write()) :: Nil // error since {f*} !<: {xs*}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:32:7 ---------------------------------------
+32 |      (() => f.write()) :: Nil // error since {f*} !<: {xs*}
    |       ^^^^^^^^^^^^^^^^^^^^^^^
    |       Found:    List[box () ->{f} Unit]
    |       Required: box List[box () ->{xs*} Unit]^?
@@ -15,22 +15,29 @@
    |       cannot be included in outer capture set {xs*} of value cur which is associated with method runAll1
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:36:6 ------------------------------------------------------------
-36 |  var cur: List[Proc] = xs // error: Illegal type for var
+-- Error: tests/neg-custom-args/captures/reaches.scala:35:6 ------------------------------------------------------------
+35 |  var cur: List[Proc] = xs // error: Illegal type for var
    |      ^
    |      Mutable variable cur cannot have type List[box () => Unit] since
    |      the part box () => Unit of that type captures the root capability `cap`.
--- Error: tests/neg-custom-args/captures/reaches.scala:43:15 -----------------------------------------------------------
-43 |  val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
+-- Error: tests/neg-custom-args/captures/reaches.scala:42:15 -----------------------------------------------------------
+42 |  val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
    |            ^^^^^^^^^^^^^^^
    |            Sealed type variable T cannot be instantiated to List[box () => Unit] since
    |            the part box () => Unit of that type captures the root capability `cap`.
    |            This is often caused by a local capability in an argument of constructor Ref
    |            leaking as part of its result.
--- Error: tests/neg-custom-args/captures/reaches.scala:53:31 -----------------------------------------------------------
-53 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
+-- Error: tests/neg-custom-args/captures/reaches.scala:52:31 -----------------------------------------------------------
+52 |  val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
    |                               ^^^^^^^^^^^^^^^^^^^^
    |                               Sealed type variable A cannot be instantiated to box () => Unit since
    |                               that type captures the root capability `cap`.
    |                               This is often caused by a local capability in an argument of constructor Id
    |                               leaking as part of its result.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:60:27 --------------------------------------
+60 |    val f1: File^{id*} = id(f) // error
+   |                         ^^^^^
+   |                         Found:    File^{id, f}
+   |                         Required: File^{id*}
+   |
+   | longer explanation available when compiling with `-explain`

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

@@ -17,7 +17,6 @@ def runAll0(xs: List[Proc]): Unit =
     next()
     cur = cur.tail: List[() ->{xs*} Unit]
 
-
   usingFile: f =>
     cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
 
@@ -52,4 +51,11 @@ class Id[sealed -A, sealed +B >: A]():
 def test =
   val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
   usingFile: f =>
-    id(() => f.write())  // escape, if it was not for the error above
+    id(() => f.write())  // escape, if it was not for the error above
+
+def attack2 =
+  val id: File^ -> File^ = x => x
+
+  val leaked = usingFile[File^{id*}]: f =>
+    val f1: File^{id*} = id(f) // error
+    f1