We will give some strong evidence for the claim "natural transformations must treat their arguments opauely". This is the best I can come up with short of defining a lambda calculus with type-switch and showing that the type-switch can always be eliminated (which I suspect would be possible) but is too difficult. Instead, we show that the requirement that a function be a natural transformation is invariant under encodings -- that is, if you mangle the argument in whatever way you like, and unmangle the result, you get the same thing as if you didn't do any mangling.
Therefore, in order to a natural transformation t :: F a -> G a to make an "exception" for a type, it would have to
make the same exception for all possible encodings of that type as well. In particular, one possible encoding is to
encode each incoming a in F as a unique integer. The resulting integers in the result G value show us exactly
which as in the input go where in the output, and this mapping must remain consistent across types by the theorem h
ere. These integers, then, become the "variable names", which can not be manipulated in any way except for moved around opaquely.
The theorem is simple. Given
encode :: A -> B
decode :: B -> A
decode . encode = id -- notice we don't need the other direction
t :: F a -> G a
Naturality says
for any f, t . fmap f = fmap f . t
So:
fmap decode . t . fmap encode
= fmap decode . fmap encode . t
= fmap (decode . encode) . t
= fmap id t
= t