Switch version where separation checking starts to 3.8

odersky · odersky · commit 0b9acb39e470 · 2025-01-21T22:08:08.000+01:00
3.7 is already on us, so bump by one.

Two new tests for separation checking. One i15749a required a change in SepCheck:
We need to be able to declare reach capabilities in dependencies. The reach is
imply dropped. But we can't sometimes use a normal capability since its capture
set might be empty.
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -256,7 +256,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       (formal, arg) <- mt.paramInfos.zip(args)
       dep <- formal.captureSet.elems.toList
     do
-      val referred = dep match
+      val referred = dep.stripReach match
         case dep: TermParamRef =>
           argMap(dep.binder)(dep.paramNum) :: Nil
         case dep: ThisType if dep.cls == fn.symbol.owner =>
diff --git a/project/Build.scala b/project/Build.scala
@@ -1223,7 +1223,7 @@ object Build {
     settings(scala2LibraryBootstrappedSettings).
     settings(
       moduleName := "scala2-library-cc",
-      scalacOptions ++= Seq("-Ycheck:all", "-source", "3.7")
+      scalacOptions ++= Seq("-Ycheck:all", "-source", "3.8")
     )
 
   lazy val scala2LibraryBootstrappedSettings = Seq(
diff --git a/tests/neg-custom-args/captures/box-adapt-cases.scala b/tests/neg-custom-args/captures/box-adapt-cases.scala
@@ -1,4 +1,4 @@
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 trait Cap { def use(): Int }
 
 def test1(): Unit = {
diff --git a/tests/neg-custom-args/captures/depfun-reach.scala b/tests/neg-custom-args/captures/depfun-reach.scala
@@ -1,6 +1,6 @@
 import language.experimental.captureChecking
 import caps.cap
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 def test(io: Object^, async: Object^) =
   def compose(op: List[(() ->{cap} Unit, () ->{cap} Unit)]): List[() ->{op*} Unit] =
     List(() => op.foreach((f,g) => { f(); g() }))
diff --git a/tests/neg-custom-args/captures/existential-mapping.scala b/tests/neg-custom-args/captures/existential-mapping.scala
@@ -1,5 +1,5 @@
 import language.experimental.captureChecking
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 class A
 class C
 type Fun[X] = (x: C^) -> X
diff --git a/tests/neg-custom-args/captures/i19330.scala b/tests/neg-custom-args/captures/i19330.scala
@@ -1,4 +1,4 @@
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 import language.experimental.captureChecking
 
 
diff --git a/tests/neg-custom-args/captures/i21614.scala b/tests/neg-custom-args/captures/i21614.scala
@@ -1,7 +1,7 @@
 import language.experimental.captureChecking
 import caps.Capability
 import caps.use
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 trait List[+T]:
   def map[U](f: T => U): List[U]
 
diff --git a/tests/neg-custom-args/captures/lazyref.scala b/tests/neg-custom-args/captures/lazyref.scala
@@ -1,4 +1,4 @@
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 class CC
 type Cap = CC^
 
diff --git a/tests/neg-custom-args/captures/outer-var.scala b/tests/neg-custom-args/captures/outer-var.scala
@@ -1,4 +1,4 @@
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 class CC
 type Cap = CC^
 
diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala
@@ -1,4 +1,4 @@
-import caps.use; import language.`3.7` // sepchecks on
+import caps.use; import language.`3.8` // sepchecks on
 class File:
   def write(): Unit = ???
 
diff --git a/tests/neg-custom-args/captures/reaches2.check b/tests/neg-custom-args/captures/reaches2.check
@@ -1,10 +1,25 @@
--- Error: tests/neg-custom-args/captures/reaches2.scala:8:10 -----------------------------------------------------------
-8 |  ps.map((x, y) => compose1(x, y)) // error // error
-  |          ^
-  |reference ps* is not included in the allowed capture set {}
-  |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
--- Error: tests/neg-custom-args/captures/reaches2.scala:8:13 -----------------------------------------------------------
-8 |  ps.map((x, y) => compose1(x, y)) // error // error
-  |             ^
-  |reference ps* is not included in the allowed capture set {}
-  |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
+-- Error: tests/neg-custom-args/captures/reaches2.scala:10:10 ----------------------------------------------------------
+10 |  ps.map((x, y) => compose1(x, y)) // error // error // error
+   |          ^
+   |reference ps* is not included in the allowed capture set {}
+   |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
+-- Error: tests/neg-custom-args/captures/reaches2.scala:10:13 ----------------------------------------------------------
+10 |  ps.map((x, y) => compose1(x, y)) // error // error // error
+   |             ^
+   |reference ps* is not included in the allowed capture set {}
+   |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
+-- Error: tests/neg-custom-args/captures/reaches2.scala:10:31 ----------------------------------------------------------
+10 |  ps.map((x, y) => compose1(x, y)) // error // error // error
+   |                               ^
+   |                               Separation failure: argument of type  (x$0: A) ->{y} box A^?
+   |                               to method compose1: [A, B, C](f: A => B, g: B => C): A ->{f, g} C
+   |                               corresponds to capture-polymorphic formal parameter g of type  box A^? => box A^?
+   |                               and captures {ps*}, but this capability is also passed separately
+   |                               in the first argument with type  (x$0: A) ->{x} box A^?.
+   |
+   |                                 Capture set of first argument         : {x}
+   |                                 Hidden set of current argument        : {y}
+   |                                 Footprint of first argument           : {x, ps*}
+   |                                 Hidden footprint of current argument  : {y, ps*}
+   |                                 Declared footprint of current argument: {}
+   |                                 Undeclared overlap of footprints      : {ps*}
diff --git a/tests/neg-custom-args/captures/reaches2.scala b/tests/neg-custom-args/captures/reaches2.scala
@@ -1,9 +1,11 @@
+import language.`3.8` // sepchecks on
+
 class List[+A]:
   def map[B](f: A -> B): List[B] = ???
 
 def compose1[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) => compose1(x, y)) // error // error
+  ps.map((x, y) => compose1(x, y)) // error // error // error
 
diff --git a/tests/neg-custom-args/captures/unsound-reach-2.scala b/tests/neg-custom-args/captures/unsound-reach-2.scala
@@ -1,4 +1,4 @@
-import language.experimental.captureChecking; import language.`3.7` // sepchecks on
+import language.experimental.captureChecking; import language.`3.8` // sepchecks on
 trait Consumer[-T]:
   def apply(x: T): Unit
 
diff --git a/tests/neg-custom-args/captures/unsound-reach-3.scala b/tests/neg-custom-args/captures/unsound-reach-3.scala
@@ -1,6 +1,6 @@
 
 
-import language.experimental.captureChecking; import language.`3.7` // sepchecks on
+import language.experimental.captureChecking; import language.`3.8` // sepchecks on
 trait File:
   def close(): Unit
 
diff --git a/tests/neg-custom-args/captures/unsound-reach-4.scala b/tests/neg-custom-args/captures/unsound-reach-4.scala
@@ -1,6 +1,6 @@
 
 
-import language.experimental.captureChecking; import language.`3.7` // sepchecks on
+import language.experimental.captureChecking; import language.`3.8` // sepchecks on
 trait File:
   def close(): Unit
 
diff --git a/tests/neg-custom-args/captures/vars.scala b/tests/neg-custom-args/captures/vars.scala
@@ -1,4 +1,4 @@
-import language.`3.7` // sepchecks on
+import language.`3.8` // sepchecks on
 
 class CC
 type Cap = CC^
diff --git a/tests/pos-custom-args/captures/i15749a.scala b/tests/pos-custom-args/captures/i15749a.scala
@@ -1,5 +1,6 @@
 import caps.cap
 import caps.use
+import language.`3.8` // sepchecks on
 
 class Unit
 object u extends Unit
@@ -13,7 +14,7 @@ def test =
   def wrapper[T](x: T): Wrapper[T] = Wrapper:
     [X] => (op: T ->{cap} X) => op(x)
 
-  def strictMap[A <: Top,  B <: Top](mx: Wrapper[A])(f: A ->{cap} B): Wrapper[B] =
+  def strictMap[A <: Top,  B <: Top](mx: Wrapper[A])(f: A ->{cap, mx*} B): Wrapper[B] =
     mx.value((x: A) => wrapper(f(x)))
 
   def force[A](thunk: Unit ->{cap} A): A = thunk(u)

Original file line number	Diff line number	Diff line change
`@@ -1223,7 +1223,7 @@ object Build {`
`1223`	`1223`	`settings(scala2LibraryBootstrappedSettings).`
`1224`	`1224`	`settings(`
`1225`	`1225`	`moduleName := "scala2-library-cc",`
`1226`		`- scalacOptions ++= Seq("-Ycheck:all", "-source", "3.7")`
	`1226`	`+ scalacOptions ++= Seq("-Ycheck:all", "-source", "3.8")`
`1227`	`1227`	`)`
`1228`	`1228`
`1229`	`1229`	`lazy val scala2LibraryBootstrappedSettings = Seq(`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		-import language.`3.7` // sepchecks on
	`1`	+import language.`3.8` // sepchecks on
`2`	`2`	`trait Cap { def use(): Int }`
`3`	`3`
`4`	`4`	`def test1(): Unit = {`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		-import caps.use; import language.`3.7` // sepchecks on
	`1`	+import caps.use; import language.`3.8` // sepchecks on
`2`	`2`	`class File:`
`3`	`3`	`def write(): Unit = ???`
`4`	`4`