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

[Pablo Nogueira]

Stupid of me:

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

The proof outlined is that of (forall a. a -> a) -> Box -> Box, my apologies.
We have to prove a universally quantified formula and that requires
forall-introduction. If someone has the proof in the tip of their
fingers, I'm grateful if you could let me know.