Closed type families and type inference in Haskell

Question

In GHC-7.7 (and 7.8) closed type families were introduced:

A closed type family has all of its equations defined in one place and cannot be extended, whereas an open family can have instances spread across modules. The advantage of a closed family is that its equations are tried in order, similar to a term-level function definition

I want to ask you, why the following code does not compile? GHC should be able to infer all the types - GetTheType is defined only for type X and if we comment out the marked line, the code compiles.

Is this a bug in GHC or closed type families does not have such optimizations YET?

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"

And the error is:

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

There's nothing wrong with closed type families. The problem is that not all type functions are injective.

Say, you could have this closed type function：

data X = X
data Y = Y

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

you can't infer the argument type from the result type X.

Data families are injective, but not closed:

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