[Agda] Monads with polymorhic bind.

[flicky frans]

Hi. I'm trying to implement more or less usable monads with
polymorphic bind. Here is the attempt:

record RawMonad {α β : Level} (M : {γ : Level} → Set γ → Set γ) : Set
(suc (α ⊔ β)) where
  infixl 1 _>>=_
  field
    return : {A : Set α} → A → M A
    _>>=_  : {A : Set α} {B : Set β} → M A → (A → M B) → M B

But β does not mentioned in the type of return, so it produces
unresolved metas from time to time.
It can be used however like this:

open RawMonad {{...}}
module MonoMonad {α} = RawMonad {α} {α}
module MM = MonoMonad {{...}}

test3 : (b : Bool) -> Maybe Set₁
test3 b = boolToMaybe b >>= λ _ -> MM.return Set

But return is always "monomorphic", so it should be just return and
not MM.return. That's how I got this bug:
http://code.google.com/p/agda/issues/detail?id=1094&thanks=1094&ts=1396747124

Some examples: http://lpaste.net/7187804666674020352
Does this approach have another disadvantages? Are there better approaches?