Missing expressiveness when combining scoped and fresh capabilities

[odersky]

Compiler version

3.8.0

Minimized example

import language.experimental.captureChecking
import caps.*

class Ref[T](init: T) extends Mutable:
  var x = init
  def get: T = x
  update def put(y: T): Unit = x = y

class File:
  def read(): String = ???

def withFile[T](op: (f: File^) => T): T =
  op(new File)

def Test =
  withFile: f =>
    Ref(f.read()) // error

Output

-- [E007] Type Mismatch Error: ref-with-file.scala:15:12 -----------------------
15 |  withFile: f =>
   |            ^
   |Capability cap outlives its scope: it leaks into outer capture set 's1 which is owned by method Test.
   |The leakage occurred when trying to match the following types:
   |
   |Found:    (f: File^'s2) ->'s3 Ref[String]^
   |Required: (f: File^²) => Ref[String]^'s1
   |
   |where:    =>  refers to a fresh root capability created in method Test when checking argument to parameter op of method withFile
   |          ^   refers to a root capability associated with the result type of (f: File^'s2): Ref[String]^
   |          ^²  refers to the universal root capability
   |          cap is a root capability associated with the result type of (f: File^²): T
16 |    Ref(f.read())
   |
   | longer explanation available when compiling with `-explain`

Expectation

It would be nice if this could work.

One idea is to use a new classifier Unscoped and declare Ref to extend it. Then level checking could be turned off for FreshCap instances of this classifier.

Are there other ideas how we could make the example compile?