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

[Luke Palmer]

On Nov 30, 2007 12:20 PM, Pablo Nogueira <pirelo at googlemail.com> wrote:
> A question about existential quantification:
>
> Given the existential type:
>
>   data Box = forall a. B a
>
[...]
>
> 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)
>
> However, at first sight |f| is polymorphic so it could be applied to
> any value, included the value hidden in  |Box|.

f is not polymorphic here; mapBox is.

> Of course, this works:
>
> mapBox :: (forall a b. a -> b) -> Box -> Box
> mapBox f (B x) = B (f x)

Here f is polymorphic.

> 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.

Yes, but that is only because your Box type is trivial.  It can contain
any value, so you can never extract any information from it.

Let's detrivialize your box and see where that leads us:

data Box = forall a. (Num a) => B a

Then:

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

Should work fine, and there are functions which you can give to mapBox
which are not bottom.

Luke