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