Dlaczego kompilator nie mógł dopasować typu "a == a" z "True" dla rodziny typów?

Question

Czy jest jakiś powód, dlaczego ten kod nie jest kompilowany:

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 

z błędem:

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

ale jeśli mogę zmienić definicję rodziny typ do

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

jest kompilowany dobrze?

(ghc-7.10.3)

Answer 1

W związku z prośbą o całkowitym przykład roboczego od Daniel Wagner, znalazłem odpowiedź.

Kompletny przykład najpierw:

{-# 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 

Problemem tutaj jest z PolyKinds Pragma. Bez niego działa dobrze. I prawdopodobnie trzeba go tak, że mogę napisać

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

i wszystko idzie dobrze.

Powód jest teraz jasny. Rodzina typów (==) nie ma instancji typu poly-kinded (szczegóły wyjaśniające, dlaczego takie przykłady nie zostały dostarczone here), więc nie możemy zmniejszyć wszystkich równości. Musimy więc określić rodzaj.