Haskell中的单个实例出现重叠实例错误

Question

我在Haskell上有以下代码：

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, ExistentialQuantification, ConstraintKinds #-}
import Data.Proxy
class C p a b where
c :: p b -> a -> Maybe (Ctx b)
class X a
instance X ()
data Ctx ctx = forall a. ctx a => Ctx a
instance C p (Ctx a) a where
c _ = Just
instance C Proxy a b where
c _ _ = Nothing
x :: Maybe (Ctx X)
x = c (Proxy :: Proxy X) (Ctx () :: Ctx X)

但当我试图编译这段代码(或在ghci中加载(时，我得到了错误：

* Overlapping instances for C Proxy (Ctx X) X
arising from a use of `c'
Matching instances:
instance C p (Ctx a) a
-- Defined at Main.hs:14:10
There exists a (perhaps superclass) match:
(The choice depends on the instantiation of `'
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
* In the expression: c (Proxy :: Proxy X) (Ctx () :: Ctx X)
In an equation for `x': x = c (Proxy :: Proxy X) (Ctx () :: Ctx X)
|
21 | x = c (Proxy :: Proxy X) (Ctx () :: Ctx X)
|     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

为什么？

如果我删除最后一个实例声明instance C Proxy a b，它可以正常工作。为什么？

我尝试在第一个实例声明中添加{-# OVERLAPPING #-}杂注，或在第二个实例声明上添加{-# OVERLAPPABLE #-}，但错误仍然存在。为什么？

但如果我将第二个实例标记为{-# INCOHERENT #-}，它将被成功编译。

Answer 1

实例C p' (Ctx a') a'和C Proxy a' b'对于约束C Proxy (Ctx a'') b''是相同特定的匹配，主要是因为它们都需要在类头C p a b中进行单个替换，即p ~ Proxy或a ~ Ctx a'。

只有当编译器可以选择最特定的匹配实例时，重叠实例才起作用，这就是为什么此代码需要IncoherentInstances才能选择第一个匹配。如果没有关于您要做什么的进一步上下文，很难建议您如何更改代码以避免这种情况。如果可以确保两个实例都产生相同的行为，但它们当前没有，则不需要来避免这种情况。您期望x的值是多少？

正如@AntC在评论中指出的那样，将一个实例优先于另一个实例的一种方法是将匹配的移出实例头的，从而使其不那么具体，并引入相等约束：

• instance (p ~ Proxy) => C p a b
• instance (a ~ Ctx a', b ~ a') => C p a b

此类约束是在匹配实例后引入的。然后，您可以使用杂注来指定，例如，不太特定的实例是OVERLAPPABLE，和/或更特定的实例为OVERLAPPING。

如果您打算将您所表示的关系表示为函数，那么可能更容易推断基于(封闭(类型族的实现，而不是MPTC的完全通用性。