haskell - 用类型相等约束固定的模棱两可的类型变量

Question

我正在开发一个单子(monad)流媒体库，但遇到了一个我不理解的类型。我设法将其简化为以下示例:

{-# 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 user guide section on instance resolution是一个很好的起点。

以下是如何分解为什么会发生这种情况。您的 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 的文档。 .再次取决于您正在做什么， type families 中的一些最新创新，如 closed type families , 可能是相关的。