Test case showing that second soundness hole is filled

Author: odersky

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

@@ -19,8 +19,6 @@ import annotation.internal.sharable
 
 object root:
 
-  @sharable private var rootId = 0
-
   enum Kind:
     case Result(binder: MethodType)
     case Fresh(hidden: CaptureSet.HiddenSet)
@@ -35,6 +33,8 @@ object root:
         case _ => false
   end Kind
 
+  @sharable private var rootId = 0
+
   /** The annotation of a root instance */
   case class Annot(kind: Kind) extends Annotation:
 

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

@@ -0,0 +1,7 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/contracap.scala:15:48 ------------------------------------
+15 |  val g: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit = f // error
+   |                                                ^
+   |                                                Found:    (f : (Ref[Int]^, Ref[Int]^) -> Unit)
+   |                                                Required: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit
+   |
+   | longer explanation available when compiling with `-explain`

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

@@ -0,0 +1,16 @@
+import language.experimental.captureChecking
+import caps.*
+
+class Ref[T](init: T) extends Mutable:
+  private var value: T = init
+  def get: T = value
+  mut def set(newValue: T): Unit = value = newValue
+
+// a library function that assumes that a and b MUST BE separate
+def swap[T](a: Ref[Int]^, b: Ref[Int]^): Unit = ???
+
+def test2(): Unit =
+  val a: Ref[Int]^ = Ref(0)
+  val f: (Ref[Int]^, Ref[Int]^) -> Unit = swap
+  val g: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit = f // error
+  g(a, a)  // OH NO