MonadControlT vs transitive closure of MonadControl

Stream: lean4

[Brendan Seamas Murphy]

The doc string for the MonadControlT class says "Transitive closure of MonadControlT". If this is the case, why is the input MonadControlT.stM m n α of MonadControlT.restoreM not wrapped in m? I don't really understand this stuff well enough to figure out if there's some intentional difference between MonadControlT.stM and MonadControl.stM that works out because of typeclass resolution, but it seemed off to me

[Brendan Seamas Murphy]

I'm writing down and formalizing the laws for MonadControl as stated in Haskell's monad-control package and this is tripping me up. There also seem to be some design decisions in haskell monad transformers libraries that are influenced by parametricity, more specifically there are external free theorems that we can't prove in lean because e.g. they fail in the precense of LEM and this implies certain coherence conditions for the typeclasses. I'm not sure if this is relevant to anything right now, but I wanted to point it out

[Jannis Limperg]

The "transitive closure" refers to the declared instances, not to their methods. This means that MonadControlT and MonadControl provide the exact same interface, but MonadControl instances perform only one step of lifting (from m, say, to Reader σ m) while MonadControlT instances perform any finite number of steps (from m, say, to Reader σ (ExceptT ε m)).

variable (m : Type → Type) [Monad m] (ε σ : Type)

#synth MonadControl m (ReaderT σ m)
#synth MonadControl m (ExceptT ε m)
#synth MonadControl m (ReaderT σ (ExceptT ε m)) -- fails
#synth MonadControlT m (ReaderT σ (ExceptT ε m))

So in practice, you always declare MonadControl instances and when you have a function that uses the MonadControl interface, you give it a MonadControlT instance argument. There's also a similar pattern for MonadLift/MonadLiftT and probably similar classes.

[Brendan Seamas Murphy]

But they don't have the same interface, the type of restoreM is different

[Jannis Limperg]

Ah! Sorry, I didn't realise there was a discrepancy there even though you pointed it out explicitly. I'm not sure that's intentional.