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

这里的问题在于 PolyKinds pragma。没有它它也能很好地工作。我可能需要它以便我可以写作

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

一切顺利。

现在原因已经清楚了。类型族 (==) 没有多类实例(详细解释了为什么不提供此类实例 here )，因此我们无法减少所有相等性。所以我们需要指定一种。