Separation checking for product types

[odersky]

This is based on #22588 and contains changes to make product types containing fresh entities work (at least in simple cases). There's a neat combination with both path capabilities and reach capabilities which makes this work.

In short, if we have

class Ref { var current: Int }
case class Pair[+A, +B](fst: A, snd: B)

then we can form a Pair[Ref^, Ref^]:

val r1 = Ref()
val r2 = Ref()
val p_exact: Pair[Ref^{r1}, Ref^{r2}] = Pair(r1, r2)
val p:  Pair[Ref^, Ref^] = p_exact

And if p has this type, then we can also take it apart:

val x = p.fst
val y = p.snd

With types added, this is

val x: Ref^{p.fst*} = p.fst
val y: Ref^{p.snd*} = p.snd

That is, we can get at the position of the boxed first element with p.fst and we can access what's in the box via p.fst*.
Furthermore, p.fst* is known to be separate from p.snd*, so this means we can form another pair from them:

val p2: Pair[Ref^, Ref^] = Pair(x, y)

In short, separation is preserved by forming products and taking them apart. It took quite a bit of work to get there.

[hamzaremmal]

@odersky CI will fail because of the timeouts here too. Revert seems the fastest solution to unblock this situation.

[odersky]

This is built on top of #22588. So CI failures due to timeout are the same.

[Linyxus]

Some fresh soundness holes!

import language.experimental.captureChecking
import caps.*

class Ref[T](init: T) extends Mutable:
  private var value: T = init
  def get: T = value
  mut def set(newValue: T): Unit = value = newValue

// a library function that assumes that a and b MUST BE separate
def swap[T](a: Ref[Int]^, b: Ref[Int]^): Unit = ???

def test1(): Unit =
  val a: Ref[Int]^ = Ref(0)
  val foo: (x: Ref[Int]^) -> (y: Ref[Int]^{a}) ->{x} Unit =
    x => y => swap(x, y)
  foo(a)(a)  // OH NO

def test2(): Unit =
  val a: Ref[Int]^ = Ref(0)
  val f: (Ref[Int]^, Ref[Int]^) -> Unit = swap
  val g: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit = f
  g(a, a)  // OH NO

[Linyxus]

One more unsound snippet:

import language.experimental.captureChecking
import caps.*

class Ref[T](init: T) extends Mutable:
  private var value: T = init
  def get: T = value
  mut def set(newValue: T): Unit = value = newValue

// a library function that assumes that a and b MUST BE separate
def swap(a: Ref[Int]^, b: Ref[Int]^): Unit = ???

case class Foo[T](bar: Ref[T]^)

def foo(x: Foo[Int]^): Unit =
  val t1: Ref[Int]^{x.bar} = x.bar
  swap(t1, t1)  // no error, OH NO

  // sanity check
  val t2: Ref[Int]^ = Ref(0)
  val t3: Ref[Int]^{t2} = t2
  swap(t3, t3)  // error, as expected

[odersky]

@Linyxus The first hole is plugged now.

[Linyxus]

One soundness issue related to @consume:

import language.experimental.captureChecking
import caps.*

class Ref extends Mutable:
  private var _data = 0
  def get: Int = _data
  mut def put(x: Int): Unit = _data = x

// require f and g to be non-interfering
def par(f: () => Unit, g: () => Unit): Unit = ???

def bad(@consume op: () ->{cap.rd} Unit): () => Unit = op

def test2(@consume x: Ref^): Unit =
  val f: () ->{x.rd} Unit = () => x.get
  val rx: () => Unit = bad(f)  // hides x.rd in the resulting `cap`
  par(rx, () => x.put(42))  // data race!

This compiles but should not. And it has data races.
I was expecting @consume has some sort of "killing" effect. For instance, the function call on the last but two line bad(f) hides x.rd in a consume parameter. This should disable x.rd (and therefore x) afterwards when the function call finishes.

[odersky]

Second soundness hold related to contravariant cap is now also fixed

[odersky]

Soundness issue related to @consume is fixed now.