Data families can have unmatchable kinds
It turns out that this compiles:
data family DF :: Type ~> Type
λ> :kind DF
DF :: Type ~> Type
This a bit odd, considering that data family type constructors are supposed to be matchable. Moreover, if you try the plain data type equivalent of this:
data D :: Type ~> Type
Then GHC will rewrite ~> to -> behind the scenes:
λ> :kind D
D :: Type -> Type
I can't exhibit any unsound behavior from DF having an unmatchable kind, although you can do weird things with it (e.g., inject :: Id3 a :~: Id3 b -> a :~: b works). It does feel inconsistent to have the ~>--> rewriting behavior for plain data types but not for data families, however.
EDIT: That should read DF a :~: DF b -> a :~: b, not Id3 a :~: Id3 b -> a :~: b.
Edited by Ryan Scott