Expressiveness problem with capture checking paths

[odersky]

Compiler version

3.7.0RC1

Minimized example

import language.experimental.captureChecking
import caps.*

case class A()

trait HasCap:
  def mkA: A^{this}

object HasCap:
  def apply[T](body: HasCap^ ?=> T): T = ???

class Box(using h: HasCap^):
  var t: A^{h} = h.mkA

def main() =
  HasCap: h1 ?=>
    val b = Box(using h1)
    b.t = h1.mkA

Output

-- [E007] Type Mismatch Error: classcaps.scala:19:13 ---------------------------
19 |    b.t = h1.mkA
   |          ^^^^^^
   |          Found:    A^{h1}
   |          Required: A^{b.h}
   |
   | longer explanation available when compiling with `-explain`
[[syntax trees at end of                        cc]] // classcaps.scala

Expectation

It would be nice if there was no error. If we look at the generated code we find:

    def main(): Unit =
      HasCap.apply[Unit]((using h1: HasCap^) =>
        {
          val b: Box{val h: HasCap^{h1}}^{h1} = new Box(using h1)()
          b.t = h1.mkA
        }
      )

The problem here is that b.h <:< {h1} but we do not know that b.h == h1. We used to imply this, but it was unsound in general. /cc @noti0na1

[odersky]

I verified that the example compiles correctly if Box is modified to use a tracked parameter. This compiles:

import language.experimental.captureChecking
import language.experimental.modularity      // <<< need language import
import caps.*

case class A()

trait HasCap:
  def mkA: A^{this}

object HasCap:
  def apply[T](body: HasCap^ ?=> T): T = ???

class Box(using tracked val h: HasCap^):  // <<< need tracked parameter
  var t: A^{h} = h.mkA

def main() =
  HasCap: h1 ?=>
    val b = Box(using h1)
    b.t = h1.mkA

Maybe that workaround is good enough?

[noti0na1]

The code is similar to the test we had: tests/neg-custom-args/captures/filevar-multi-ios.scala

I think a tracked is required in this case to explicitly show h1 =:= b.h

[natsukagami]

tracked doesn't work if we instead mention a capture set member of HasCap:

//> using scala 3.7.0-RC1-bin-SNAPSHOT

import language.experimental.captureChecking
import language.experimental.modularity
import caps.*

case class A()

trait HasCap:
  type Cap >: CapSet <: CapSet^
  def mkA: A^{Cap^}

object HasCap:
  def apply[T](body: HasCap^ => T): T = ???

class Box(tracked val h: HasCap^):
  var t: A^{h.Cap^} = h.mkA

def main() =
  HasCap: h =>
    val b = Box(h)
    b.t = h.mkA // Found A^{h.Cap^}, Required: A^{b.h².Cap^}

[noti0na1]

b.t = h.mkA // Found A^{h.Cap^}, Required: A^{b.h².Cap^}

Given h =:= b.h, we should use sub typing itself to check h.Cap <:< b.h.Cap.