Overlapping Instances + Existentials = Incoherent Instances
simonpj at microsoft.com
Wed Feb 10 07:13:10 EST 2010
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.
| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Dan Doel
| Sent: 03 February 2010 03:08
| To: glasgow-haskell-users at haskell.org
| Subject: Overlapping Instances + Existentials = Incoherent Instances
| 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.)
| -- Dan
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
More information about the Glasgow-haskell-users