Several separation checker issues

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
case class Box[+T](unbox: T)
class Ref extends Mutable:
  private var _data: Int = 0
  update def set(x: Int): Unit = _data = x
  def get: Int = _data
def swap(a: Ref^, b: Ref^): Unit = ()
def test1(): Unit =
  val a = Ref()
  val bad: (x: Ref^) -> List[() ->{a,x} Unit] =
    x => List(() => swap(a, x))
  bad(a).head()  // should be error, but ok // boom at runtime

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
case class Box[+T](unbox: T)
class Ref extends Mutable:
  private var _data: Int = 0
  update def set(x: Int): Unit = _data = x
  def get: Int = _data
def swap(a: Ref^, b: Ref^): Unit = ()
def test1(): Unit =
  val a = Ref()
  val b = Ref()
  val ok: (x: Ref^) -> (y: Ref^{x}) ->{x} Unit = x => y => ()
  ok(a)   // should be ok, but error

Output

The first compiles but the second issues an error.

Expectation

The first should be an error while the second should succeed.

These all originate from one problematic piece of the current separation checker. I am working on a fix and this is to track the issues.