用类型相等约束修复的模糊类型变量

我正在研究一个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时代替。]

来源

2014-10-01 Itai Zukerman

我相信第二种形式是有效的，而第一种形式没有效果，因为在第二种形式中，您有'x〜x'的约束。然后这个约束可以让类型检查器找出'a〜Int'，而没有这个约束它只是看不到'Foo（Bar a）（Bar Int）'的实例。如果你使用第一种形式，然后有'z =（x :: Bar Int）> - > y'，它就编译。 – bheklilr 2014-10-01 17:31:27

编辑：本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'（大致），其中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的文档。再次取决于你在做什么，type families中的一些最近的创新如closed type families可能是相关的。

来源

2014-10-01 17:33:30

因此，这个答案和一些测试最终导致了启示：第一个实例只匹配类型相同而第二个匹配任何类型对的情况，但后来追加了类型相等约束。所以在第一种情况下，我可以在'Foo（Bar Char）（Bar Int）'上定义新的实例，但是在第二个这样的新实例中会发生冲突。你能否在你的回答中加入一些关于这个的东西？ – 2014-10-02 14:48:23

用类型相等约束修复的模糊类型变量

回答

相关问题