explicitly quantified classes in functions

[John Hughes]

	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. 

Well, of course! The result has to have type (forall q . Foo q => q), but p
actually has type Double. Of course GHC complains.

The question is, why YOU think it is OK. And the answer is that you reason:
there is only one instance of Foo, so when I say Foo q, that means q must be
Double. But you're making the "closed world assumption", that you know all of
the instances of Foo. The compiler doesn't, and for good reason.

Suppose you were to export these definitions from the module where they
appear, into another module which defines

	instance Foo Integer

Now, of course, it should be OK to use Foo with the type Double -> Integer
(since Foo Integer holds in this context). Yet clearly, the *definition* you
gave cannot be used with this type. Hence the type is wrong.

Of course, you could argue that if the definition of foo is *not* exported,
then the compiler should use the closed world assumption and the program
should be accepted. But it would be really weird if whether a definition is
well-typed or not depended on whether or not it was exported...

John