Skip to content

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