Tighten subsumption checking of Fresh instances

Fresh instances cannot subsume TermParamRefs since that would be a level
violation.

Author: odersky

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

@@ -256,7 +256,11 @@ trait CaptureRef extends TypeProxy, ValueType:
     || this.match
       case root.Fresh(hidden) =>
         vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
-        || !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
+        || !y.stripReadOnly.isCap
+            && !yIsExistential
+            && !y.isInstanceOf[TermParamRef]
+            && canAddHidden
+            && vs.addHidden(hidden, y)
       case x @ root.Result(binder) =>
         val result = y match
           case y @ root.Result(_) => vs.unify(x, y)

tests/neg-custom-args/captures/capt-test.scala

@@ -20,7 +20,7 @@ def handle[E <: Exception,  R <: Top](op: (CT[E] @retains(caps.cap)) => R)(handl
   catch case ex: E => handler(ex)
 
 def test: Unit =
-  val b = handle[Exception, () => Nothing] { // error
+  val b = handle[Exception, () => Nothing] { // error // error
     (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
   } {
     (ex: Exception) => ???

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

@@ -7,4 +7,4 @@ class Foo:
 def Test: Unit =
   val f = new Foo
   f.withSession(s => s).request // error
-  f.withSession[Session^](t => t) // error
+  f.withSession[Session^](t => t) // error // error

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

@@ -0,0 +1,19 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:13:4 ----------------------------------------
+13 |    (ref1, f1) => map[A, B](ref1, f1) // error
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |    Found:    (ref1: LazyRef[box A^?]{val elem: () ->{cap, fresh} A^?}^{io}, f1: (x$0: A^?) => B^?) ->?
+   |      LazyRef[box B^?]{val elem: () ->{localcap} B^?}^{f1, ref1}
+   |    Required: (ref1: LazyRef[A]^{io}, f1: A => B) ->{fresh} LazyRef[B]^{fresh}
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ----------------------------------------
+15 |    (ref1, f1) => map[A, B](ref1, f1) // error
+   |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |    Found:    (ref1: LazyRef[box A^?]{val elem: () ->{cap, fresh} A^?}^{io}, f1: (x$0: A^?) => B^?) ->?
+   |      LazyRef[box B^?]{val elem: () ->{localcap} B^?}^{f1, ref1}
+   |    Required: (ref: LazyRef[A]^{io}, f: A => B) ->{fresh} LazyRef[B]^{localcap}
+   |
+   |    Note that the existential capture root in LazyRef[B]^
+   |    cannot subsume the capability f1.type since that capability is not a SharedCapability
+   |
+   | longer explanation available when compiling with `-explain`

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

@@ -0,0 +1,16 @@
+class Cap extends caps.Capability
+
+class LazyRef[T](val elem: () => T):
+  val get: () ->{elem} T = elem
+  def map[U](f: T => U): LazyRef[U]^{f, this} =
+    new LazyRef(() => f(elem()))
+
+def map[A, B](ref: LazyRef[A]^, f: A => B): LazyRef[B]^{f, ref} =
+  new LazyRef(() => f(ref.elem()))
+
+def main(io: Cap) = {
+  def mapc[A, B]: (LazyRef[A]^{io}, A => B) => LazyRef[B]^ =
+    (ref1, f1) => map[A, B](ref1, f1) // error
+  def mapd[A, B]: (ref: LazyRef[A]^{io}, f: A => B) => LazyRef[B]^ =
+    (ref1, f1) => map[A, B](ref1, f1) // error
+}

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

@@ -4,10 +4,17 @@
    |              Type variable T of object Boxed cannot be instantiated to box IO^ since
    |              that type captures the root capability `cap`.
 -- Error: tests/neg-custom-args/captures/i21401.scala:15:18 ------------------------------------------------------------
-15 |  val a = usingIO[IO^](x => x) // error
+15 |  val a = usingIO[IO^](x => x) // error // error
    |                  ^^^
    |                  Type variable R of method usingIO cannot be instantiated to box IO^ since
    |                  that type captures the root capability `cap`.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:15:23 ---------------------------------------
+15 |  val a = usingIO[IO^](x => x) // error // error
+   |                       ^^^^^^
+   |                       Found:    (x: IO^) ->? box IO^{x}
+   |                       Required: (x: IO^) ->{fresh} box IO^{fresh}
+   |
+   | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------
 16 |  val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
    |                                                                  ^^^

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

@@ -12,7 +12,7 @@ def mkRes(x: IO^): Res =
     val op1: Boxed[IO^] -> R = op
     op1(Boxed[IO^](x)) // error
 def test2() =
-  val a = usingIO[IO^](x => x) // error
+  val a = usingIO[IO^](x => x) // error // error
   val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
   val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
   val y: IO^{x*} = x.unbox // was error

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

@@ -44,6 +44,13 @@
    |                                                   ^
    |                                Type variable A of constructor Id cannot be instantiated to box () => Unit since
    |                                that type captures the root capability `cap`.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:59:27 --------------------------------------
+59 |  val id: File^ -> File^ = x => x // error
+   |                           ^^^^^^
+   |                           Found:    (x: File^) ->? File^{x}
+   |                           Required: (x: File^) -> File^{fresh}
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:38 --------------------------------------
 62 |  val leaked = usingFile[File^{id*}]: f => // error // error
    |                                      ^

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

@@ -56,7 +56,7 @@ def test =
     id(() => f.write()) // was error
 
 def attack2 =
-  val id: File^ -> File^ = x => x
+  val id: File^ -> File^ = x => x // error
     // val id: File^ -> File^{fresh}
 
   val leaked = usingFile[File^{id*}]: f => // error // error

tests/neg-custom-args/captures/refine-reach-shallow.scala

@@ -1,7 +1,7 @@
 import language.experimental.captureChecking
 trait IO
 def test1(): Unit =
-  val f: IO^ => IO^ = x => x
+  val f: IO^ => IO^ = x => x // error
   val g: IO^ => IO^{f*} = f  // error
 def test2(): Unit =
   val f: [R] -> (IO^ => R) -> R = ???