Geschlossene Familien und Typinferenz in Haskell

Question

In GHC-7.7 (und 7.8) geschlossen Familien Typ eingeführt wurden:

Eine geschlossene Familie an einem Ort alle seine Gleichungen definiert hat und nicht verlängert werden kann, während eine offene Familie kann Instanzen über Module verteilt haben. Der Vorteil einer geschlossenen Familie ist, dass seine Gleichungen um, ähnlich einem Begriff Ebene Funktionsdefinition

versucht werden möchte ich Sie fragen, warum der folgende Code kompiliert nicht? GHC sollte in der Lage sein, auf alle Typen zu schließen - GetTheType ist nur für den Typ X definiert, und wenn wir die markierte Zeile auskommentieren, wird der Code kompiliert.

Ist dies ein Fehler in GHC oder geschlossenen Typ Familien hat solche Optimierungen noch nicht?

Code:

{-# LANGUAGE TypeFamilies #-} 

data X = X 

type family GetTheType a where 
    GetTheType X = X 

class TC a where 
    tc :: GetTheType a -> Int 

instance TC X where 
    tc X = 5 

main = do 
    -- if we comment out the following line, the code compiles 
    let x = tc X 
    print "hello" 

Und der Fehler ist:

Couldn't match expected type ‛GetTheType a0’ with actual type ‛X’ 
The type variable ‛a0’ is ambiguous 
In the first argument of ‛tc’, namely ‛X’ 
In the expression: tc X 

Answer 1

Es ist nichts falsch mit geschlossenen Typ Familien. Das Problem ist, dass Typfunktionen nicht injektiv sind.

Sag mal, könnten Sie diese geschlossene Funktion haben:

data X = X 
data Y = Y 

type family GetTheType a where 
    GetTheType X = X 
    GetTheType Y = X 

Sie X das Argument Typ aus dem Ergebnistyp nicht ableiten kann.

Daten Familien sind injektiv, aber nicht geschlossen:

{-# LANGUAGE TypeFamilies #-} 

data X = X 

data family GetTheType a 

data instance GetTheType X = RX 

class TC a where 
    tc :: (GetTheType a) -> Int 

instance TC X where 
    tc RX = 5 

main = do 
    let x = tc RX 
    print "hello"