fundeps help

[Manuel M T Chakravarty]

Jan-Willem Maessen:
> Is it really a good idea to permit a type signature to include  
> equality constraints among unifiable types?  Does the above type  
> signature mean something different from a ->a?  Does the type  
> signature:
>    foo :: (a~Bar b) => a -> Bar b
> mean something different from:
>    foo :: Bar b -> Bar b
> ?  I know that System FC is designed to let us write stuff like:
>    foo :: (Bar a ~ Baz b) => Bar a -> Baz b
> Which is of course what we need for relating type functions.  But  
> I'm wondering if there's a subtlety of using an equality constraint  
> vs just substitution that I've missed---and if not why there are so  
> many ways of writing the same type, many of them arguably unreadable!

Simon answered most of your question, but let me make a remark  
regarding "why there are so many ways of writing the same type, many  
of them arguably unreadable!"  Equalities of the form "a ~ someType"  
are essentially a form of let-bindings for types - you can give a type  
a name and then use the name in place of the type.  Just like with  
value-level let bindings, you can abuse the notation and write  
unreadable terms.  However, this is no reason to remove let-bindings  
from the value level, so why should it be different at the type level?

Manuel