Opened 3 years ago
Closed 3 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 Revisions: |
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 3 years ago by simonpj
- difficulty set to Unknown
comment:2 Changed 3 years ago by heisenbug
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 3 years ago by simonpj
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 3 years ago by simonpj@…
commit 6bf815982df88468035593a07b0be593d1326af2
Author: Simon Peyton Jones <[email protected]> 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 3 years ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to polykinds/T6002
I've added a test that -XIncoherentInstances makes the code be accepted, so I'll close the ticket.
Simon
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) does later 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.