[Haskell-cafe] Rigid type-var unification failure in existentials used with parametrically polymorphic functions

[Pablo Nogueira]

A question about existential quantification:

Given the existential type:

  data Box = forall a. B a

in other words:

  -- data Box = B (exists a.a)
  -- B :: (exists a.a) -> Box

I cannot type-check the function:

mapBox :: forall a b. (a -> b) -> Box -> Box
--            :: forall a b. (a -> b) -> (exists a.a) -> (exists a.a)
mapBox f (B x) = B (f x)

Nor can I type check:

mapBox :: forall a. (a -> a) -> Box -> Box
--            :: forall a. (a -> a) -> (exists a.a) -> (exists a.a)
mapBox f (B x) = B (f x)

The compiler tells me that in both functions, when it encounters the
expression |B (f x)|, it cannot unify the  universally quantified |a|
(which generates a rigid type var) with the existentially quatified
|a| (which generates a different rigid type var) -- or so I interpret
the error message.

However, at first sight |f| is polymorphic so it could be applied to
any value, included the value hidden in  |Box|.

Of course, this works:

mapBox :: (forall a b. a -> b) -> Box -> Box
mapBox f (B x) = B (f x)

Because it's a tautology: given a proof of a -> b for any a or b I can
prove Box -> Box. However the only value of type forall a b. a -> b is
bottom.

This also type-checks:

mapBox :: (forall a. a -> a) -> Box -> Box
mapBox f (B x) = B (f x)

When trying to give an explanation about why one works and the other
doesn't, I see that, logically, we have:

  forall a. P(a) => Q  implies (forall a. P(a)) => Q   when a does not
occur in Q.

The proof in our scenario is trivial:

p :: (forall a. (a -> a) -> (Box -> Box)) -> (forall a. a -> a) -> Box -> Box
p mapBox f b = mapBox f b

However, the converse is not true.

Yet, could somebody tell me the logical reason for the type-checking
error? In other words, how does the unification failure translate
logically. Should the first mapBox actually type-check?

Isn't the code for  mapBox :: forall a. (a -> a) -> Box -> Box
encoding the proof:

  Assume forall a. a -> a
  Assume exists a.a
  unpack the existential, x :: a = T for some T
  apply f to x, we get (f x) :: a
  pack into existential,   B (f x) :: exists a.a
  Discharge first assumption
  Discharge second assumption

The error must be in step 3. Sorry if this is obvious, it's not to me right now.