Data families seem not to be "surely apart" from anything
The following code is not compiling (GHC 7.10.2), it looks as if data families are not considered "surely apart" from any type, despite being injective.
{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}
type family Equals x y where
Equals x x = True
Equals x y = False
data Booly b where
Truey :: Booly True
Falsey :: Booly False
data family ID a
data instance ID Bool = IB
test :: Booly (Equals (ID Bool) Int)
test = Falsey
This gives the error
Test.hs:16:8: Warning:
Couldn't match type ‘Equals (ID Bool) Int’ with ‘'False’
Expected type: Booly (Equals (ID Bool) Int)
Actual type: Booly 'False
In the expression: Falsey
In an equation for ‘test’: test = Falsey
This gives no error with an ordinary type instead of a data family.
(Inspired and simplified from http://stackoverflow.com/questions/32733368/type-inequalities-in-the-presence-of-data-families#32733368.)