Scoped capabilities can leak through path-dependent types

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking

trait Logger
def usingLogger[T](op: Logger^ => T): T = ???

trait Foo:
  type T >: () => Logger^

class Bar extends Foo:
  type T = () => Logger^

def foo(x: Foo): x.T =
  val leaked = usingLogger[x.T]: l =>
    val t: () => Logger^ = () => l
    t: x.T
  leaked

def test(): Unit =
  val bar = new Bar
  val bad: bar.T = foo(bar)
  val leaked: Logger^ = bad()  // leaked scoped capability!

Output

It compiles.

Expectation

It should not compile.

Essentially, the above example is equivalent to the following code but the following uses type parameters instead of path-dependent types:

def foo[X >: () => Logger^](): X =
  val leaked = usingLogger[X]: l =>
    val t: () => Logger^ = () => l
    t: X
  leaked
val bad = foo[() => Logger^]()  // error

But this code is rejected as wanted, as we perform the no-root-capability check for the type application foo[() => Logger^].
Given that path-dependent types is, in some sense, equivalent to type parameters, a similar check should be performed for foo(bar) in the unsound code example.
But that one is currently missing.

Alternatively, instead of checking the type members on the callsite, we could do that check when instantiating a type member. In this case, that would be when defining the class Bar.