Mutual recursive objects - when to allow them?

[marzipankaiser]

Assume we defined:

interface Ping { def ping(): Unit }
interface Pong { def pong(): Unit }

Then, the following top-level definition is accepted by Effekt (albeit not working for LLVM):

def pinger = new Ping { def ping() = ponger.pong() }
def ponger = new Pong { def pong() = pinger.ping() }

(let's ignore non-termination here, we could add a counter).

Locally in a function, this does not compile (ponger is not defined):

def foo() = {
  def pinger = new Ping { def ping() = ponger.pong() }
  def ponger = new Pong { def pong() = pinger.ping() }
  ()
}

Also, the following (which uses boxing implicitly) doesn't work (locally or globally):

def mkPing {ponger: Pong} = new Ping { def ping() = ponger.pong() }
def mkPong {pinger: Ping} = new Pong { def pong() = pinger.ping() }

def pingr = unbox mkPing { pongr }
def pongr = unbox mkPong { pingr }

IIUC, this means that mutually recursive interface definitions are only possible on the toplevel, and not in LLVM. Is this the behavior we want? Which of those should work? (Are there interesting other variants?)