Make MonadControlT the transitive closure of MonadControl

[Shamrock-Frost]

Summary

Changes the types of MonadControl.restoreM and MonadControlT.restoreM. See https://github.com/leanprover/lean4/issues/2894 for more information, I'm not sure whether the difference between the existing types is or is not intentional

[github-actions[bot]]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-16 21:30:15)

[kim-em]

The current PR title makes it sounds like an instance is missing. Perhaps change to "feat: align definition of MonadControlT with MonadControl"?

[kim-em]

Please rebase onto origin/nightly so we can get a Mathlib CI run.

[kim-em]

Update: a PR touching MonadControl and MonadControlT is likely to take a long time to review, because this is a complex system that affects many internals. If this is blocking progress on something critical, please let us know, but otherwise this will probably be marked as low-priority.