Type arguments of capability classes not properly boxed in CC Setup

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
import caps.*
trait Cap
class Inv[T] extends Capability
class Inv2[T]
class Inv3[T] extends Mutable
def test(c: Cap^): Unit =
  val t1: Inv[() ->{c} Unit] = Inv()  // error
  val t2: Inv2[() ->{c} Unit] = Inv2()  // ok
  val t3: Inv3[() ->{c} Unit] = Inv3()   // error, too

Output

-- [E007] Type Mismatch Error: issues/cc-boxed-types.scala:8:34 ------------------------------------------------------------------------------------------------------------------------
8 |  val t1: Inv[() ->{c} Unit] = Inv()  // error
  |                               ^^^^^
  |                               Found:    (Inv^{cap.rd})[box () ->? Unit]^{cap².rd}
  |                               Required: Inv[() ->{c} Unit]^{cap³.rd}
  |
  |                               where:    cap  is a fresh root capability created in value t1 when instantiating constructor Inv's type (): (Inv^{cap⁴.rd})[box () ->? Unit]
  |                                         cap² is a fresh root capability created in value t1 when constructing Capability instance (Inv^{cap⁴.rd})[box () ->? Unit]
  |                                         cap³ is a fresh root capability in the type of value t1
  |
  | longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: issues/cc-boxed-types.scala:10:36 -----------------------------------------------------------------------------------------------------------------------
10 |  val t3: Inv3[() ->{c} Unit] = Inv3()   // error, too
   |                                ^^^^^^
   |                           Found:    (Inv3^{cap.rd}.reader)[box () ->? Unit]^{cap².rd}.reader
   |                           Required: Inv3[() ->{c} Unit]^{cap³.rd}.reader
   |
   |                           where:    cap  is a fresh root capability created in value t3 when instantiating constructor Inv3's type (): (Inv3^{cap⁴.rd}.reader)[box () ->? Unit]
   |                                     cap² is a fresh root capability created in value t3 when constructing mutable (Inv3^{cap⁴.rd}.reader)[box () ->? Unit]
   |                                     cap³ is a fresh root capability in the type of value t3
   |
   | longer explanation available when compiling with `-explain`
[[syntax trees at end of                        cc]] // issues/cc-boxed-types.scala
package <empty> {
  import language.experimental.captureChecking
  import caps.*
  @SourceFile("issues/cc-boxed-types.scala") trait Cap() extends Object {}
  @SourceFile("issues/cc-boxed-types.scala") class Inv[T]() extends Object(), (scala.caps.Capability^{<fresh in class Inv hiding ?>.rd}) {
    T
  }
  @SourceFile("issues/cc-boxed-types.scala") class Inv2[T]() extends Object() {
    T
  }
  @SourceFile("issues/cc-boxed-types.scala") class Inv3[T]() extends Object(), (scala.caps.Mutable^{<fresh in class Inv3 hiding ?>.rd}.reader) {
    T
  }
  final lazy module val cc-boxed-types$package: cc-boxed-types$package = new cc-boxed-types$package()
  @SourceFile("issues/cc-boxed-types.scala") final module class cc-boxed-types$package() extends Object() {
    private[this] type $this = cc-boxed-types$package.type
    private def writeReplace(): AnyRef = new scala.runtime.ModuleSerializationProxy(classOf[cc-boxed-types$package.type])2 errors found

    def test(c: Cap^{<fresh in method test hiding {c}?>}): Unit =
      {
        val t1: Inv[() ->{c} Unit]^{<fresh in val t1 hiding ?>.rd} = new Inv[box () ->? Unit]()
        val t2: Inv2[box () ->{c} Unit] = new Inv2[box () ->{c}? Unit]()
        val t3: Inv3[() ->{c} Unit]^{<fresh in val t3 hiding ?>.rd}.reader = new Inv3[box () ->? Unit]()
        ()
      }
  }
}

Expectation

There should be no error. From the outputed tree we can see that only t2's type arguments are properly boxed, but not t1 and t3. The type mismatch is due to the mismatch between boxing status.