[Haskell-cafe] Re: Rigid type-var unification failure in
existentials used with parametrically polymorphic functions
pirelo at googlemail.com
Fri Nov 30 07:29:09 EST 2007
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.
More information about the Haskell-Cafe