Good signatures and typical families

Question

I expect

type family Rep a

and

type family Rep :: * -> *

to be the same, but it seems that 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

I just stumbled upon a Haskell extension error, or is there any indication of this behavior?

Answer 1

Yes, there is a subtle difference.

Roughly speaking, type family F a :: *->*it states that, for example, F Intis a type constructor injective type [], Maybe. This is used by the compiler, which can enter the verification code for 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 check the type above, the compiler used the fact that F Int a ~ F Int bmeans a ~ bthat follows from injectivity.

type family F a b :: * F Int, .

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