@Mathew In the definition

``
interpret t = run t ()
``

GHC complains with

``
Variable not in scope: run :: r0 h0 a -> () -> a
``