Undetected escaping capability when using first class functions

[mm0821]

There seems to be a problem with undetected capabilities escaping their delimiters when using first class functions closing over them, if the handler for the corresponding effect is defined in a separate function. In the following example the escaping capability for Effect2 is detected (fcfCaughtErr.txt):

effect Effect1(): Unit
effect Effect2(): Unit


def escape { prog: () => Unit / { Effect1, Effect2 } }: Unit = {
  var k: (Unit) => Unit / { escape } = fun (x: Unit) { () }
  try {
    try {
      prog()
    } with Effect1 { () =>
      k = fun (x: Unit) { resume(x) };
      resume(())
    }
  } with Effect2 { () => resume(()) }
  k(())
}

def main() = {
  escape { do Effect1(); do Effect2() }
}

However, if the handler for Effect2 is defined in the function handle2 as is done here

effect Effect1(): Unit
effect Effect2(): Unit


def handle2 { prog: () => Unit / { Effect2 } }: Unit = {
  try { prog() }
  with Effect2 { () => resume(()) }
}

def escape { prog: () => Unit / { Effect1, Effect2 } }: Unit = {
  var k: (Unit) => Unit / { escape } = fun (x: Unit) { () }
  handle2 {
    try {
      prog()
    } with Effect1 { () =>
      k = fun (x: Unit) { resume(x) };
      resume(())
    }
  }
  k(())
}

def main() = {
  escape { do Effect1(); do Effect2() }
}

this is not detected and results in a runtime error (fcfUncaughtErr.txt).

[b-studios]

Thanks for reporting! This is a soundness bug with region inference on continuations. Instead of using escape on the region, we need to use the lambda passed to handle2 as the current region. This might be overly restrictive in some cases, but would be along the lines of our current region approximation and would prevent this source of unsoundness.

[b-studios]

This really was an oversight on my sight, as can be seen in the branch fixing it. Lambdas (that is, fun() { ... }) did introduce a new region, but anonymous block arguments (like in handle2 { ... }) did not. This is clearly wrong as illustrated by your example.