Class for monad transformers

Stream: lean4

[James Gallicchio]

Does Lean core have a way to express that a parameter is a monad transformer? MonadFunctor is too general, and I'm not sure how to get typeclass synthesis to find the value of type ∀ m, [Monad m] → MonadFunctor m (StateT Unit m), even though a compatible instance is declared in the core.

Should I make my own MonadTransformer typeclass?