使用类型相等约束修复了不明确的类型变量

Question

我正在开发一个一元流媒体库，遇到了一个我不理解的类型问题。我已经设法将其简化为以下示例：

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
class Foo a b where
  type E a b :: *
  (>->) :: a -> b -> E a b
data Bar x
instance Foo (Bar x) (Bar x) where
  type E (Bar x) (Bar x) = Bar x
  (>->) = undefined
x = undefined :: Bar a
y = undefined :: Bar Int
z = x >-> y

当我试图编译它时，我得到：

No instance for (Foo (Bar a0) (Bar Int))
  arising from a use of ‘>->’
The type variable ‘a0’ is ambiguous
Relevant bindings include
  z :: E (Bar a0) (Bar Int)
    (bound at /usr/local/google/home/itaiz/test/test.hs:17:1)
Note: there is a potential instance available:
  instance Foo (Bar x) (Bar x)
    -- Defined at /usr/local/google/home/itaiz/test/test.hs:10:10
In the expression: x >-> y
In an equation for ‘z’: z = x >-> y

我想，这会让我有点惊讶，尽管可能不会太惊讶。真正让我惊讶的是，如果我用以下内容替换实例，那么一切都正常：

instance (x ~ x') => Foo (Bar x) (Bar x') where
  type E (Bar x) (Bar x') = Bar x
  (>->) = undefined

我看不出这两个实例声明之间有什么区别。我猜这与类型变量的作用域有关。有人能解释一下发生了什么吗？

[旁白：我在使用fundeps时也看到了同样的情况。]

Answer 1

编辑：关于实例解析的GHC用户指南部分是一个很好的起点。

以下是如何分解为什么会发生这种情况。您的z大致相当于：

z :: Bar a -> Bar Int -> E (Bar a) (Bar Int)
z = (>->)

现在更清楚为什么这是不可能的了吗？我们得到的错误是：

SO26146983.hs:20:5:
    No instance for (Foo (Bar a) (Bar Int)) arising from a use of `>->'
    In the expression: (>->)
    In an equation for `z': z = (>->)

没有什么可以显示a ~ Int。让我们重写一下：

z' :: (a ~ Int) => Bar a -> Bar Int -> E (Bar a) (Bar Int)
z' = (>->)

即使使用原始实例，这也能很好地工作。（编辑：我怀疑下面的句子要么没有帮助，要么有误导性，要么两者兼而有之。）z'（大致）是类型检查器最终得到重写的实例定义的地方：它看到(Bar a) (Bar a')的一个需要(a ~ a')的实例，并将该约束添加到调用中。

粗略地说，实例解析从右到左，有时会产生意想不到的后果。

编辑：从右到左分辨率的结果是instance (x ~ x') => Foo (Bar x) (Bar x')匹配任何两种类型的x和x'，无论x ~ x'是否真的是这样。约束仅传播到调用站点。因此，您不能为特定类型编写另一个实例。它会重叠，这是默认情况下禁止的，而且GHC在解决实例时特别不会回溯。另一方面，instance Foo (Bar x) (Bar x)不会被应用，除非它在两个地方都是相同的类型——GHC不会发明约束，因为(x ~ y) => M x y与M x x不同。

根据您的实际用例，您可能需要阅读OverlappingInstances的文档。同样，根据你正在做的事情，最近在类型族中的一些创新，例如闭合类型族，可能是相关的。