#3584: type signature involving a type family rejected
----------------------------------------+-----------------------------------
Reporter: baramoglo | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.10.2
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Os: Unknown/Multiple
Architecture: x86 |
----------------------------------------+-----------------------------------
Changes (by simonpj):
* difficulty: => Unknown
Comment:
The problem is your instance for `Natural x`. You are saying "If you want
to prove `Natural x`, then please prove (`IsNegative x ~ False`)". Now in
the RHS of `add1`, GHC is faced with thee following problem:
{{{
From (Natural (m:+:n), -- From signature
Natural n, -- From first pattern match
Natural m) -- From second pattern match
please prove
Natural (m:+:n)
}}}
That seems easy enough, since the thing to prove is one of the premises.
But a possible reasoning step is to use the instance declaration first,
leading to
{{{
please prove
IsNegative (m:+:n) ~ False
}}}
which we obviously can't do. Your instance declaration promises an
alternative way to prove a constraint `(Natural ty)`, but one which turns
out to be a blind alley. But GHC does not ''search'' for a proof; it
follows just one path. (In general the search could be very complicated.)
Nevertheless, I think there is a bug here: GHC should really ''not'' use
an instance declaration if there is any possibility that one of the local
premises might match, rather in the same way that it refrains from
committing to one instance if more than one matches. Thanks for pointing
this out.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3584#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
