FunDeps weaker than type families

I’ve just run into a situation where functional dependencies seem to propagate less type information than the corresponding type family. This seems to be related to the GHC feature request #4894. I just want to document here it for future reference.

The Data.Tuple.Select module in the tuple package has general methods for selecting elements from tuples. The Sel1class relates any tuple (up to a certain limit) to its first element (omitting the select method):

class Sel1 a b | a -> b

The instance for pairs looks as follows:

instance Sel1 (a,b) a

According to my understanding, the functional dependency of Sel1 should be equivalent to the following type function:

type family S1 a
type instance S1 (a,b) = a

If this is the case, the two constructors A and B in this data type should be equivalent

data AB a
  where
    A :: (Sel1 a b) => AB (a -> b)
    B :: (S1 a ~ b) => AB (a -> b)

Yet, the following example demonstrates that this is not the case:

data PairWitness a
  where
    PairWitness :: PairWitness (a,b)

test :: PairWitness a -> AB (a -> b) -> (a -> b)
test PairWitness A (a,b) = a
test PairWitness B (a,b) = a

This gives rise to a type error at the line matching on A. However, the B line works fine.

This has been tested with GHC 6.12.3 and GHC 7.0.2.

Download the source of this post (literate Haskell).