Warum konnte der Compiler den Typ 'a == a' nicht mit 'True' für die Typfamilie vergleichen?

Question

Gibt es einen Grund, warum dieser Code nicht kompiliert wird:

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 

mit Fehler:

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

aber wenn ich Typ Familie Definition

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

es kompiliert gut ändern?

(GHC-7.10.3)

Answer 1

Aufgrund einer Anfrage für ein komplettes Arbeitsbeispiel von Daniel Wagner, fand ich eine Antwort.

Komplettes Beispiel zuerst:

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

Das Problem hier ist mit PolyKinds Pragma. Ohne es geht es gut. Ich brauche es wahrscheinlich so, dass ich

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

schreiben und alles gut geht.

Der Grund ist jetzt klar. Die Typfamilie (==) hat keine poly-kinded Instanzen (Details, die erklären, warum solche Instanzen nicht zur Verfügung gestellt werden here), so dass wir nicht alle Gleichheiten reduzieren können. Also müssen wir eine Art angeben.