Opened 6 years ago

Closed 5 years ago

## #6002 closed bug (fixed)

# GHC 7.4+ thinks class instance is incoherent, 7.0.4 disagrees

Reported by: | heisenbug | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 7.4.1 |

Keywords: | Cc: | ||

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | GHC rejects valid program | Test Case: | polykinds/T6002 |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

Load this file into GHCi:

http://omega.googlecode.com/svn/mosaic/TypeMachinery.lhs?r=1086

With v7.4 (and HEAD) I get:

GHCi, version 7.5.20120410: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling TypeMachinery ( TypeMachinery.lhs, interpreted ) TypeMachinery.lhs:78:23: Overlapping instances for Show (Nat' (Plus n n1)) arising from a use of `Hide' Matching instances: instance Show (Nat' a) -- Defined at TypeMachinery.lhs:24:3 There exists a (perhaps superclass) match: from the context (Show (Nat' n)) bound by a pattern with constructor Hide :: forall (a :: * -> *) n. Show (a n) => a n -> Hidden a, in an equation for `+' at TypeMachinery.lhs:78:5-10 or from (Show (Nat' n1)) bound by a pattern with constructor Hide :: forall (a :: * -> *) n. Show (a n) => a n -> Hidden a, in an equation for `+' at TypeMachinery.lhs:78:14-19 (The choice depends on the instantiation of `n, n1' To pick the first instance above, use -XIncoherentInstances when compiling the other instance declarations) In the expression: Hide In the expression: Hide $ plus a b In an equation for `+': (Hide a) + (Hide b) = Hide $ plus a b Failed, modules loaded: none.

With 7.0.4 all compiles (and runs) correctly.

### Change History (5)

### comment:1 Changed 6 years ago by

difficulty: | → Unknown |
---|

### comment:2 Changed 6 years ago by

I tried `IncoherentInstances`

but the error message changed instead of disappearing.

I ask myself, how did this work in 7.0.4? Are we checking constraints more aggressively recently?

Also I have a user-defined kinds version here, maybe the inference logic would be simpler when no phantom types are involved? http://omega.googlecode.com/svn/mosaic/TypeMachinery.kinds.lhs

Thanks for looking into this!

### comment:3 Changed 6 years ago by

Reminder: I said "I was going to say that a workaround is to use `-XIncoherentInstances`

; but in fact that does not currently work, although it should. I'll fix that part."

I don't know why 7.0.4 accepted it. But HEAD's rejection is for a good reason, as I explain above.

Nothing to do with phantom types; the issue here, as I say above, is what the type-function application `(Plus a1 a2)`

might evaluate to.

### comment:4 Changed 5 years ago by

commit 6bf815982df88468035593a07b0be593d1326af2

Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Fri Apr 13 12:54:44 2012 +0100 Allow overlaps when -XIncoherentInstances is in force This change allows a top-level instance to be used even if there is a (potentially) overlapping local given. Which isn't fab, but it is what IncoherentInstances is *for*. This fixes the bug part of Trac #6002. compiler/typecheck/TcInteract.lhs | 18 ++++++++++-------- 1 files changed, 10 insertions(+), 8 deletions(-)

### comment:5 Changed 5 years ago by

Resolution: | → fixed |
---|---|

Status: | new → closed |

Test Case: | → polykinds/T6002 |

I've added a test that `-XIncoherentInstances`

makes the code be accepted, so I'll close the ticket.

Simon

**Note:**See TracTickets for help on using tickets.

This is a very delicate case. Suppose we have these definitions.

and typecheck this function

So we have

Now, if

`Plus a1 a2`

evaluated to`a1`

, we would satisfy`dw`

with d1; and similarly if it evaluated to`a2`

. Otherwise we should use the top-level instance.The trouble is that it's hard to perform negative reasoning: we rightly refrain from using the top level instance for

`Show (Nat a)`

, in case the`(Plus a1 a2)`

doeslater evaluate, and it's hard to get to the point where we say "ok, it definitely doesn't evaluate to a1 or a2, so use the top-level instance".I'm not sure how to "fix" this; it does seem tricky to solve type class constraints coherently, in the presence of (a) existentials and (b) type functions.

I was going to say that a workaround is to use

`-XIncoherentInstances`

; but in fact that does not currently work, although it should. I'll fix that part.