Unsound application of boxed functions

[Linyxus]

Compiler version

3.1.3-RC4

Minimized code

class Unit
object unit extends Unit

type Top = {*} Any

type LazyVal[T] = {*} Unit -> T

case class Foo[T](x: T)

// Foo[□ {*} Unit -> T]
type BoxedLazyVal[T] = Foo[LazyVal[T]]

def force[A](v: BoxedLazyVal[A]): A =
  // Γ ⊢ v.x : □ {*} Unit -> A
  v.x(unit)  // (unbox v.x)(unit), where (unbox v.x) should be untypable

Output

The code compiles but it shouldn't.

[[syntax trees at end of                        cc]] // issues/unbox-minimised.scala
package <empty> {
  @CaptureChecked @SourceFile("issues/unbox-minimised.scala") class Unit() extends Object() {}
  final lazy module val unit: unit = new unit()
  @CaptureChecked @SourceFile("issues/unbox-minimised.scala") final module class unit() extends Unit() {
    private[this] type $this = unit.type
    private def writeReplace(): AnyRef = new scala.runtime.ModuleSerializationProxy(classOf[unit.type])
  }
  @CaptureChecked @SourceFile("issues/unbox-minimised.scala") case class Foo[T](x: T) extends Object(), Product, Serializable {
    override def hashCode(): Int = scala.runtime.ScalaRunTime._hashCode(this)
    override def equals(x$0: Any): Boolean = 
      this.eq(x$0.$asInstanceOf[Object]).||(
        matchResult1[Boolean]: 
          {
            case val x1: (x$0 : Any) = x$0
            if x1.$isInstanceOf[Foo[T] @unchecked] then 
              {
                case val x$0: Foo[T] = x1.$asInstanceOf[Foo[T] @unchecked]
                return[matchResult1] this.x.==(x$0.x).&&(x$0.canEqual(this))
              }
             else ()
            return[matchResult1] false
          }
      )
    override def toString(): String = scala.runtime.ScalaRunTime._toString(this)
    override def canEqual(that: Any): Boolean = that.isInstanceOf[Foo[T] @unchecked]
    override def productArity: Int = 1
    override def productPrefix: String = "Foo"
    override def productElement(n: Int): Any = 
      matchResult2[T]: 
        {
          case val x3: (n : Int) = n
          if 0.==(x3) then return[matchResult2] this._1 else ()
          throw new IndexOutOfBoundsException(n.toString())
        }
    override def productElementName(n: Int): String = 
      matchResult3[("x" : String)]: 
        {
          case val x4: (n : Int) = n
          if 0.==(x4) then return[matchResult3] "x" else ()
          throw new IndexOutOfBoundsException(n.toString())
        }
    T
    val x: T
    def copy[T](x: T): Foo[T] = new Foo[T](x)
    def copy$default$1[T]: T = Foo.this.x
    def _1: T = this.x
  }
  final lazy module val Foo: Foo = new Foo()
  @CaptureChecked @SourceFile("issues/unbox-minimised.scala") final module class Foo() extends AnyRef(), scala.deriving.Mirror.Product {
    private[this] type $this = Foo.type
    private def writeReplace(): AnyRef = new scala.runtime.ModuleSerializationProxy(classOf[Foo.type])
    def apply[T](x: T): Foo[T] = new Foo[T](x)
    def unapply[T](x$1: Foo[T]): Foo[T] = x$1
    override def toString: String = "Foo"
    type MirroredMonoType = Foo[? <: AnyKind]
    def fromProduct(x$0: Product): Foo.MirroredMonoType = new Foo[Any](x$0.productElement(0))
  }
  final lazy module val unbox-minimised$package: unbox-minimised$package = new unbox-minimised$package()
  @CaptureChecked @SourceFile("issues/unbox-minimised.scala") final module class unbox-minimised$package() extends Object() {
    private[this] type $this = unbox-minimised$package.type
    private def writeReplace(): AnyRef = new scala.runtime.ModuleSerializationProxy(classOf[unbox-minimised$package.type])
    type Top = {*} Any
    type LazyVal = [T] =>> {*} Unit -> T
    type BoxedLazyVal = [T] =>> Foo[{*} Unit -> T]
    def force[A](v: BoxedLazyVal[A]): A = v.x.apply(unit)
    def main(): Unit = 
      {
        abstract class Cap() extends Object() {
          def close(): Unit = unit
        }
        def withCap[T](op: ({*} Cap) => T): T = 
          {
            val cap: ? Cap = 
              {
                final class $anon() extends Cap() {}
                new Cap {...}():(? Cap)
              }
            val result: ? T = op.apply(cap)
            cap.close()
            result:({result} T)
          }
        def leaked: {} BoxedLazyVal[Cap] = 
          withCap[? Foo[{*} (x$0: ? Unit) -> ? Cap]](
            {
              {
                def $anonfun(cap: {*} Cap): ? Foo[{cap, *} (x$0: ? Unit) -> ? Cap] = 
                  {
                    val bad: {cap} (x$0: {} Unit) -> {cap} Cap = 
                      {
                        def $anonfun(_$1: Unit): {cap} Cap = cap
                        closure($anonfun)
                      }
                    Foo.apply[{bad, cap, *} (x$0: ? Unit) -> {cap} Cap](bad)
                  }
                closure($anonfun)
              }
            }
          )
        val leakedCap: {} Cap = force[? Cap](leaked)
        ()
      }
  }
}

