| I have been playing with ghc6.8.1 and type families and the following | program is accepted without any type-checking error: Martin's comments are spot on. FWIW, in the HEAD -- as Stefan says, type families are not *supposed* to work in 6.8.1 -- your program gives TF.hs:9:7: Couldn't match expected type `a' against inferred type `b' `a' is a rigid type variable bound by the type signature for `c' at TF.hs:8:7 `b' is a rigid type variable bound by the type signature for `c' at TF.hs:8:15 Expected type: a :=: b Inferred type: b :=: b In the expression: Eq In the definition of `c': c Eq = Eq That's fair enough. If you change K to be a 'data family', then decomposition works, and the program compiles. Bugs in type families against the HEAD are, as Don says, highly welcome. Simon