MonadControlT is not the transitive closure of MonadControl

[Shamrock-Frost]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The docstring of MonadControlT says that it's the transitive closure of MonadControl, but the types of MonadControl.restoreM and MonadControlT.restoreM are different. It's not clear to me why this is, and it's different from the relationship between MonadLiftT and MonadLift (whose fields are identical). I think this should either be clarified in the documentation or changed so that the types agree. I don't know what the intended behavior is here.

Context

I've been adding typeclasses for lawful MonadLift and MonadControl and was unable to implement

instance instLawfulMonadControlT.{u, v₁, v₂, v₃} (m : Type u → Type v₁) (n : Type u → Type v₂) (o : Type u → Type v₃)
  [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
  [MonadControl n o] [MonadControlT m n] [LawfulMonadControl n o] [LawfulMonadControlT m n]
    : LawfulMonadControlT m o

If the difference between the types of MonadControl.restoreM and MonadControlT.restoreM is intentional I would appreciate any suggestions on what the laws for MonadControlT should be.

I asked about this in a zulip thread.

Versions

[Output of #eval Lean.versionString] 4.3.0-rc1 [OS version] Windows 11 Home, 10.0.22621 Build 22621

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.