Opened 2 years ago

Last modified 9 months ago

#8338 new bug

Incoherent instances without -XIncoherentInstances

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #2356 Differential Revisions:

Description

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.

Attachments (1)

incoherent.tgz (395 bytes) - added by goldfire 2 years ago.
Files that produced the problem

Download all attachments as: .zip

Change History (7)

Changed 2 years ago by goldfire

Files that produced the problem

comment:1 Changed 2 years ago by goldfire

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.
  1. 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.
  1. 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.
  1. 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.
  1. 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.
  1. 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.

comment:2 Changed 23 months ago by illissius

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.

comment:3 Changed 23 months ago by goldfire

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!

comment:4 Changed 14 months ago by rwbarton

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.

comment:5 Changed 9 months ago by thomie

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

comment:6 Changed 9 months ago by goldfire

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.

Note: See TracTickets for help on using tickets.