On Mon, 3 Dec 2007, Simon Peyton-Jones wrote:
No, you didn't miss anything. I wouldn't expect anyone to write these types directly. But it can happen:
class C a b | a->b instance C Int Bool
class D x where op :: forall y. C x y => x -> y
instance D Int where op = ...
In the (D Int) instance, what's the type of op? Well, it must be op :: forall y. C Int y => Int -> y
And here we know that y=Bool; yet since we don't write the type sig directly we can't say it. So GHC's implementation of fundeps rejects this program; again it can't be translated into System F.
Conveniently, this is a good example of my other problem with fundeps :-) I can work around the problem from my first email with an unsafeCoerce, but is there any way I can get around the issue above at the moment in either 6.8 or the HEAD? I actually plan to recast the code in question using associated type synomyms once they're working properly, but would like to be able to make some progress now. Cheers, Ganesh