Overlapping Instances + Existentials = Incoherent Instances

[Simon Peyton-Jones]

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-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
| 
| 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users