Lifting `StateRefT`

Stream: lean4

[Leni Aniva]

If I want to run StateRefT State M1 inside StateRefT State M2 when MonadLiftT M1 M2, how can I define an instance to do so?

e.g. this doesn't work and it's quite long already

instance [Monad M₁] [Monad M₂] [MonadLiftT IO M₁] [STWorld σ₁ M₁] [MonadLiftT (ST σ₁) M₁] [STWorld σ₂ M₂] [MonadLiftT (ST σ₂) M₂] [MonadLiftT M₁ M₂]
  : MonadLift (StateRefT State M₁) (StateRefT State M₂) where
  monadLift m := do
    let (a, σ) ← m.run (← get)
    set σ
    return a

[Jovan Gerbscheid]

This works:

variable {M₁ M₂ : Type → Type} {σ : Type} {State : Type}
instance [Monad M₁] [Monad M₂] [STWorld σ M₁] [STWorld σ M₂] [MonadLift M₁ M₂] :
    MonadLift (StateRefT State M₁) (StateRefT State M₂) where
  monadLift m := fun ref => m ref