haskell - 为什么这违反了 "Coverage Condition"

Question

阅读UndecidableInstances我明白我的问题在 this question相当于:

class Convert a b | a -> b where
     convert :: a -> b

instance Convert a b => Convert [a] [b] where
     convert = map convert

我理解为什么“UndecidableInstance”是必要的以及(某种程度上)为什么类型检查器可以在某些情况下循环。不过，我还是不明白它怎么违反了“承保条件”。我的意思是，当我阅读定义时

For each functional dependency, tvsleft -> tvsright, of the class, every type variable in S(tvsright) must appear in S(tvsleft), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration.

前面的例子似乎满足这个定义。我知道不是，但我不明白为什么(我可能不太明白)。

Answer 1

我猜你和我一样，首先认为 tvsleft 与实例中 => 左侧的部分有关。但仔细阅读后，我发现事实并非如此。至少对于这个例子来说，这只是对实例head的限制。

对于带有头 Convert a b 和函数依赖 a -> b 的类，我们有

tvsleft = a
tvsright = b

对于实例，我们必须替换类头中的变量 Convert a b 以获得实例头 Convert [a] [b]，给出

S(tvsleft) = S(a) = [a]
S(tvsright) = S(b) = [b]

并且[b]中的类型变量b不会出现在[a]中。