IncoherentInstances如何运作？

Question

玩一些代码:

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Arity f where
  arity :: f -> Int

instance Arity x where
  arity _ = 0

instance Arity f => Arity ((->) a f) where
  arity f = 1 + arity (f undefined)

没有IncoherentInstances:

ghci> arity foldr
blah blah ambiguous blah blah possible fix blah
ghci> arity (foldr :: (a -> Int -> Int) -> Int -> [a] -> Int)
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3
2

如果我们添加IncoherentInstances到pragma列表中,那么它可以处理foldr而不需要单态类型签名,但它在lambda上得到了错误的答案:

ghci> arity foldr
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3 -- should be 2
0

Incoherent Instances背后的黑魔法是什么？它为什么要做它在这里做的事情？

Answer 1

这很复杂.让我们从模棱两可的错误开始:

<interactive>:1:1:
    Ambiguous type variable `b0' in the constraint:
      (Arity b0) arising from a use of `arity'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: arity foldr
    In an equation for `it': it = arity foldr

通常,在没有重叠实例的情况下,当尝试将类型与类匹配时,它会将类型与该类的所有实例进行比较.如果只有一个匹配,它将使用该实例.过度使用,您将获得无实例错误(例如,带有show (*))或重叠实例错误.例如,如果OverlappingInstances从上述程序中删除语言功能,则会出现以下错误 arity (&&):

<interactive>:1:1:
    Overlapping instances for Arity (Bool -> Bool -> Bool)
      arising from a use of `arity'
    Matching instances:
      instance Arity f => Arity (a -> f)
        -- Defined at tmp/test.hs:9:10-36
      instance Arity x -- Defined at tmp/test.hs:12:10-16
    In the expression: arity (&&)
    In an equation for `it': it = arity (&&)

它匹配Arity (a -> f),如a能Bool和f可Bool -> Bool.它还匹配Arity x,如x可以Bool -> Bool -> Bool.

随着OverlappingInstances,当两个或多个实例可以匹配时面临的情况,如果有,将选择一个最特殊的一个.如果可以匹配,则X实例比实例更具体,但反之亦然.YXY

在这种情况下,(a -> f)匹配x但x不匹配(a -> f)(例如考虑x存在Int).所以Arity (a -> f)比具体更具体Arity x,因此如果两者匹配,前者将被选中.

使用这些规则,arity (&&)将首先匹配Arity ((->) a f),a存在Bool和f存在Bool -> Bool.下一场比赛将a是Bool和f布尔.最后它将结束Arity x与xBool的匹配.

注意上面的函数,(&&)结果是具体类型Bool.但是当类型不具体时会发生什么？例如,让我们看看结果arity undefined.undefined有类型a,所以它不是具体类型:

<interactive>:1:1:
    Ambiguous type variable `f0' in the constraint:
      (Arity f0) arising from a use of `arity'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: arity undefined
    In an equation for `it': it = arity undefined

你得到一个不明确的类型变量错误,就像foldr那样.为什么会这样？这是因为取决于什么a,将需要不同的实例.如果a是Int,Arity x则应匹配实例.如果a是Int -> Int,Arity ((->) a f)则应匹配实例.因此,ghc拒绝编译程序.

如果你注意到foldr:的类型foldr :: forall a b. (a -> b -> b) -> b -> [a] -> b,你会注意到同样的问题:结果不是具体的变量.

以下是其中IncoherentInstances的内容:启用该语言功能后,它将忽略上述问题,只选择一个始终与变量匹配的实例.例如arity undefined,Arity x将始终匹配a,因此结果将为0.类似的事情是为了完成foldr.

现在针对第二个问题,为什么arity $ \x y -> 3在IncoherentInstaces启用时返回0 ？

这是非常奇怪的行为.以下ghci会话将显示它有多奇怪:

*Main> let f a b = 3
*Main> arity f
2
*Main> arity (\a b -> 3)
0

这让我觉得ghc中有一个bug,\a b -> 3可以看到IncoherentInstances有类型x而不是a -> b -> Int.我想不出为什么这两个表达式不应该完全一样的原因.