重叠多参数实例和实例特异性

Question

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
module OverlappingSpecificsError where

class EqM a b where
    (===) :: a -> b -> Bool

instance {-# OVERLAPPABLE #-} Eq a => EqM a a where
    a === b = a == b

instance {-# OVERLAPPABLE #-} EqM a b where
    a === b = False

aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyreallyeq (Left a1) (Right b2) = a1 == b2

aretheyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyeq (Left a1) (Right b2) = a1 === b2

aretheyreallyeq 或 aretheyeq 都无法编译，但 aretheyreallyeq 的错误对我来说是有意义的，并且还告诉我 aretheyeq 不应该给出错误：GHCi 建议的实例之一对于 @ 是可能的由于aretheyreallyeq 上的相同错误，aretheyeq 中的 987654326@ 应该是不可能的。怎么回事？

关键是，GHCi 坚持EqM 的两个实例都适用于aretheyeq。但是a1 是a 类型，而b2 是b 类型，所以为了使第一个实例适用，它必须具有a 和b 类型统一。

但这应该是不可能的，因为它们在函数签名处被声明为类型变量（也就是说，使用第一个 EqM 实例会导致函数的类型为 Either a a -> Either a a -> Bool，并且 @ 中的错误987654339@ 告诉我 GHCi 不允许这样做（无论如何，这是我所期望的）。

我是否遗漏了什么，或者这是如何检查具有多参数类型类的重叠实例的错误？

我在想这可能与a 和b 可以在以后进一步实例化到它们相等的点有关，在aretheyeq 之外，然后第一个实例会 有效吗？但aretheyreallyeq 也是如此。唯一的区别是，如果他们不统一，我们可以选择aretheyeq，但我们没有aretheyreallyeq。在任何情况下，Haskell 没有动态调度有很多好的和明显的原因，所以在提交实例时担心会总是工作，无论以后是否a 和@987654347 @是统一的吗？也许有一些方法可以在调用函数时以某种方式选择实例？

值得注意的是，如果我删除第二个实例，那么该函数显然仍然无法编译，说明找不到实例EqM a b。所以如果我没有那个实例，那么没有一个有效，但是当那个有效时，突然另一个也有效，我有重叠？几英里外我闻起来像虫子。

Answer 1

泛型变量上的实例匹配以这种方式工作，以防止出现一些可能令人困惑（和危险）的情况。

如果编译器屈服于您的直觉并在编译 aretheyeq 时选择了 EqM a b 实例（因为正如您所说，a 和 b 不一定统一），那么以下调用：

x = aretheyeq (Left 'z') (Right 'z')

会返回False，这与直觉相反。

问：等一下！但是在这种情况下，a ~ Char 和b ~ Char，我们还有Eq a 和Eq b，这意味着Eq Char，这应该可以选择EqM a a 实例，不是吗？

嗯，是的，我想这可能在理论上会发生，但 Haskell 就是不能这样工作。类实例只是传递给函数的额外参数（作为方法字典），所以为了有一个实例，它必须在函数本身中明确地选择，或它必须从消费者。

前者（明确选择的实例）必然要求只有一个实例。事实上，如果您删除 EqM a a 实例，您的函数将编译并始终返回 False。

后者（从消费者传递一个实例）意味着对函数的约束，像这样：

aretheyeq :: EqM a b => Either a b -> Either a b -> Bool

您要问的是，Haskell 本质上具有此函数的两个不同版本：一个需要 a ~ b 并选择 EqM a a 实例，而另一个不需要，并选择 EqM a b 实例。

然后编译器会巧妙地选择“正确”的版本。所以如果我调用aretheyeq (Left 'z') (Right 'z')，第一个版本会被调用，但如果我调用aretheyeq (Left 'z') (Right 42) - 第二个。

但现在再想一想：如果aretheyeq 有两个版本，而选择哪一个取决于类型是否相等，那么考虑一下：

dummy :: a -> b -> Bool
dummy a b = aretheyeq (Left a) (Right b)

dummy 如何知道选择哪个版本的aretheyeq？所以现在也必须有两个版本的dummy：一个用于a ~ b，另一个用于其他情况。

等等。涟漪效应一直持续到出现具体类型为止。

问：等一下！为什么有两个版本？不能只有一个版本，然后根据传入的参数决定做什么？

啊，但它不能！这是因为类型在编译时被擦除。当函数开始运行时，它已经编译好了，没有更多的类型信息。所以一切都必须在编译时决定：选择哪个实例，以及从中产生的连锁反应。

Answer 2

这不是工作exactly as documented 意义上的错误。以

开头

现在假设，在某个客户端模块中，我们正在搜索目标约束(C ty1 .. tyn) 的实例。搜索工作如下：

寻找候选实例的第一阶段按您的预期工作； EqM a b 是唯一的候选人，因此是主要候选人。但最后一步是

现在查找与目标约束统一但不匹配的所有实例或范围内的给定约束。当目标约束被进一步实例化时，此类非候选实例可能匹配。如果它们都是不连贯的顶级实例，则搜索成功，返回主要候选者。否则搜索失败。

EqM a a 实例属于这一类，并且不是不连贯的，因此搜索失败。您可以通过将其标记为{-# INCOHERENT #-} 而不是可重叠来实现您想要的行为。

Answer 3

为了进一步完成 Alexey 的回答，这确实给了我应该做些什么来实现我想要的行为的提示，我编译了以下稍微不同的情况的最小工作示例，更类似于我的真实用例（必须这样做ExistentialQuantification):

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ExistentialQuantification #-}
module ExistentialTest where

class Class1 a b where
    foo :: a -> b

instance {-# INCOHERENT #-} Monoid a => Class1 a (Either b a) where
    foo x = Right (x <> x)

instance {-# INCOHERENT #-} Monoid a => Class1 a (Either a b) where
    foo x = Left x

data Bar a = Dir a | forall b. Class1 b a => FromB b

getA :: Bar a -> a
getA (Dir a) = a
getA (FromB b) = foo b

createBar :: Bar (Either String t)
createBar = FromB "abc"

createBar2 :: Bar (Either t String)
createBar2 = FromB "def"

如果您删除 {-# INCOHERENT #-} 注释，您会得到与我在 createBar 和 createBar2 的原始示例中完全相同的编译错误，并且要点是相同的：在 createBar 中，很明显唯一合适的实例是第二个，而在createBar2 中唯一合适的是第一个，但是 Haskell 拒绝编译，因为它在使用它时可能会造成明显的混乱，直到你用注释它们 INCOHERENT.

然后，代码完全按照您的预期工作：getA createBar 返回 Left "abc"，而 getA createBar2 返回 Right "defdef"，这正是合理类型系统中唯一可能发生的事情。

所以，我的结论是：INCOHERENT 注释正是为了让我从一开始就想做我想做的事情，而 Haskell 不会抱怨可能令人困惑的实例，并且确实选择了唯一有意义的实例。关于INCOHERENT 是否可以做到这一点仍然存在疑问，以便即使在考虑到所有内容之后确实仍然重叠的实例使用任意一个（这显然是坏和危险的）编译。因此，我的结论的一个推论是：仅在绝对需要并且绝对确信确实只有一个有效实例时才使用INCOHERENT。

我仍然认为 Haskell 没有更自然和安全的方法来告诉编译器不要再担心我可能会感到困惑并做显然是解决问题的唯一类型检查答案的事情有点荒谬......

Answer 4

aretheyreallyeq 失败，因为作用域中有两个不同的类型变量。在

aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyreallyeq (Left a1) (Right b2) = a1 == b2

a1 :: a 和 b2 :: b，没有方法可以比较可能不同类型的值（因为这是它们的声明方式），所以这失败了。当然，这与任何已启用的扩展或 pragma 无关。

aretheyeq 失败是因为有两个实例可以 匹配，而不是它们肯定匹配。我不确定您使用的是什么版本的 GHC，但这是我看到的异常消息，对我来说似乎很清楚：

    • Overlapping instances for EqM a b arising from a use of ‘===’
      Matching instances:
        instance [overlappable] EqM a b -- Defined at /home/tmp.hs:12:31
        instance [overlappable] Eq a => EqM a a
          -- Defined at /home/tmp.hs:9:31
      (The choice depends on the instantiation of ‘a, b’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: a1 === b2
      In an equation for ‘aretheyeq’:
          aretheyeq (Left a1) (Right b2) = a1 === b2

在这种情况下，我的解释是，给定 a 和 b 的某些选择，可能存在多个不同的匹配实例。