使用类型相等约束修复的歧义类型变量

Question

我正在研究一个monadic流媒体库,我遇到了一个我不理解的类型.我已设法将其减少到以下示例:

{-# 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'(大致)是typechecker以你的重写实例定义结束的地方:它看到了一个(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的文档.同样取决于你正在做什么,最近类型系列中的一些创新,例如封闭式系列,可能是相关的.