haskell - 为什么编译器无法将类型 'a==a' 与类型族的 '`True' 匹配？

Question

这段代码没有被编译是否有一些原因：

type family Foo a b :: Bool where
    Foo a b = a == b

foo :: Foo a b ~ True => Proxy a -> Proxy b
foo _ = Proxy

bar :: Proxy a -> Proxy a
bar = foo

有错误：

Couldn't match type ‘a == a’ with ‘'True’
Expected type: 'True
  Actual type: Foo a a

但是如果我将类型族定义更改为

type family Foo a b :: Bool where
    Foo a a = True
    Foo a b = False

它编译好了吗？

(ghc-7.10.3)

Answer 1

由于 Daniel Wagner 要求提供完整的工作示例，我找到了答案。

首先完整的例子：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
module Test where

import Data.Type.Equality(type (==))
import Data.Proxy(Proxy(..))

type family Foo a b :: Bool where
    Foo a b = a == b

foo :: Foo a b ~ True => Proxy a -> Proxy b
foo _ = Proxy

bar :: Proxy a -> Proxy a
bar = foo

这里的问题在于PolyKindspragma。没有它，它工作得很好。我可能需要它以便我可以写

bar :: Proxy (a :: *) -> Proxy a

一切顺利。

原因现在很清楚了。类型族 ( ==) 没有多类实例（详细解释了为什么此处未提供此类实例），因此我们不能减少所有等式。所以我们需要指定一种。