Kind signatures and Type families

Question

I expect

type family Rep a

and

type family Rep :: * -> *

to be the same, but it seems there is a difference

type family   Rep a
type instance Rep Int  = Char
-- ok

type family   Rep :: * -> *
type instance Rep Int  = Char
-- Expected kind * -> *, but got 'Int' instead

Have I simply stumbled over an Haskell extension bug, or is there some point to this behavior?

Answer 1

Yes, there is a subtle difference.

Roughly, type family F a :: *->* states that, say, F Int is an injective type constructor like [], Maybe. This is exploited by the compiler, which can type check the following code:

type family F a :: * -> *

-- these three examples can be removed / changed, if wished
type instance F Int = []
type instance F Char = Maybe
type instance F Bool = (,) String

foo :: (F Int a :~: F Int b) -> (a :~: b)
foo Refl = Refl

To type check the above, the compiler exploited the fact that F Int a ~ F Int b implies a ~ b, which follows from injectivity.

Instead, declaring type family F a b :: * does not ensure injectivity of F Int, since the following becomes legal.

type family F a b :: *
type instance F Int a = ()