Haskell Functor implied law

Question

Typeclassopedia says:

"A similar argument also shows that any Functor instance satisfying the first law (fmap id = id) will automatically satisfy the second law as well. Practically, this means that only the first law needs to be checked (usually by a very straightforward induction) to ensure that a Functor instance is valid."

If this is the case, why do we even mention the second functor law?

Law 1: fmap id = id Law 2: fmap (g . h) = (fmap g) . (fmap h) 

Answer 1

While I can't give a proof, I believe what this is saying is that due to parametricity, the type system enforces the second law as long as the first law holds. The reason to specify both rules is that in the more general mathematical setting, you might have some category C where it is perfectly possible to define a "mapping" from C to itself (i.e. a pair of endofunctions on Obj(C) and Hom(C) respectively) which obeys the first rule but fails to obey the second rule, and therefore fails to constitute a functor.

Remember that Functors in Haskell are endofunctors on the category Hask, and not even everything that would mathematically be considered an endofunctor on Hask can be expressed in Haskell... the constraints of parametric polymorphism rule out being able to specify a functor which does not behave uniformly for all objects (types) which it maps.

Based on this thread, the general consensus seems to be that the second law follows from the first for Haskell Functor instances. Edward Kmett says,

Given fmap id = id, fmap (f . g) = fmap f . fmap g follows from the free theorem for fmap.

This was published as an aside in a paper a long time back, but I forget where.