GHC: Ticket #6002: GHC 7.4+ thinks class instance is incoherent, 7.0.4 disagrees
http://ghc.haskell.org/trac/ghc/ticket/6002
<p>
Load this file into GHCi:
</p>
<p>
<a class="ext-link" href="http://omega.googlecode.com/svn/mosaic/TypeMachinery.lhs?r=1086"><span class="icon"></span>http://omega.googlecode.com/svn/mosaic/TypeMachinery.lhs?r=1086</a>
</p>
<p>
With v7.4 (and HEAD) I get:
</p>
<pre class="wiki">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.
</pre><p>
With 7.0.4 all compiles (and runs) correctly.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/6002
Trac 1.0.1simonpjFri, 13 Apr 2012 08:26:50 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:1
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:1
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
This is a very delicate case.
Suppose we have these definitions.
</p>
<pre class="wiki"> data Nat a = ...
instance Show (Nat a) where ...
data Hidden a where
Hide :: Show (Nat a) => Nat a -> Hidden a
type family Plus m n :: *
plus :: Nat a -> Nat b -> Nat (Plus a b)
</pre><p>
and typecheck this function
</p>
<pre class="wiki"> f (Hide a) (Hide b) = Hide (plus a b)
</pre><p>
So we have
</p>
<pre class="wiki"> Given: d1 :: Show (Nat a1)
d2 :: Show (Nat a2)
Wanted: dw :: Show (Nat (Plus a1 a2))
</pre><p>
Now, if <tt>Plus a1 a2</tt> evaluated to <tt>a1</tt>, we would satisfy <tt>dw</tt> with d1; and similarly
if it evaluated to <tt>a2</tt>. Otherwise we should use the top-level instance.
</p>
<p>
The trouble is that it's hard to perform negative reasoning: we rightly refrain from
using the top level instance for <tt>Show (Nat a)</tt>, in case the <tt>(Plus a1 a2)</tt> <em>does</em> 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".
</p>
<p>
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.
</p>
<p>
I was going to say that a workaround is to use <tt>-XIncoherentInstances</tt>; but in fact
that does not currently work, although it should. I'll fix that part.
</p>
TicketheisenbugFri, 13 Apr 2012 09:25:32 GMT
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:2
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:2
<p>
I tried <tt>IncoherentInstances</tt> but the error message changed instead of disappearing.
</p>
<p>
I ask myself, how did this work in 7.0.4? Are we checking constraints more aggressively recently?
</p>
<p>
Also I have a user-defined kinds version here, maybe the inference logic would be simpler when no phantom types are involved? <a class="ext-link" href="http://omega.googlecode.com/svn/mosaic/TypeMachinery.kinds.lhs"><span class="icon"></span>http://omega.googlecode.com/svn/mosaic/TypeMachinery.kinds.lhs</a>
</p>
<p>
Thanks for looking into this!
</p>
TicketsimonpjFri, 13 Apr 2012 09:29:40 GMT
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:3
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:3
<p>
Reminder: I said "I was going to say that a workaround is to use <tt>-XIncoherentInstances</tt>; but in fact that does not currently work, although it should. I'll fix that part."
</p>
<p>
I don't know why 7.0.4 accepted it. But HEAD's rejection is for a good reason, as I explain above.
</p>
<p>
Nothing to do with phantom types; the issue here, as I say above, is what the type-function application <tt>(Plus a1 a2)</tt> might evaluate to.
</p>
Ticketsimonpj@…Fri, 20 Apr 2012 17:39:36 GMT
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:4
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:4
<p>
commit <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/6bf815982df88468035593a07b0be593d1326af2/ghc" title="Allow overlaps when -XIncoherentInstances is in force
This change allows ...">6bf815982df88468035593a07b0be593d1326af2</a>
</p>
<pre class="wiki">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(-)
</pre>
TicketsimonpjTue, 24 Apr 2012 11:16:49 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:5
http://ghc.haskell.org/trac/ghc/ticket/6002#comment:5
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>testcase</strong>
set to <em>polykinds/T6002</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
I've added a test that <tt>-XIncoherentInstances</tt> makes the code be accepted, so I'll close the ticket.
</p>
<p>
Simon
</p>
Ticket