I've heard that there are some problems with Haskell's "broken" constraint system, as of GHC 7.6 and below. What's "wrong" with it? Is there a comparable existing system that overcomes those flaws?
For example, both edwardk and tekmo have run into trouble (e.g. this comment from tekmo).
好的，在发帖之前，我与其他人进行了几次讨论，因为我想把这件事做好。他们都向我表明，我描述的所有问题都归结为缺乏多态约束。
这个问题最简单的例子就是MonadPlus类，定义为：
class MonadPlus m where
mzero :: m a
mplus :: m a -> m a -> m a
...具有以下法律：
mzero `mplus` m = m
m `mplus` mzero = m
(m1 `mplus` m2) `mplus` m3 = m1 `mplus` (m2 `mplus` m3)
请注意，这些是Monoid法律，其中Monoid类由下式给出：
class Monoid a where
mempty :: a
mappend :: a -> a -> a
mempty `mplus` a = a
a `mplus` mempty = a
(a1 `mplus` a2) `mplus` a3 = a1 `mplus` (a2 `mplus` a3)
那么我们为什么还要MonadPlus上课呢？原因是因为 Haskell 禁止我们编写形式的约束：
(forall a . Monoid (m a)) => ...
因此 Haskell 程序员必须通过定义一个单独的类来处理这种特殊的多态情况来解决类型系统的这个缺陷。
然而，这并不总是一个可行的解决方案。例如，在我自己的pipes库工作中，我经常遇到需要对表单提出约束：
(forall a' a b' b . Monad (p a a' b' b m)) => ...
与MonadPlus解决方案不同，我无法将Monad类型类切换到不同的类型类来解决多态约束问题，因为这样我的库的用户会丢失do符号，这是要付出高昂的代价。
这在编写转换器时也会出现，包括单子转换器和我的库中包含的代理转换器。我们想写这样的东西：
data Compose t1 t2 m r = C (t1 (t2 m) r)
instance (MonadTrans t1, MonadTrans t2) => MonadTrans (Compose t1 t2) where
lift = C . lift . lift
第一次尝试不起作用，因为lift不会将其结果限制为Monad. 我们实际上需要：
class (forall m . Monad m => Monad (t m)) => MonadTrans t where
lift :: (Monad m) => m r -> t m r
...但是 Haskell 的约束系统不允许这样做。
随着 Haskell 用户转向更高种类的类型构造函数，这个问题将变得越来越明显。您通常会有以下形式的类型类：
class SomeClass someHigherKindedTypeConstructor where
...
...但你会想要约束一些低种类的派生类型构造函数：
class (SomeConstraint (someHigherKindedTypeConstructor a b c))
=> SomeClass someHigherKindedTypeConstructor where
...
但是，如果没有多态约束，则该约束是不合法的。我最近一直是抱怨这个问题的人，因为我的pipes库使用了非常高级的类型，所以我经常遇到这个问题。
有几个人向我提出的使用数据类型的解决方法，但我（还没有）有时间评估它们以了解它们需要哪些扩展或哪个扩展正确解决了我的问题。更熟悉这个问题的人可能会提供一个单独的答案，详细说明解决方案及其工作原理。
[加布里埃尔冈萨雷斯回答的后续]
Haskell 中约束和量化的正确表示法如下：
<functions-definition> ::= <functions> :: <quantified-type-expression>
<quantified-type-expression> ::= forall <type-variables-with-kinds> . (<constraints>) => <type-expression>
<type-expression> ::= <type-expression> -> <quantified-type-expression>
| ...
...
kinds 可以省略，forallrank-1 类型的 s 也可以省略：
<simply-quantified-type-expression> ::= (<constraints-that-uses-rank-1-type-variables>) => <type-expression>
例如：
{-# LANGUAGE Rank2Types #-}
msum :: forall m a. Monoid (m a) => [m a] -> m a
msum = mconcat
mfilter :: forall m a. (Monad m, Monoid (m a)) => (a -> Bool) -> m a -> m a
mfilter p ma = do { a <- ma; if p a then return a else mempty }
guard :: forall m. (Monad m, Monoid (m ())) => Bool -> m ()
guard True = return ()
guard False = mempty
或没有Rank2Types（因为我们这里只有 rank-1 类型），并使用CPP(j4f)：
{-# LANGUAGE CPP #-}
#define MonadPlus(m, a) (Monad m, Monoid (m a))
msum :: MonadPlus(m, a) => [m a] -> m a
msum = mconcat
mfilter :: MonadPlus(m, a) => (a -> Bool) -> m a -> m a
mfilter p ma = do { a <- ma; if p a then return a else mempty }
guard :: MonadPlus(m, ()) => Bool -> m ()
guard True = return ()
guard False = mempty
“问题”是我们不能写
class (Monad m, Monoid (m a)) => MonadPlus m where
...
或者
class forall m a. (Monad m, Monoid (m a)) => MonadPlus m where
...
也就是说，forall m a. (Monad m, Monoid (m a))可以用作独立约束，但不能使用新的类型的单参数类型类来别名*->*。
这是因为类型类定义机制是这样工作的：
class (constraints[a, b, c, d, e, ...]) => ClassName (a b c) (d e) ...
即rhs端引入类型变量，而不是lhs 或foralllhs。
相反，我们需要编写 2 参数类型类：
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
class (Monad m, Monoid (m a)) => MonadPlus m a where
mzero :: m a
mzero = mempty
mplus :: m a -> m a -> m a
mplus = mappend
instance MonadPlus [] a
instance Monoid a => MonadPlus Maybe a
msum :: MonadPlus m a => [m a] -> m a
msum = mconcat
mfilter :: MonadPlus m a => (a -> Bool) -> m a -> m a
mfilter p ma = do { a <- ma; if p a then return a else mzero }
guard :: MonadPlus m () => Bool -> m ()
guard True = return ()
guard False = mzero
缺点：我们每次使用时都需要指定第二个参数MonadPlus。
问题：如何
instance Monoid a => MonadPlus Maybe a
MonadPlus如果是单参数类型类可以写吗？MonadPlus Maybe来自base：
instance MonadPlus Maybe where
mzero = Nothing
Nothing `mplus` ys = ys
xs `mplus` _ys = xs
不像Monoid Maybe：
instance Monoid a => Monoid (Maybe a) where
mempty = Nothing
Nothing `mappend` m = m
m `mappend` Nothing = m
Just m1 `mappend` Just m2 = Just (m1 `mappend` m2) -- < here
：
(Just [1,2] `mplus` Just [3,4]) `mplus` Just [5,6] => Just [1,2]
(Just [1,2] `mappend` Just [3,4]) `mappend` Just [5,6] => Just [1,2,3,4,5,6]
类似地，forall m a b n c d e. (Foo (m a b), Bar (n c d) e)如果我们想要*类型，则产生 (7 - 2 * 2)-parametric typeclass，类型产生 (7 - 2 * 1)-parametric typeclass，* -> *类型产生 (7 - 2 * 0) * -> * -> *。