The type of id is universally quantified, that's why the free theorem holds. If it was id :: Typeable a => a -> a then it could inspect the type representation and do something different if it's an Int or whatever, but in this case the theorem is different from ∀a. a → a. The Wadler paper goes in greater length about why the universal quantification holds.

Also the computer can't, at runtime, introspect what you typed due to erasure (i.e. the types are erased at runtime) which is part of proper parametricity.