Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses

This is an idea how to fix #80 and #207 . Since M never appears unapplied, it should not introduce the universe constraints. Note that the universe of gmap and gset and similar remain constrained due to the MonadSet and FinMap typeclasses.

In particular, with

Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
Global Instance x : MBind list.
Admitted.
Print Universes.

one gets the contraint list.u0 = MBind.u0. But with

Class MBind' (A MA MB : Type) := mbind : (A → MB) → MA → MB.
Notation MBind M := (∀ A B, MBind' A (M A) (M B)).
Global Instance x : MBind list.
Admitted.
Print Universes.

one only gets the constraints

x.u0 <= list.u0
x.u0 <= MBind'.u0
x.u0 <= MBind'.u1
x.u1 <= list.u0
x.u1 <= MBind'.u2