(+)    :: Int -> Int -> Int
even   :: Int -> Bool

head   :: [a] -> a
(++)   :: [a] -> [a] -> [a]
foldr  :: (a -> b -> b) -> b -> [a] -> b
map    :: (a -> b) -> [a] -> [b]
concat :: [[a]] -> [a]
(.)    :: (b -> c) -> (a -> b) -> a -> c

{-
We know that 
2, 3 :: Int 
so
[3, 2], [2] :: [Int].
Now,
(++) :: [a] -> [a] -> [a]
and 
[3, 2], [2] :: [Int]
so it follows that 
[3, 2] ++ [2] :: [a] with the constraint that a ~ Int.
That is,
[3 ,2] ++ [2] :: [Int].
Finally, 
head :: [a] -> a
and 
[3, 2] ++ [2] :: [Int]
implies that 
head ([3, 2] ++ [2]) :: a with the constraint that a ~ Int.
That is,
head ([3, 2] ++ [2]) :: Int 
-}

{-
We know that 
3 :: Int 
and 
(+) :: Int -> Int -> Int
Therefore,
(+) 3 :: Int -> Int
-}

{-
We know that 
map :: (a -> b) -> [a] -> [b]
and 
even :: Int -> Bool 
Therefore,
map even :: [a] -> [b] with the constraint that (a -> b) ~ (Int -> Bool)
That is, 
map even :: [a] -> [b] with the constraints that a ~ Int and b ~ Bool
That is,
map even :: [Int] -> [Bool]
-}

{-
We know that 
map :: (a -> b) -> [a] -> [b]
and 
concat :: [[c]] -> [c]  (note the fresh type variable we use here to avoid confusion!)
Therefore,
map concat :: [a] -> [b] with the constraint that (a -> b) ~ ([[c]] -> [c])
That is, 
map concat :: [a] -> [b] with the constraints that a ~ [[c]] and b ~ [c]
That is,
map concat :: [[[c]]] -> [[c]]
-}

{-
First, we note that
reverse . reverse
is syntactic sugar for 
(.) reverse reverse 
Seeing that function application associates to the left, this is equivalent to 
((.) reverse) reverse 
Let us syntactically distinguish the two copies of reverse as they might be instantiations of reverse at two different types and write
((.) reverse1) reverse2 

We know that 
(.) :: (b -> c) -> (a -> b) -> (a -> c)
reverse1 :: [d] -> [d]   (note the freshly chosen type variable d, to avoid confusion with existing type variables)
reverse2 :: [e] -> [e]   (again a fresh type variable e)

It therefore follows that 
reverse . reverse = ((.) reverse1) reverse2  :: a -> c with the constraints (b -> c) ~ ([d] -> [d]) and (a -> b) ~ ([e] -> [e])

Simplifying the constraints gives us that:
b ~ [d] 
c ~ [d] 
a ~ [e] 
b ~ [e] 
and therefore that 
[d] ~ [e]

We conclude:
reverse . reverse :: a -> c with constraints ... = [e] -> [e]
-}

{-
We know that 
foldr :: (a -> b -> b) -> b -> [a] -> b
and 
map :: (c -> d) -> [c] -> [d]  (note the fresh type variables we use here to avoid confusion!)
Therefore,
foldr map :: b -> [a] -> b with the constraint that (a -> b -> b) ~ ((c -> d) -> [c] -> [d])
That is, 
foldr map :: b -> [a] -> b with the constraints that a ~ (c -> d), b ~ [c] and b ~ [d]
That is,
foldr map :: b -> [a] -> b with the constraints that a ~ (c -> c) and b ~ [c] (because [c] ~ [d] implies that c ~ d)
That is,
foldr map :: [c] -> [c -> c] -> [c]
Up to renaming of bound type variables (which is irrelevant), this is answer 1.
-}

{-
We know that 
map :: (a -> b) -> [a] -> [b]   (we'll use the type variables a and b for the left copy of map)
and also 
map :: (c -> d) -> [c] -> [d]   (we'll use fresh type variables c and d for the right copy of map, to avoid confusion)
Therefore,
map map :: [a] -> [b] with the constraint that (a -> b) ~ ((c -> d) -> [c] -> [d])
That is, 
map map :: [a] -> [b] with the constraints that a ~ (c -> d) and b ~ [c] -> [d]     (note that -> associates to the right)
That is,
map map :: [c -> d] -> [[c] -> [d]]
-}

{-
We know that 
map :: (a -> b) -> [a] -> [b] 
and also (from the previous question)
map map :: [c -> d] -> [[c] -> [d]]   (note that we use fresh type variables to avoid confusion)
Therefore,
map (map map) :: [a] -> [b] with the constraint that (a -> b) ~ ([c -> d] -> [[c] -> [d]])
That is, 
map (map map) :: [a] -> [b] with the constraints that a ~ [c -> d] and b ~ [[c] -> [d]]
That is,
map (map map) :: [[c -> d]] -> [[[c] -> [d]]]
Up to (irrelevant) renaming of bound type variables this is answer 1.
-}