Identity function in Haskell has multiple inhabitants?

Question

In category theory it can be proven that the identity function is unique. It is also said that, reasoning with parametricity, that the type forall a. a -> a has only one inhabitant. In Haskell though I can think of more implementations of the identity function:

id x = x
id x = fst (x, "useless")
id x = head [x]
id x = (\x -> x) x
id x = (\x -> (\x -> x) x) x

How can I understand the statement "the identity function is unique" and "any function with type forall a. a -> a has only one inhabitant" when there are multiple implementations?

Answer 1

Those all look like the same single inhabitant to me. To show that they are different, try to construct an input for which they behave differently. If you cannot, they must in fact be the same function implemented differently.

Consider an analogue from a different discipline. In number theory, it can be proven that there is one unique smallest prime, namely 2. But how can this be? 10/5 is also the smallest prime, as is 1+1. It is possible for all of these statements to be true at once because 10/5 is in fact the same thing as 2, just as all the expressions you've written are the same thing as the identity function.

Answer 2

Those are different implementations of the same function. Thus there is no more then a single inhabitant here as this refers to the function, not to its implementation.