Incoherent instances without -XIncoherentInstances

Consider the following 4 modules:

{-# LANGUAGE GADTs #-}

module A where

data One = One

data ShowInstFor a = Show a => MkSIF

incoherent :: ShowInstFor One -> ShowInstFor One -> String
incoherent MkSIF MkSIF = show One

module B where

import A

instance Show One where
  show _ = "from module B"

fromB :: ShowInstFor One
fromB = MkSIF

module C where

import A

instance Show One where
  show _ = "from module C"

fromC :: ShowInstFor One
fromC = MkSIF

module D where

import A
import B
import C

oops1 = incoherent fromB fromC
oops2 = incoherent fromC fromB

According to ghci, oops1 is "from moduleB" and oops2 is "from module C". This seems bad.

Trac metadata

Trac field	Value
Version	7.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #7296

changed weight to 5

added Tbug Trac import labels

Attached file incoherent.tgz (download).

Files that produced the problem

It's not clear where the error is among these files. Here are arguments for or against various places:

1. The error is the definition of ShowInstFor. Packaging up an instance may be awkward, but I think it's useful enough not to ban outright.
2. The error is the definition of incoherent. This function has access to multiple instances of the same type, so how is it to choose among them? But, by making this definition an error, we potentially rule out various desirable programs that operate over datatypes that package instances. Because there's no way to pattern-match on a constructor without making the instance available, these program would become very awkward to write.
3. The error is in the type of fromB. It could be argued that the type of fromB should be Show One => ShowInstFor One, thus requiring a coherent instance for Show One at any use of fromB. This seems awkward, and makes the new, constructor-based constraints feel like the old, stupid, datatype-based constraints.
4. The error is in the import statements of module D. We could prohibit importing two modules that export conflicting instances. But, that would cause interoperability problems between different modules/packages that define overlapping instances. And, without a way to control instance import / export, it would be impossible to rectify this problem.
5. There is no error here, just a silly programmer. I find this dissatisfying, because it is reasonable for a programmer to assume coherence of instances. Yes, this program is silly, indeed, but I feel like dismissing it is somehow weakening Haskell's claim to offer coherence unless the programmer uses "dangerous" extensions, like OverlappingInstances or IncoherentInstances.
6. This is a feature, not a bug. We could say that the program above behaves as expected. If this is the case, we need to document the behavior and then maintain it, which I don't think will be particularly easy.

So, what to do? I don't honestly know! It may perhaps be best to let sleeping dogs lie (essentially, option 5), but I wanted to document the problem. I should also note that, in GHC 7.8, this becomes much more apparent, because Coercible allows you to do this in just one module! To wit:

{-# LANGUAGE GADTs #-}

module G where

import GHC.Exts

data One = One
instance Show One where
  show _ = "datatype One"

newtype Two = MkTwo One
instance Show Two where
  show _ = "datatype Two"

data ShowInstFor a = Show a => MkSIF

showOne :: ShowInstFor One
showOne = MkSIF

showTwo :: ShowInstFor Two
showTwo = coerce showOne

incoherent :: ShowInstFor Two -> String
incoherent MkSIF = show (MkTwo One)

GHCi reports that incoherent showTwo is "datatype One" and incoherent MkSIF is "datatype Two". Yikes!

It might also be worth noting that HEAD produces the opposite output on the original program from 7.6.3 -- the B and C are reversed in the output.

I might be missing something important, but it seems to me that the answer is very obviously 4. I'm not familiar with the precise language of the standard, but I always understood the rule to be very simple: "thou shalt have no more than one instance of a class for a type in thy program". We're blatantly violating this rule, the question is why GHC is not catching us. I think the answer is that you've come up with a way to distinguish GHC's lazy checking of instance overlap from other compilers' eager checking, to GHC's detriment. There's no use of a Show One instance in D, so GHC doesn't bother to investigate it. If overlap were checked eagerly at imports instead of lazily at use sites, the error would be caught.

Obviously there must be a reason why GHC does lazy rather than eager checking (and I think it might have something to do with Overlapping- and IncoherentInstances?), but I don't know the specifics. What would break if overlap checking were eager?

We could prohibit importing two modules that export conflicting instances. But, that would cause interoperability problems between different modules/packages that define overlapping instances.

Do you mean overlapping instances using OverlappingInstances, or without it? In the latter case I think it's the absence of interoperability problems that should count as a bug.

In my comment, I was referring to overlapping instances from modules that ''don't'' use OverlappingInstaces. Here's how I can see it happening:

• Suppose package dayta exports a datatype T and package klass exports a class C.
• Now, packages a and b both import T and C from their respective packages and define an instance C T.
• Package c wants to use the relevant modules from both a and b. Disaster with eager checking of overlap.

I've used packages here instead of modules to emphasize that the authors of all of these parts may be different. From a technical standpoint, replacing "package" with "module" would also work here.

I should say I'm not really disagreeing with illissius about eager checking, just drawing out the example of where this might be a problem. I find it very hard to come up with an opinion on this issue that I would feel comfortable defending!

GHC has allowed multiple instances for the same type and class to coexist in a single program for a long time without any fancy language features. See discussion at #2356.

Trac metadata

Trac field	Value
Related	→ #2356

mentioned in issue #9701

Only looking at the title, is this a duplicate of #7296?

No, #7296 is unrelated. This ticket is all about GHC's lazy overlap check, while #7296 is a puzzling behavior introduced by considering overlap differently when type-checking an instance method.

added Pnormal label