Skip to content

Leaking local reach capability #21442

Closed
@Linyxus

Description

@Linyxus

Compiler version

main

Minimized code

import language.experimental.captureChecking
trait IO:
  def use(): Unit
case class Boxed[+T](unbox: T)

// `foo` is a function that unboxes its parameter
// and uses the capability boxed inside the parameter.
def foo(x: Boxed[IO^]): Unit =
  x.unbox.use()  // error: local reach capability {x*} leaks

// `bar` is a function that does the same thing in a
// slightly different way.
// But, no type error reported.
def bar(x: Boxed[IO^]): Unit =
  val x1: Boxed[IO^] = x
  val io = x1.unbox
  io.use()

Output

-- Error: issues/localreach.scala:9:4 ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
9 |  x.unbox.use()  // error: local reach capability {x*} leaks
  |  ^^^^^^^
  |  Local reach capability x* leaks into capture scope of method foo

(only one error reported)

Expectation

Both functions should have a type error.

/cc @odersky

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions