We use `MProd` instead of `Prod` to group values when expanding the
`do` notation. `MProd` is a universe monomorphic product.
The motivation is to generate simpler universe constraints in code
that was not written by the user but generated by the `do` macro.
Note that we are not really restricting the macro power since the
`HasBind.bind` combinator already forces values computed by monadic
actions to be in the same universe.
The new test cannot be compiled without this modication.
@Kha `withReader` is a well-behaved version of `adaptReader`. `adaptReader` is
too general, and it often produces counterintuitive elaboration
errors.
Here are two super annoying issues I hit all the time:
1- `adaptReader` + polymorphic code
```
def ex1 : ReaderT Nat IO Unit :=
adaptReader (fun x => x + 1) $
IO.println "foo" -- 3 Errors here failed to synthesize `Monad ?m` and `MonadIO ?m`, and don't know how to synthesize `Type → Type`
```
2- `adaptReader` and notation that requires the expected type
```
structure Context :=
(x y : Nat)
def ex2 : ReaderT Context IO Nat :=
adaptReader (fun s => { s with x := 10 }) $ -- Error at the structure instance
...
```
In the example above, I have to write `fun (s : Context) => ...` to
fix the problem.
The two problems above happen in the old and new frontends. However,
there is a new problem specific for the new frontend. In the new
frontend, a `do` is only elaborated when the expected type is known.
So, `adaptReader (fun ctx => ...) do ...` seldom works :(
As I said above, the issue is that `adaptReader` is too general. Its
type is
```
{ρ ρ' : Type u_1} → {m m' : Type u_1 → Type u_2} → [MonadReaderAdapter ρ ρ' m m'] → {α : Type u_1} → (ρ' → ρ) → m α → m' α
```
`withReader` is a simpler version of `adaptReader`
```
withReader : {ρ : Type u_1} → {m : Type u_1 → Type u_2} → [MonadWithReader ρ m] → {α : Type u_1} → (ρ → ρ) → m α → m α
```
It doesn't have any of the problems above. Moreover, I managed to replace
every single instance of `adaptReader` with `withReader` at the stdlib
and tests. We don't need the `adaptReader` generality.
@Kha I did not implement support for reassignments and `continue`,
`break`, `return` inside the `finally` clause. It is doable, but it
feels like unnecessary complexity. We currently don't have any
instance in our code base where this would be useful.
@Kha The new `do` notation works for pure code too.
It automatically inserts `Id` if the expected type is not a monad.
This works great when we are not conflating data and control.
After deleting `Monad List`, we will be able to write functions such as
```lean
def mapWhen (p : Nat → Bool) (f : Nat → Nat) (xs : List Nat) : List Nat := do
for x in xs do
if p x then
x := f x
```
without adding `Id.run` before the `do`.
In the following example, the output produced by `dbgTrace!` was not
being captured. It could break the lean server. At least, it broke the lean4-mode.
```lean
def f (x : Nat) : Nat :=
dbgTrace! ">>> " ++ toString x;
x + 1
eval f 10
```
cc @Kha
