Would `MonadLift (StateM σ) (StateT σ m)` make sense

Stream: lean4

[Mai]

I find it counterintuitive you can't bind a StateM σ in a StateT σ Option, for example. Would adding something like this make sense?

instance [Pure m] : MonadLift (StateM σ) (StateT σ m) where
  monadLift m σ := m σ

[Jovan Gerbscheid]

I think this is similar to the Option/OptionT matter from the other thread, in the sense that there is a different way to write what you want that is clearer than an implicit coercion.

In particular, if f : StateM σ α, then you can write modifyGet f : StateT σ m α.