title: Why does `forall (a :: j) (b:: k)` work differently than `forall (p :: (j,k))`?
body: <p>I'm trying to understand the difference between using <code>forall</code> to quantify two type variables and using <code>forall</code> to quantify a single type variable of tuple kind.</p>
  
  <p>For example, given the following type families:</p>
  
  <pre><code>{-# 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)
  </code></pre>
  
  <p>I can define an identity on pairs using two type variables, and get it to compile on GHC 8.0.1:</p>
  
  <pre><code>ex0 :: forall (a :: Type) (b :: Type). Pair '(a,b) -&gt; (Fst '(a,b), Snd '(a,b))
  ex0 = id
  </code></pre>
  
  <p>The same definition doesn't compile if I use a single type variable of tuple kind, however:</p>
  
  <pre><code>ex1 :: forall (p :: (Type,Type)). Pair p -&gt; (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 -&gt; (Fst p, Snd p)
  --         Actual type: (Fst p, Snd p) -&gt; (Fst p, Snd p)
  --     • In the expression: id
  --       In an equation for ‘ex1’: ex1 = id
  --     • Relevant bindings include
  --         ex1 :: Pair p -&gt; (Fst p, Snd p) (bound at Ex.hs:20:1)
  </code></pre>
  
  <p>Is the problem that <code>p</code> might be <code>⊥</code>?</p>