# 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 #-}
```

+3

source to share

No one has answered this question yet

Check out similar questions:

eleven