feat: generalize ReaderT instances

[digama0]

There are no behavioral changes here, only generalizing things like "ReaderT r m is an applicative when m is" to all the defined semimonad types instead of assuming Monad for everything.

[leodemoura]

bench!

[digama0]

I think the bang is on the other side. Can I do that?

!bench

...guess not.

[leodemoura]

!bench

[leanprover-bot]

Here are the benchmark results for commit c60f108.
There were significant changes against commit 578adcd:

  Benchmark   Metric       Change
  ========================================
- stdlib      task-clock       1% (77.2 σ)

[leodemoura]

!bench

[leodemoura]

@digama0 Did you find out what was triggering the stack overflow in debug mode?

[digama0]

No, in the end I ran out of time / patience on debugging and just did black box testing to find the part of the PR that doesn't hit the error. That's also why it scaled back from the original intent (it's not really generalizing the instances anymore, only adding implementations for the missing functions). If we could find the culprit we might be able to do this better later.

If you are interested in pursuing this, here's a list of things that cause the error:

• Inlining ReaderT.pure or ReaderT.bind into the instance
• Generalizing any of the instances to, e.g. [Pure m] : Pure (ReaderT r m) instead of [Monad m] : Pure (ReaderT r m)
  • This includes ReaderT.pure, even though it's not even an instance

The working theory is that inlining these cause lean to be more aggressive about inlining generally for monad stacks including ReaderT. We generally want ReaderT to be inlined, but it is possible that there is something else that we don't want to inline that is being hidden behind the ReaderT implementation. The error occurred in debug mode when elaborating 1365.lean, so it is likely during the construction of the Repr instance, but concretely it is a stack overflow that occurs in instantiateMVars inside mkInjectiveTheorems.

[leanprover-bot]

Here are the benchmark results for commit ebf5b1a.
There were no significant changes.

[leodemoura]

@digama0 Thanks for the explanation. I will try to take a look later at the StackOverflow issue.