import language.experimental.captureChecking
import caps.*
class Ref(private var x: Int):
  def get = x
  def set(y: Int) = x = y
trait Region extends SharedCapability:
  r: Region^ =>
    type R^
    def alloc(x: Int): Ref^{R} = Ref(x)
    def subregion[T](f: (Region { type R >: r.R }) => T): T =
      class R2 extends Region:
        type R = r.R
      f(new R2)
def withRegion[T](f: Region => T): T = f(new Region {})
@main def main() =
  withRegion: r1 =>
    val x = r1.subregion[Ref^{r1.R}]: r2 =>
      var a: Ref^{r1.R} = r1.alloc(0)
      var b: Ref^{r2.R} = r2.alloc(0)
      val c: Ref^{r1.R} = b
      a
    0

-- Error: issues/cc-region.scala:17:36 -------------------------------------------------------------------------------------------------------------------------------------------------
17 |    val x = r1.subregion[Ref^{r1.R}]: r2 =>
   |            ^
   |            Local reach capability r1.R leaks into capture scope of enclosing function.
   |            You could try to abstract the capabilities referred to by r1.R in a capset variable.
18 |      var a: Ref^{r1.R} = r1.alloc(0)
19 |      var b: Ref^{r2.R} = r2.alloc(0)
20 |      val c: Ref^{r1.R} = b
21 |      c
1 error found