Ways around impredictive polymorphism

I'm new to some of the more complicated type constructs in Haskell, and have been messing around. I'm currently stuck trying to get a function that I think should work to type check.

Take the following code as an example:

{-# LANGUAGE RankNTypes   #-}
{-# LANGUAGE TypeFamilies #-}

class X a where
  data Y a
  z :: Y a -> Int

data D1 = D1
instance X D1 where
  data Y D1 = YD1
  z _ = 1

data D2 = D2
instance X D2 where
  data Y D2 = YD2
  z _ = 2

sumZ :: X a => [Y a] -> Int
sumZ = foldl' sumFn 0
  where sumFn = flip ((+) . z)

I want a = sumZ [YD1, YD2] to type check. This (obviously) doesn't work since the a type variable gets fixed with the first YD1.

I understand enough to know that I should probably use higher ranked types here, so I tried this:

sumZ' :: [(forall a. X a => Y a)] -> Int
sumZ' = foldl' sumFn 0
  where sumFn = flip ((+) . z)

But, when I try and compile it I run into "impredicative polymorphism":

     • Illegal polymorphic type: forall a. X a => Y a
       GHC doesn't yet support impredicative polymorphism
     • In the type signature: sumZ' :: [(forall a. X a => Y a)] -> Int
    |
 48 | sumZ' :: [(forall a. X a => Y a)] -> Int
    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

After doing a bit of reading, I see that the conventional solution is to wrap the value in a newtype to skirt around the impredicative polymorphism.

newtype Wrap = Wrap { unWrap :: forall a. X a => Y a }

sumZ'' :: [Wrap] -> Int
sumZ'' = foldl' sumFn 0
  where
    sumFn acc (Wrap v) = acc + (z v)

Unfortunately, this doesn't seem to work either. Compilation fails with this message:

     • Ambiguous type variable ‘a0’ arising from a use of ‘z’
       prevents the constraint ‘(X a0)’ from being solved.
       Probable fix: use a type annotation to specify what ‘a0’ should be.
       These potential instances exist:
         instance X D1
           -- Defined at ...
         instance X D2
           -- Defined at ...
     • In the second argument of ‘(+)’, namely ‘(z v)’
       In the expression: acc + (z v)
       In an equation for ‘sumFn’: sumFn acc (Wrap v) = acc + (z v)
    |
 64 |     sumFn acc (Wrap v) = acc + (z v)
    |                                 ^^^

Finally, my question(s):

Why doesn't the standard "wrapping" technique work in this case? When inspecting the type of v I see that it has the type forall a. X a => Y a, to me this seems like it should work.
How can I get the a = sumZ [YD1, YD2] to work? Am I going about this wrong?

Solution

The fact that v :: forall a. X a => Y a is exactly why applying z doesn't work.

That forall in there means that v can be of any type, you choose which one. To illustrate, compare to this:

empty :: forall a. [a]
empty = []

There value empty can be of any type, the consumer chooses which type. That's what forall means here. I hope this much is obvious.

And so it is with your value v: it can be of any type, you choose which. But in your code you don't choose a type: you're applying z, which itself can work with any type, and so the type of v remains unchosen. This is exactly what the compiler is telling you when it complains about the "ambiguous type variable a0".

To make this work, you should put the forall on the other side of Wrap:

data Wrap = forall a. X a => Wrap (Y a)

(you'll need to enable the GADTs extension for this to be allowed)

This way, whoever constructs a Wrap has to choose the specific type a. And on the other side, when you do pattern matching, you get the type a that was chosen by whoever constructed the value.