This is supported by the parametricity theorem. That is a big word, but it boils down to this: let's say you wrote an identity function of type "a -> a", and it passed the type checker. Then it is correct: you simply can't do much with a value of type "a", because you don't know anything about it.
If an identity function is too simple, consider "compose :: (a -> b) -> (c -> a) -> (c -> b)". I think it can be proven that if you write an implementation that passes the type checker for this signature, the implementation is necessarily correct.
If an identity function is too simple, consider "compose :: (a -> b) -> (c -> a) -> (c -> b)". I think it can be proven that if you write an implementation that passes the type checker for this signature, the implementation is necessarily correct.