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

Pablo Nogueira pirelo at googlemail.com
Fri Nov 30 07:20:16 EST 2007

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

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.

More information about the Haskell-Cafe mailing list