Youssef Shoaib

I've updated with a simpler example to show the issue. It seems to require both boxing (to dynamically remove a prompt) and bidirectional effects (for `resume` to have the incorrect...

FYI, here's an [example](https://github.com/effekt-lang/effekt/issues/395#issuecomment-1969012129) (check the "Details" section) of code that, if changed around, may exhibit the same bug: > ``` > def twice[R](default: R) = { > var other:...

@b-studios I (very respectfully) disagree, tentative on what a "theoretical problem" is, and with full acknowledgement that I may be very wrong, especially since I didn't design this language 😅...

@phischu Thank you, first of all! I've been into effect handlers the past couple of years, with the goal of implementing then in Kotlin, and Effekt, in particular, has had...

> forbid closing over _any_ capabilities in the block passed to resume. Except for capabilities that `resume` already captures, right? So that one can use outer handlers inside `resume` just...

Out of curiosity, doesn't Effekt have proofs of effect safety and such? I haven't looked thru some of papers in a while, but I'm guessing the combination of bidirectional effects...

Is this considered fully eta-expanded? ```effekt def res() = resume(()) ``` because one can then `box res`, and I don't see how you'd track that easily. Similarly, this is allowed:...

A mildly less naive version is: - Check all bidirectional `resume`s first (before any other type checking for `resume`) - if any of them capture a middle handler, typecheck using...

I didn't think too hard about the local mutual recursion here, so that's a good thing to point out! It'd be ideal if that could be supported somehow, but even...

With #948, this'd come in handy so that one may write a generic `summon`: ```effekt def summon[T](): (T at t) / {t: T} = t ```