Change Monad polymorphism

[omelkonian]

competitor to PR #11 (a more general solution to #2)

This approach stems from a comment originally posted by @omelkonian in #11 (review)

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

[omelkonian]

@WhatisRT the plot thickens!

Now there is a crucial drawback to this more liberal polymorphism: due to inner quantification over the levels (in contrast to stdlib's outer quantification), we lose the ability to support non-level-polymorphic types, e.g.

data newtype₀ (A : Type) : Type where
  mk : A → newtype₀ A

instance
  _ : Functor newtype₀
  _ = ?

(Type ℓ) != Type
when checking that the expression newtype₀ has type
Class.Core.Type[ ℓ ↝ _ℓ↑_393 ℓ ]

[WhatisRT]

Yes, you're right. So it seems we're in a situation where we have two mutually exclusive properties that we want: level-monomorphic instances, and cross-level functions.

I feel like monomorphic instances are mostly a convenience thing though. I don't think I could come up with a construction that is actually practically relevant that cannot be extended to a polymorphic one. Whereas the cross-level functions clearly do have use cases.