Interaction between separation checking and pattern matching

[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)
def test1(a: Cell[Int]^): Unit =
  swap(a, a)  // error
  val b = a
  swap(a, b)  // error
  a match
    case a0: Cell[Int]^ =>
      swap(a, a0)  // should be error, but ok

Output

Two errors are emitted but the last line passed.

Expectation

The last line should be an error, since a and a0 are really aliases.

[Linyxus]

I looked at the cc tree:

    def test1(a: Cell[Int]^): Unit =
      matchResult1[Unit]:
        {
          case val x1: (a : Cell[Int]^) = a
          if x1.$isInstanceOf[Cell[Int]^] then
            {
              case val a0: Cell[Int]^ = x1.$asInstanceOf[Cell[Int]^]
              return[matchResult1]
                {
                  swap[Int](a, a0)
                }
            }
           else ()
          throw new MatchError(x1)
        }

I think the cause is the $asInstanceOf inserted by pattern matching, which blindly widens x1 to Cell[Int]^ and bypasses the hidden set computation.

[noti0na1]

We need #21828