Which of these four statements is false?
newtype and data definitions could be replaced by type constructions of (->) and forall.RankNTypes is implemented correctly.ImpredicativeTypes would be hard to implement correctly even if GADTs didn't exist.Edit: I'm surprised that wasn't clear. data Maybe = Nothing | Just a could be written as type Maybe a = forall b. b -> (a -> b) -> b. data [] a = [] | a : [a] could be written as type [] a = forall b. b -> (a -> b -> b) -> b. (Compare to maybe and foldr.) The same thing ought to be possible for all newtype and data definitions, and is called continuation passing style (CPS).
As far as I know, type inference for types that have deeply nested foralls and (->) is implemented correctly by ghc using the RankNTypes extension, but ImpredicativeTypes, which allows foralls even in arguments to type constructors other than (->), is hopelessly broken.
But couldn't you implement ImpredicativeTypes by translating all data and newtype types to their CPS forms, using RankNTypes machinery for inference and then translating back into data/newtype forms?
None of them. The difficulty in using ImpredicativeTypes comes from not having type inference, requiring the user to provide explicit type signatures. You assume that since RankNTypes are widely used that type inference works in general for RankNTypes, but that's not true:
It is not possible to infer higher-rank types in general; type annotations must be supplied by the programmer in many cases.