The issue is that you can't prove that whicher set of MonadPlus laws you are using _follows_ from whichever set of Alternative laws you are using.
This discussion is somewhat hampered by neither one having a well-written set of laws, because we use MonadPlus in two or three mutually incompatible ways and for the most part "it just works" so people don't notice.
Consider the space of laws mentioned in:
https://wiki.haskell.org/MonadPlus_reform_proposalThese don't necessarily follow from any of the popular Alternative law proposals.
Left Zero:
On the Applicative side you can do more to explore the tree, can "run" effects right to left, etc.
We have a _left_ zero law for a monadplus:
mzero >>= f = mzero
but not a right one, just because of the existence of the function space in (>>=) that we can't see through
(do putStrLn "die"; mzero) /= mzero
But nothing keeps us from seeing through an (*>) to count up something on the right. Control.Applicative.Backwards exists and would satisfy a "right zero" law if the original satisfied a left zero law.
Left Distribution:
Similarly, you can imagine a data type that is Alternative and also a Monad, but where
mplus a b >>= k = mplus (a >>= k) (b >>= k)
fails to hold in the left distributive style, and it also fails to be in the left catch style.
Without _retiring_ MonadPlus, we should at least use it consistently to imply the requirement of this sort of extra structure, even if it is ambiguous what that structure should be.
-Edward