explicitly quantified classes in functions

[David Feuer]

On Thu, Apr 04, 2002, Hal Daume III wrote:
> Why can I not define the following (in ghc):
> 
> > class Foo p where
> > instance Foo Double where
> > foo :: Double -> (forall q . Foo q => q)
> > foo p = p
> 
> >From my humble (lack of) knowledge, there seems to be nothing wrong here,
> but ghc (5.03) complains about unifying q with Double.  I *can* write:


I believe that ghc translates the signature above to

foo :: forall q . Foo q => Double -> q

(I don't understand why GHC does this... it seems to have more potential
for confusion)

This should more clearly show that foo is required to take a Double and
give, in return, anything in class Foo that is requested, which it
certainly does not (it always returns a Double).  

> 
> > class Foo p where
> > instance Foo Double where
> > data T = forall q . Foo q => T q
> > foo :: Double -> T
> > foo p = T p
> 
> which is very similar, except that the explicit universal quantification
> is happening in in the datatype and not the function type.

Actually, this is not really universal quantification, it is existential
quantification.  If you actually wrote a datatype that did universal
quantification, it wouldn't work either:

data T = T (forall q . Foo q => q)

(I think this can also be written  data T = T (Foo q => q)  but I don't
remember for sure).

David