#6002: GHC 7.4+ thinks class instance is incoherent, 7.0.4 disagrees
---------------------------------+------------------------------------------
Reporter: heisenbug | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid program
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Changes (by simonpj):
* difficulty: => Unknown
Comment:
This is a very delicate case.
Suppose we have these definitions.
{{{
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)
}}}
and typecheck this function
{{{
f (Hide a) (Hide b) = Hide (plus a b)
}}}
So we have
{{{
Given: d1 :: Show (Nat a1)
d2 :: Show (Nat a2)
Wanted: dw :: Show (Nat (Plus a1 a2))
}}}
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6002#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
