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
.