[Haskell-cafe] handling rank 2 types

[Andrew Pimlott]

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#universal-quantification