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

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.