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

Ryan Ingram ryani.spam at gmail.com
Fri Nov 30 18:01:12 EST 2007

```It seems you've already figured this out, but here's a quick counterexample:

> {-# LANGUAGE ExistentialQuantification, RankNTypes #-}
> module Box where
> data Box = forall a. B a
>
> --mapBox :: forall a b. (a -> b) -> Box -> Box -- incorrect type
> mapBox f (B x) = B (f x)

then:

> boxedInt :: Box
> boxedInt = B (1 :: Int)

> f :: [Int] -> Int
> f = sum

mf :: Box -> Box
mapBox f -- this is well-typed according to the specified type of "mapBox"

But,
mf boxedInt :: Box

mf boxedInt
= mapBox f boxedInt
= mapBox sum (B (1 :: Int))
= B (sum (1 :: Int))
which is not well-typed.

The least specific type for MapBox is

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

There are non-bottom functions of this type, for example:
const (1 :: Int) :: forall a. a -> Int

With this type,

> ok :: Box
> ok = mapBox (const 1) (B "hello")

is well-typed.

-- ryan

On 11/30/07, Pablo Nogueira <pirelo at googlemail.com> wrote:

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