| entirely so, since the result of it is not of type 'forall b. b', but | rather of 'forall b. C Int b => b'. Thus, if the C class has a function | which takes a 'b' as an argument, then this value does have use.

I disagree. Can you give an example of its use?

I believe something along the lines of the following would work:

class C a b | a -> b where { foo :: b -> String } instance C Int Int where { foo x = show (x+1) } x :: forall b. C Int b => b x = 5

(Supposing that the above definition were valid; i.e., we didn't get the type signature error, this reads that x has type "b" for all types "b" such that C Int b -- the fact that there is only one such type (due to the fun dep) is for us to know.) Then, we should be able to say:

foo x

and get "6".

From a "translation to untyped core" perpective (*grin*), we essentially replace class constraints with dictionaries. The definition of C introduces a dictionary like the following (I'm not 100% familiar with MPTC dictionaries, but I assume they're just like normal dictionaries):

data CDict a b = CDict (b -> String)

Then the instance will give us:

cIntIntDict :: CDict Int Int cIntIntDict = CDict (\x -> show (x+1))

foo will become:

foo (CDict foo_f) x = foo_f x

and if we apply this properly, we get: | foo cIntIntDict x | ==> (\ (CDict foo_f) x -> foo_f x) cIntIntDict x | ==> (\ (CDict foo_f) -> foo_f x) cIntIntDict | ==> (\x -> show (x+1)) x | ==> show (5+1) | ==> "6" or something like that? In fact, except for the type definition on x, this is actually a valid translation into typed core, I believe. The weird type on x is the only stumbling block, afaics. ...it is well known that I could be wrong though... - Hal