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

1. GHC 7.8.X isn't released yet so it's a bit early to call it a bug 2. Are you sure closed type families are going to be the default and not require any sort of flag or pragma? — Thomas M. DuBuisson
I just asked Richard Eisenberg about this a week ago, see the comments at the bottom here. I'm also really excited about the potential there. I sketched out on paper the mechanics of how I think inference should work, and am slowly working myself up to the idea of trying to get into hacking GHC, but TBH I'm not confident that will happen in any reasonable time frame. — jberryman
@ThomasM.DuBuisson: We do not know yet, but since this feature is available in GHC 7.7 we can test it and concider some of its behaviours as bugs or not. GHC 7.8 should be released soon I think. — Wojciech Danilo

mgampkay mgampkay · Accepted Answer · 2013-12-23T07:23:34

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"

Closed type families and type inference in Haskell

1 Answers