Separation checking treats `p` and `p.fst` as separate

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
import caps.*
class Cell[T](init: T) extends Mutable:
  private var _data: T = init
  def get: T = _data
  mut def set(x: T) = _data = x
def swap[T](a: Cell[T]^, b: Cell[T]^): Unit =
  val t: T = a.get
  a.set(b.get)
  b.set(t)

case class Pair(fst: Cell[Int]^, snd: Cell[Int]^)
def test1(p: Pair^): Unit =
  val t1: Cell[Int]^{p} = p.fst
  val t2: Cell[Int]^{p.fst} = p.fst
  swap(t1, t2)   // should be error, but ok

Output

No error.

Expectation

The last line should be an error, since {p} and {p.fst} overlaps.

[Linyxus]

Another manifest of this issue:

import language.experimental.captureChecking
import caps.*
class Cell[T](init: T) extends Mutable:
  private var _data: T = init
  def get: T = _data
  mut def set(x: T) = _data = x
case class P(fst: Cell[Int]^, snd: Cell[Int]^)
def bye[T](@consume x: Cell[T]^): Unit = ()
def byeP(@consume p: P^): Unit = ()
def test(@consume p: P^): Unit =
  byeP(p)
  bye(p.fst)  // should be error

I think this two examples are correlated.