-- Warning: issues/unbox-minimised.scala:1:6 -------------------------------------------------------------------------------------------------------------------------------------
1 |class Unit
  |      ^
  |      class Unit differs only in case from object unit. Such classes will overwrite one another on case-insensitive filesystems.
1 warning found
[success] Total time: 2 s, completed Jul 26, 2022, 4:25:25 PM

Expectation

This code is minimised from Ondrej's list encoding example (in #15731). In force, the function v.x is a boxed function of type □ {*} Unit -> A, so we should not allow the application v.x(unit) since we can not unbox it.

This leads to the leaking of scoped capabilities, for example:

def main() = {
  abstract class Cap { def close(): Unit = unit }
  def withCap[T](op: ({*} Cap) => T): T = {
    val cap = new Cap {}
    val result = op(cap)
    cap.close()
    result
  }

  def leaked: {} BoxedLazyVal[Cap] = withCap { cap =>
    val bad = (_: Unit) => cap
    Foo(bad)
  }

  val leakedCap: {} Cap = force(leaked)
}

[odersky]

There's something wrong with the isBoxedCapturing predicate. What happens is that the new selection rule for v.x kicks
in which says that since v has a pure type and the type of x as a member of v is unboxed, the result is also pure. The second part is wrong; the type of x should be boxed.

Before it was not a problem since we did not apply this reasoning to selections, so the type of v.x was simply {*} Unit -> Int.

[Linyxus]

Ah, so this simplified snippet reveals a problem different from the original one in #15731 (since the list in that example is church-encoded and no selection is involved).

[Linyxus]

I tweaked the snippet a bit (defining the wrapper in church-style) and found this (which is closer to the original list encoding example and seems to reveal the same problem):

class Unit
object unit extends Unit

type Top = {*} Any

type Wrapper[T] = [X] -> (op: T => X) -> X

def wrapper[T](x: T) = [X] => (op: T => X) => op(x)

def strictMap[A <: Top, B <: Top](mx: Wrapper[A])(f: A => B): Wrapper[B] =
  mx((x: A) => wrapper(f(x)))

def force[A](thunk: Unit => A): A = thunk(unit)

def forceWrapper[A](mx: Wrapper[Unit => A]): Wrapper[A] =
  // Γ ⊢ mx: Wrapper[□ {*} Unit => A]
  // `force` should be typed as ∀(□ {*} Unit -> A) A, but it can not
  strictMap[{*} Unit -> A, A](mx)(force)

I am unfamiliar with how capture checker works yet, but it seems that when supplying force to strictMap we should try to type force as a function receiving boxed values, and maybe throw an error here. Is this a known issue? (I remembered it was mentioned that the boxing logic for functions is not finished yet).

[odersky]

@Linyxus Where do you think this latest example should issue an error?

[Linyxus]

Maybe we should issue an error when applying strictMap[{*} Unit -> A, A](mx) on force (on the last line). The partially-applied function strictMap[{*} Unit -> A, A](mx) expects an argument of type (□ {*} Unit -> A) => A, but force has the type ({*} Unit -> A) => A.

[odersky]

@Linyxus Yes, I think that makes sense.