Greetings, I've actually known about this for a while, but while discussing it, it occurred to me that perhaps it's something I should report to the proper authorities, as I've never seen a discussion of it. But, I thought I'd start here rather than file a bug, since I'm not sure it isn't intended. Anyhow, here's the example: class C a where foo :: a -> String instance C a where foo _ = "universal" instance C Int where foo _ = "Int" bar :: a -> String bar x = foo x Now, normally bar generates a complaint, but if you enable IncoherentInstances, it's accepted, and it always generates "universal", even if called with an Int. Adding a 'C a' constraint to the type makes it give "Int" in the case of an Int. Now, IncoherentInstances is something most people would suggest you don't use (even people who are cool with OverlappingInstances). However, it turns out that ExistentialQuantification does the same thing, because we can write: data Ex = forall a. Ex a baz :: a -> String baz x = case Ex x of Ex x' -> foo x' and this is accepted, and always yields "universal", just like bar. So, things that you get out of an existential are allowed to make use of the general versions of overlapping instances if any fit. So, I never really regarded this as anything more than an oddity that's unlikely to come up. And it might be working as intended. But I thought perhaps I should ask: is this intended? One could probably build a case that baz should only be accepted if IncoherentInstances are enabled, since it's doing about the same thing. I'm not really sure how far back this behavior goes. I've probably known about it for several 6.X releases without mentioning it except as a fun party fact (apologies). Is this the way things are supposed to work? (And sorry if I just missed the discussion somewhere. I searched the trac and didn't see anything very promising.) Cheers, -- Dan