Change Monad polymorphism

[WhatisRT]

Monads don't need to work at all levels anymore, and can have a different level for their result type.

This as an attempt at fixing #2.

[omelkonian]

@WhatisRT Please try this PR on the current Cardano ledger formalization and confirm that all monadic code still works, or if any changes were required.

I will report on other instances I have lying around.

[omelkonian]

It is not clear why one would prefer this polymorphism over the previous Type↑ approach:

• results in significantly more boilerplate
• restricts some use cases as demonstrated in the comments

However, it is still more flexible than the previous approach in the output levels, as well as being compatible to stdlib. So, the question becomes:

Do we need the extra lifting of the same-level restriction?
If so, is this PR preferable to generalizing the previous approach instead? e.g.

Level↑ = Level → Level

Type↑↑ : Level↑ → Typeω
Type↑↑ ℓ↑ = ∀ {ℓ} → Type[ ℓ ↝ ℓ↑ ℓ ]

private variable ℓ↑ : Level↑

record Functor (F : Type↑↑ ℓ↑) : Typeω where

(with the above change, all the instances typecheck without additional changes)

[omelkonian]

Here is where the restriction really shows, and in fact goes back to the definition of fmap: we now can't map across levels, e.g. the following code does not make sense any more:

postulate
  X : Type
  Y : Type₁
  g : X → Y
  xs : List X

ys : List Y
ys = fmap g xs

...let alone reasoning with functor laws across levels:

postulate
  Z : Type₂
  f : Y → Z

zs zs′ : List Z
zs  = fmap (f ∘ g) xs
zs′ = (fmap f ∘ fmap g) xs

_ : zs ≡ zs′
_ = fmap-∘ {f = f}{g} xs

[WhatisRT]

You're right, this is another downside here. Though I wonder if it comes up all that often. If I have to choose between this and having a Functor instance for A ⊎_, I'd choose the latter.

[WhatisRT]

I probably should have added an example of what's possible with this change, so I've added a Monad instance for Sum now.

I tried your above suggestion, but it seems to have really bad inference properties. It works fine in the Functor and Applicative modules, but if I try it in Monad I get ~50 unsolved constraints.

Edit: Seems like I was doing something wrong, it works just fine in #19.

[WhatisRT]

This PR breaks the following code:

open import Reflection hiding (_>>=_)
open import Class.Monad

open import Data.Nat

solve : TC Set
solve = getType (quote zero) >>= unquoteTC

This is because the two types involved in the _>>=_ (Reflection.Type and Set) have different levels.

[omelkonian]

Closing in favour of #19