Impure arity types

I tried to define some effects with impure arities / coarities (i.e., impure parameter and result types) but I failed. I wonder if this is possible in Effekt without using the special syntax for bidirectional effects.

For example, I want to define an operation `Get : () => (() ->{Exc} String)` which takes a unit and returns an impure function that takes a unit, returns a string, and might invoke the effect `Exc`. At the first attempt, I wrote down the following Effekt code
```
effect Exc[A](msg: String): A
effect Get(): => Int at { Exc }
```
which gave me the following error
```
[error] ./issue.effekt:4:27: Could not resolve capture Exc
effect Get(): => Int at { Exc }
```
I had no idea why this error appeared, because `Exc` is defined just before `Get`. To figure out the reason, I wrote down some testing code with different combinations of blocks, boxed blocks, capability types, and capability instances as follows.
```
interface Greeter {
def sayHello(): Unit
}

def hand1{f: => Unit / { Greeter }} = try f() with Greeter {
def sayHello() = { println("hi"); resume(()) }
}

def hand2{f: => Unit / { greeter }} = try f() with greeter: Greeter {
def sayHello() = { println("hi"); resume(()) }
}

def hand3(f: => Unit at { Greeter }) = try f() with Greeter {
def sayHello() = { println("hi"); resume(()) }
}

def hand4(f: => Unit at { greeter }) = try f() with greeter: Greeter {
def sayHello() = { println("hi"); resume(()) }
}
```
Only `hand1` is well-typed. The `hand2` is ill-typed with the error `Could not resolve type greeter`. The `hand3` is ill-typed with the error `Could not resolve capture Greeter`. The `hand4` is ill-typed with the error `Could not resolve capture greeter`.

Looking at `hand3` and `hand4`, I guessed the reason is that there is a lexical scoping condition for the appearance of capabilities on types. The following well-typed code verified my guess.
```
def wrapper() = {
try {
def hand2( f: => Unit at { greeter } ) = 42
42
} with greeter: Greeter { def sayHello() = { println("hello"); resume(()) } }
}
```
Also, I came up with the following assumptions about how Effekt works:
1. For block type `A => B / {E}`, E can only contain capability types, e.g., `Greeter`.
2. For boxed block type `A => B at {E}`, E can only contain capability instances, e.g., `greeter`.
3. Capability types have their globally unique names, and can appear flexibly in types with no scoping condition. (`hand1` is well-typed)
4. Capability instances must be well-scoped (i.e., used in the scope that they are introduced such as the scope of their handlers), even though they only appear in types. (`hand4` is ill-typed but `wrapper` is well-typed)

These assumptions seem to be different from the formalisation of the "Effects, Capabilities, and Boxes" paper, because in the paper there is no lexical scoping condition on capabilities at all when they appear on types after `at`. If there is indeed such lexical scoping condition, it would be restrictive without explicit abstraction over capability instances, evidenced by the fact that I failed to define effects with impure arities.

I wonder if my assumptions are correct and if there is a good reference to look at.

Back to the initial question of having impure arities / coarities, it seems that it is indeed impossible because of the lexical scoping condition. I'd like to know whether this is correct since I'm very unfamiliar with Effekt and probably just made some stupid mistakes.