I am trying to use a rank 2 type to enforce a condition on a data structure. For the purpose of this message, I am trying to ensure that a list is empty (ignoring the possibility of bottom elements):

{-# OPTIONS -fglasgow-exts #-} import Control.Monad newtype Empty = Empty (forall a. [a])

I want a function

listToEmpty :: [v] -> IO Empty listToEmpty l = liftM Empty (mapM no l) where no :: a -> IO a' no x = fail "element found"

But this gives a "less polymorphic" error. I think the problem is that ghc will not instantiate the "a'" in "IO a'" as a higher-rank type because it occurs within a type contructor. I believe this is the restriction referred to at the end of 7.4.9[1]. If I instead write

uncheckedListToEmpty :: [v] -> Empty uncheckedListToEmpty l = Empty (map no l) where no :: a -> a' no x = error "element found"

it compiles, because "v'" can be instantiated as "forall v. Rule v", and even pass through map with the higher-rank type. Is there any way to make ghc accept the first definition? I found this workaround:

newtype Any = Any { unAny :: forall a. a } listToEmptyAny :: [v] -> IO Empty listToEmptyAny l = liftM (\l -> Empty (map unAny l)) (mapM no l) where no :: a -> IO Any no x = fail "element found"

But needing a newtype wrapper Empty was bad enough; do I really need one for every intermediate result (that is inside another type constructor) as well? I could probably define a generic family of wrappers

newtype Forall = Forall (forall a. a) newtype Forall1 c1 = Forall1 (forall a. c1 a) newtype Forall2 c1 c2 = Forall2 (forall a. c1 c2 a) ...

But I would still have to use them everywhere. Any other tricks? Andrew [1] http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#uni...