fundeps known beforehand (was RE: fundeps for extended Monad definition)

[Hal Daume III]

> Suppose we are in case 1.  Then the programmer has written a too-general
> type signature on f.  The programmer *must* know that b=Int in this case
> otherwise his function definition makes no sense.  However, I don't really
> see a reason why this should be an error rather than just a warning.  If
> some other module K imports both U and (for instance) I2, then we'll get a
> fundep clash and the whole program will be invalid.

I now retract this comment :).  Clearly this is just as bad as saying:

> f :: Bool -> b
> f x = x

since this claims that it will take a Bool and produce a value of type b
for all types b.  However, would it be all right to say (in
pseudo-Haskell):

> f :: exists b . Bool -> b
> f x = x

?

Here, we're simply claiming that there is *some* type b for which f takes
a Bool and produces a b?

I believe this same analysis extends to something like:

> class C a b | a -> b where {}
> instance C Int Int where {}
> f :: exists b . C Int b => Int -> b
> f i = i

It seems that this would be legal in a language like haskell but which
allowed existensial quantification.

Am I correct?