CC: Improve inference of functions (Typing boundary/break) #22481
Description
Compiler version
Latest nightly
Minimized code
With recent support for capture variables, abstract capture members and paths
in and to captures, we can obtain a reasonable signature for boundary/break
or similar delimiter pairs that prevent leaking inner labels,
using path-dependent types:
import language.experimental.captureChecking import caps.* trait BoundaryBreak: trait Label extends Capability: type Cap >: CapSet <: CapSet^ def boundary[T,C^](block: Label{type Cap = C} ->{C^} T): T = ??? def suspend[U](label: Label)(handler: () ->{label.Cap^} U): U = ??? def test = val x = 1 boundary: outer => val y = 2 boundary: inner => val z = 3 suspend(outer): () => println(inner) // error , good! x + y + z trait File extends Capability: def write(s: String): Unit def read(): String def test2 = val f1: File = ??? boundary: outer => val f2: File = ??? suspend(outer): () => f1.write("ynot") // error, but should be legalOutput
In test2, we get an error:
-- Error: local/boundarybreak.scala:36:8 --------------------------------------- 36 | f1.write("ynot") | ^^ |reference (f1 : BoundaryBreak.this.File^) is not included in the allowed capture set {outer.Cap^} |of an enclosing function literal with expected type () ->{outer.Cap^} Unitbut we can make it work by explicitly annotating the expected capture set of the body:
def test3 = val f1: File = ??? boundary[Unit,CapSet^{f1}]: outer => val f2: File = ??? suspend(outer): () => f1.write("ynot") // accepted now!Expectation
Ideally, inference of types/captures would correctly infer CapSet^{f1}