Fixes for pattern matching under separation checking

[odersky]

1. Convert _i case selectors to the original case accessors. This gives more precise typing and avoids an unsoundness because _i accessor functions return pure results.
2. Systematically propagate consume parameters into synthesized parts of case classes.
3. Special capture check rule for case class unapply.

Based on #26569

With the changes there and in this PR we can now define recursive generic data structures of fresh elements and use these date structures in a natural way, including using pattern matching.

• Each addition to these data structures consumes the added element.
• Each decomposition returns fresh values and consumes the original argument.

[bracevac]

Can we find a representation that permits consume tails and a unique Nil object?

Without a fresh tail, it's fairly easy to subvert the system:

def Test0 =
    val r1 = Ref()
    val r2 = Ref()
    val r3 = Ref()
    val xs0 = FreshNil
    val xs1 = FreshCons(r1, xs0)
    val xs2 = FreshCons(r2, xs1)
    val xs3 = FreshCons(r3, xs1)
    val r1_2 = xs2.tail.decons.head
    val r1_3 = xs3.tail.decons.head
    par(r1_2, r1_3) // oops

[Linyxus]

this looks like a soundness bug if accepted. xs3.tail.decons should be allowed since it uses a consumed thing.

[bracevac]

The question is what do we expect from decons?

Right now it's

consume def decons: FreshCons[A]^ = this

Since the tail isn't marked consume I read it as
"sharing of tails is allowed".

We probably need a "deep" consume? Looking at the inferred capture sets:

val xs2: FreshCons[Ref^{}]{val tail: FreshList[Ref^{}]^{}}^{} =
          FreshCons.apply[Ref^'s2](r2, xs1)

All those lists are pure, but shouldn't we make FreshList trackable? Then I could see how decons also affects the tails.

But then we have the problem that a singleton Nil list can't be supported? I'd imagine the superclass FreshList should be an ExclusiveCapability.

[Linyxus]

A minimization of the snippet posted by Oliver, which is clearly a soundness bug (double-consume):

def Test0 =
    val r1 = Ref()
    val xs0 = FreshNil
    val xs1 = FreshCons(r1, xs0)
    val ys1 = xs1.decons // ok
    val ys2 = xs1.decons // should be error, but still ok

[Linyxus]

This crashes the compiler:

import language.experimental.separationChecking
import caps.*
class Ref extends Mutable:
  var x = 0
  def get: Int = x
  update def put(y: Int): Unit = x = y
trait FreshList[+A]
case class FreshCons[+A](val head: A^, val tail: FreshList[A]^) extends FreshList[A]
def Test1(xs1: FreshList[Ref^{}]^) =
  val ys = xs1 match
    case FreshCons(h, t) => FreshCons(h, t)

[odersky]

The problem is in the type produced by FreshCons (which is a bug). If you ascribe the type explicitly, the double decons is an error:

def Test0 =
    val r1: Ref^ = Ref()
    val xs0 = FreshNil
    val xs1: FreshCons[Ref^{}]^ = FreshCons(r1, xs0)
    val ys1 = xs1.decons // ok
    val ys2 = xs1.decons // error
    par(ys1, ys2)

[odersky]

The crash is gone now as well.

[Linyxus]

another soundness issue:

import language.experimental.separationChecking
import caps.*
class Ref extends Mutable:
  var x = 0
  def get: Int = x
  update def put(y: Int): Unit = x = y
  consume def dealloc(): Unit = ()
case class FreshRef(consume val a: Ref^):
  a.dealloc()  // should be error, but ok
def boom(consume x: FreshRef^): Unit =
  x match
    case FreshRef(core) => core.dealloc()  // boom! double-free