#1251: GADTs with newtype deriving can crash GHCi / cause Core Lint to fail
-------------------------------------------------+--------------------------
Reporter: Stefan O'Rear <[EMAIL PROTECTED]> | Owner:
Type: bug | Status: closed
Priority: normal | Milestone: 6.6.2
Component: Compiler | Version: 6.6
Severity: normal | Resolution: fixed
Keywords: | Difficulty: Unknown
Os: Linux | Testcase: gadt/CasePrune
Architecture: x86 |
-------------------------------------------------+--------------------------
Changes (by simonpj):
* resolution: => fixed
* testcase: => gadt/CasePrune
* status: new => closed
Comment:
Interesting bug. Turns out that GHC's optimiser was being to eager about
eliminating dead case branches. I've added a long comment to Unify.lhs,
reproduced below. Meanwhile, the bug is fixed in HEAD; won't be fixed in
6.6
Meanwhile, you are not justified in assuming that there is no non-bottom
value of type (II A). You can't construct one in normal Haskell, but you
can with newtype-deriving as you showed, and (more generally) you can in
GHC's intermediate lanuage FC. Use a data type you really want to be
sure.
Thank you for a nice example. newtype deriving is more powerful than I
thought!
Simon
{{{
Note [Pruning dead case alternatives]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider data T a where
T1 :: T Int
T2 :: T a
newtype X = MkX Int
newtype Y = MkY Char
type family F a
type instance F Bool = Int
Now consider case x of { T1 -> e1; T2 -> e2 }
The question before the house is this: if I know something about the type
of x, can I prune away the T1 alternative?
Suppose x::T Char. It's impossible to construct a (T Char) using T1,
Answer = YES (clearly)
Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
to 'Bool', in which case x::T Int, so
ANSWER = NO (clearly)
Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-
bottom)
value of type (T X) using T1. But *in FC* it's quite possible. The
newtype
gives a coercion
CoX :: X ~ Int
So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom
value
of type (T X) constructed with T1. Hence
ANSWER = NO (surprisingly)
Furthermore, this can even happen; see Trac #1251. GHC's newtype-deriving
mechanism uses a cast, just as above, to move from one dictionary to
another,
in effect giving the programmer access to CoX.
Finally, suppose x::T Y. Then *even in FC* we can't construct a
non-bottom value of type (T Y) using T1. That's because we can get
from Y to Char, but not to Int.
Here's a related question. data Eq a b where EQ :: Eq a a
Consider
case x of { EQ -> ... }
Suppose x::Eq Int Char. Is the alternative dead? Clearly yes.
What about x::Eq Int a, in a context where we have evidence that a~Char.
Then again the alternative is dead.
Summary
We are really doing a test for unsatisfiability of the type
constraints implied by the match. And that is clearly, in general, a
hard thing to do.
However, since we are simply dropping dead code, a conservative test
suffices. There is a continuum of tests, ranging from easy to hard, that
drop more and more dead code.
For now we implement a very simple test: type variables match
anything, type functions (incl newtypes) match anything, and only
distinct data types fail to match. We can elaborate later.
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1251>
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
