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