bindA is incoherent with the associativity of >>=

[garrigue]

bindA has type (m >>= f) >>= g = m >>= (fun x => f x >>= g), which means that it moves parentheses from left to right. However, >>= is left associative, so that bindA augments the number of parentheses. This is incoherent with usual orientation of associativity lemmas.

Proposed solution: make it non-associative.

Note that from a computational point of view, it might be more natural for >>= to be right-associative, but as discussed for Haskell this is not possible since >>= is heterogeneous. Haskell makes it left-associative too.