Why does `forall (a :: j) (b:: k)` work differently than `forall (p :: (j,k))`?

Question

I'm trying to understand the difference between using forall to quantify two type variables and using forall to quantify a single type variable of tuple kind.

For example, given the following type families:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}

type family Fst (p :: (a,b)) :: a where
  Fst '(a,_) = a
type family Snd (p :: (a,b)) :: b where
  Snd '(_,b) = b
type family Pair (p :: (Type,Type)) :: Type where
  Pair '(a,b) = (a,b)

I can define an identity on pairs using two type variables, and get it to compile on GHC 8.0.1:

ex0 :: forall (a :: Type) (b :: Type). Pair '(a,b) -> (Fst '(a,b), Snd '(a,b))
ex0 = id

The same definition doesn't compile if I use a single type variable of tuple kind, however:

ex1 :: forall (p :: (Type,Type)). Pair p -> (Fst p, Snd p)
ex1 = id
-- Ex.hs:20:7: error:
--     • Couldn't match type ‘Pair p’ with ‘(Fst p, Snd p)’
--       Expected type: Pair p -> (Fst p, Snd p)
--         Actual type: (Fst p, Snd p) -> (Fst p, Snd p)
--     • In the expression: id
--       In an equation for ‘ex1’: ex1 = id
--     • Relevant bindings include
--         ex1 :: Pair p -> (Fst p, Snd p) (bound at Ex.hs:20:1)

Is the problem that p might be ⊥?

Answer 1

The reason is simply that there is no eta-conversion checking on the type-level. To begin with, there is no mechanism for distinguishing data definitions from single-constructor records/products which possibly have eta laws. I don't think p possibly being ⊥ is a valid reason for this. Even in partial lazy languages, eta equality for pairs holds (w.r.t. observational equivalence).

Answer 2

Is the problem that p might be ⊥?

More or less. Unfortunately, all kinds are inhabited by the empty type family.

type family Any :: k

Which frustrates any theory which would allow what you are trying to do. I think it really needs to be fixed; I'm not sure if there are any plans to do so, however.