The definition is irrelevant, so I removed it.

To make it easier to reason about, I'm going to rename the second map to map'.  It means the same thing, but this is just so we can talk about each "instance" of it clearly.  Now I'm going to rename the free variables:

map :: (a -> b) -> [a] -> [b]

map' :: (c -> d) -> [c] -> [d]

-> is right-associative, so I'll add the implied parentheses:

map :: (a -> b) -> ([a] -> [b])

map' :: (c -> d) -> ([c] -> [d])

Whenever we have an application like f x, if f has type a -> b and x has type a, then f x has type b.

So map map' says that (a -> b) should be unified with the type of map', and then the type of the result will be ([a] -> [b]).  So the equation is:

a -> b  =  (c -> d) -> ([c] -> [d])

Which implies

a = c -> d

b = [c] -> [d]

That's as far as we can go with the unification, so the result will be [a] -> [b].  Substituting, we have [c -> d] -> [[c] -> [d]].

Does that help?  What I have done is more-or-less the Hindley-Milner type inference algorithm.

Luke