CC unsoundness: TypeComparer.glb strips capture set

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
trait Cap
trait Foo[+T]

def magic[T](io: Cap^, x: Foo[T]^{io}): Foo[T]^{} =
  val x1: Foo[T]^{cap} & Foo[Any]^{io} = x
  val x2: Foo[T] = x1
  x2  // boom, an impure value becomes pure

Output

It compiles.

Expectation

It should be rejected.

Problematic glb trace:

==> glb(Foo[T]^, Foo[Any]^{io})?
  ==> glb(Foo[T], Foo[Any]^{io})?
    ==> glb(Foo[T], <notype>)?
    <== glb(Foo[T], <notype>) = Foo[T]
  <== glb(Foo[T], Foo[Any]^{io}) = Foo[T]
<== glb(Foo[T]^, Foo[Any]^{io}) = Foo[T]

Possible code location that causes this issue: https://github.com/lampepfl/dotty/blob/da16f434fa3aa74bcceacb04243f742a61f8b786/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L2603-L2609

[Linyxus]

I attempted a fix in #18254. When working on the fix I was reasoning about the "glb" of two capture sets. Notably, unlike types (in DOT) which possess both glb (intersections) and lub (unions), capture sets have lubs (which are simply the set unions) but not always a glb. I believe this could lead to some interesting problems to be studied when developing the formalization combining DOT and CC. Besides, such a formalization enables us to have a more principled and solid understanding of these problems as well.