Why don't all types expand?

Let's pretend that

type family F (x :: Nat) (y :: Nat) :: (Nat, Nat) where
  F x y = '(x, y)

      

        
        
        
      

    

then

:t Proxy :: Proxy '[ (F 1 2) ]
Proxy :: Proxy '[ (F 1 2) ] :: Proxy '['(1, 2)]

      

        
        
        
      

    

But now suppose that

type family ZipWith (f :: a -> b -> c) (as :: [a]) (bs :: [b]) :: [c] where
  ZipWith f (a ': as) (b ': bs) = (f a b) ': (ZipWith f as bs)
  ZipWith f as        bs        = '[]

:t Proxy :: Proxy (ZipWith F ('[1,2]) ('[3,4]))
Proxy :: Proxy (ZipWith F ('[1,2]) ('[3,4])) :: Proxy '[F 1 3, F 2 4]

      

        
        
        
      

    

Why not type

Proxy :: Proxy (ZipWith F ('[1,2]) ('[3,4])) :: Proxy '['(1, 3), '(2, 4)]

      

        
        
        
      

    

If I say

:t (Proxy :: Proxy (ZipWith F ('[1,2]) ('[3,4]))) :: Proxy '[ '(1, 3), '(2, 4)]

      

        
        
        
      

    

then I get an error like

    Couldn't match type ‘F’ with ‘'(,)’
Expected type: Proxy (ZipWith F '[1, 2] '[3, 4])
  Actual type: Proxy '['(1, 3), '(2, 4)]
In the expression:
    (Proxy :: Proxy (ZipWith F ('[1, 2]) ('[3, 4]))) ::
      Proxy '['(1, 3), '(2, 4)]

      

        
        
        
      

    

But F is' (,) so what's going on? Does it have something to do with injectivity?

EDIT in response to a comment that is indeed the answer:

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE PolyKinds             #-}