Hello,

Consider the following:

data SimpExist a = SimpExist (forall x . x -> a) f :: SimpExist Bool f = SimpExist (const True) g = SimpExist id

What is the type of g? In a similar example, GHC tells me it is of type SimpExist c. Yet, I can't unify it with any other SimpExist c'.

Have you tried to type check this example (the "g")? It does not type check in my GHC. There are not many functions with the type "forall x . x -> a" when "a" is also polymorphic --- it is the type of unsafeCoerce.

It seems to me that this is something like exists x . SimpExist x, and is similar to:

data ExistWrap = forall a . ExistWrap (forall x . x -> a)

Sure, you should read a "forall" on the left side of a constructor as "exists". Look at section 7.4.1.4.1 of: http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html The design decision here was to avoid introducing a new "exist" construct. I believe that the justification for this option is that in Logic a "forall" in a contravariant position has the same effect as an existential. Cheers, Bruno