| I am quite intrigued at the behaviour examplified in the attached module. | It's true I am a newbie and probably don't quite get the whole consequence | spectrum of -fallow-undecidable-instances, but why providing that dummy | instance (commented out) get the thing to compile? Sorry I must have missed this. It's a nice example of the trickiness of functional dependencies. Here's what is happening. First a very cut-down version of your example: class Concrete a b | a -> b where bar :: a -> String instance (Show a) => Concrete a b wib :: Concrete a b => a -> String wib x = bar x Now consider type inference for 'wib'. GHC figures out that the call of 'bar' gives rise to the constraint (Concrete p q), where x has type 'p'. Ah, but x must have type 'a', so the constraint is (Concrete a q). Now GHC tries to satisfy (Concrete a q) from (Concrete a b). If it applied improvement right away it'd succeed, but sadly it first looks at instances declarations. Success: we can get (Concrete a q) from (Show a). So it uses the instance decl and now we can't get (Show a) from (Concrete a b). OK, so you found that adding instance Concrete Bool Bool fixed the problem. That's weird isn't it? The reason is this. When GHC looks at the instance decls, it now sees *two* instance decls matching (Concrete a q), and so it declines for now to use either of them (since it's not clear which would be the right one). Once it has finished with instance decls it tries improvement. And, yes, it now sees that q=b, so all is well. You might say that GHC should use improvement more vigorously, and perhaps you'd be right. And indeed the upcoming GHC 6.8 does exactly that. But it's a great example of the delicacy of type inference in the presence of equalities. I'm going to add it to GHC's test suite! Simon