Not enough unification of capture set between handler body and implementation

[phischu]

Consider the following program:

effect something(): Unit

def main(): Unit = {
  val thunk = try {
    do something()
    box { return () }
  } with something {
    box { println("hello"); val _ = resume(()) }
  }
  thunk()
}

It fails to typecheck with "Not allowed {io}". I would like it to typecheck as written.

The following two variants do typecheck:

effect something(): Unit

def main(): Unit = {
  val thunk = try {
    do something()
    box { return () } at io
  } with something {
    box { println("hello"); val _ = resume(()) }
  }
  thunk()
}

Where we explicitly annotate the io capture on the returned box.

Also, surprisingly:

effect something(): Unit

def main(): Unit = {
  val thunk = try {
    do something()
    box { return () }
  } with something {
    box { println("hello") }
  }
  thunk()
}

Where we do not resume.

[jiribenes]

Is this somehow related to one of the other plethora of capture-related issues? 👀