# 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 Rank2Types            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE PolyKinds             #-}
```