Generalizing over `MetaM`

Stream: lean4 dev

[Joachim Breitner]

I have a complicated function with callbacks that runs in MetaM, but I now want to use it at StateT … MetaM, so I am trying to generalize it. It works with

def transform
    {n} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadEnv n] [MonadLog n]
    [AddMessageContext n] [MonadOptions n]
    …

but it seems a bit of an excessive list of constraints, some redundant. Is that fine, or should I approach it differently?

(Here is the actual change)

[Jannis Limperg]

I guess that the first three (MonadLiftT, MonadControlT, Monad) are sufficient if you write, e.g., show MetaM _ from getEnv instead of getEnv. Not sure whether that's an improvement though...

[Joachim Breitner]

Yeah, or just MonadControlT is enough if I wrap every operation that I need to specialize in some lift operations, but then the code gets much uglier…

[Kyle Miller]

Have you seen how docs#Lean.Meta.forallTelescope works? It takes a continuation in a different monad, but the underlying implementation takes a MetaM continuation. It uses docs#Lean.Meta.map2MetaM, which I haven't understood yet.

[Joachim Breitner]

I had a look, but I think the map2MetaM-family only works when there is a single continuation that is called exactly once; my MatcherApp.transform function is more complicated than that.

I could probably try to thread through the ControlMonadT’s stM state manually in MatcherApp. I briefly tried, but it seemed differently, but similarly annoying than the plethora of type class constraints.