dyokomizo

In GHC the features are much more well-defined and bite-sized. If you ignore them you still have a very complete, usable and impressive language.

[edit s/less well/more well/]

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.