If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack. For example:
newtype List t = List (forall r. r -> (t -> r -> r) -> r) unList :: List t -> (forall r. r -> (t -> r -> r) -> r) unList (List f) = f
Is (I think) equivalent to System-F omega:
List = \t. forall r. r -> (t -> r -> r) -> r
Except you have to call
unList at the right moments.
Does this language with newtypes have more computation strength than System-F, equal to System-F omega?