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 `Sel1`

class 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).

## No comments:

## Post a Comment