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

[Pablo Nogueira]

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

I see, it's a case of not paying proper attention. I presume this will
reflect in the imposibility of introducing the forall when trying to
"prove" the type.

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

Indeed, I was just trying to play with unconstrained existentials.