Can I either tie, or avoid, this knot, without the `IORef` detour?

I'd like to describe a (web single-page) application, where input events are generated asynchronously from UI element-installed callbacks. My current implementation is the following:

record App (m : Type -> Type) (input : Type) (output : Type) where
  constructor MkApp
  view : (input -> m ()) -> m (output -> m ())
  model : input -> m output
  initial : output

runApp : HasIO m => App m input output -> m ()
runApp app = do
  box <- newIORef (\i => pure ())
  refresh <- app.view (\i => readIORef box >>= ($ i))
  writeIORef box $ \i => app.model i >>= refresh
  refresh app.initial

I don't like the IORef detour in runApp. In Haskell, I could use a MonadFix constraint on m to tie the knot, but that would then have the problem of a potential runtime crash if view calls the input event sink synchronously before returning.

So, what would be a nice (or at least nicer) way of modeling App and implementing runApp in Idris2?