This is a tricky one. The motivating example is this: -- Overlapping instances instance Show a => Show [a] where ... instance Show Char where ...
data T where MkT :: Show a => [a] -> T f :: T -> String f (MkT xs) = show xs ++ "\n" Here it's clear that the only way to discharge the (Show [a]) constraint on 'x' is with the (Show a) dictionary stored inside the MkT. Yet doing so means ignoring the possibility that a=Char. So, for example, if we go h = case MkT "boo" of MkT xs -> show xs ++ "\n" we'll get the output string "['b','o','o']", not "boo". So yes, that's incoherent, in the sense that if we did the case-elimination we'd get (show "boo" ++ "\n"), and that would give a different result. Why does GHC have this behaviour? Because in the case of type signature, such as g :: [a] -> String g xs = show xs ++ "\n" we can change g's type signature to make it compile without having to choose which instance to use: g :: Show [a] => [a] -> String But with an existential type there is no way we can alter 'f' to make it work; it's the definition of T that would have to change. So I can't say it's perfect, but it seems too much of a Big Hammer to say IncoherentInstances for f. Anyway, that's the rationale. Simon | -----Original Message----- | From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Dan Doel | Sent: 03 February 2010 03:08 | To: glasgow-haskell-users@haskell.org | Subject: Overlapping Instances + Existentials = Incoherent Instances | | 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 | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users