GADTs with newtype deriving can crash GHCi / cause Core Lint to fail

[Stefan O'Rear <stefanor@…>]

In my attempts to prove that GHC was generating errors on valid code, I have stumbled on a way to crash six versions of GHC, both F and FC, and in one case passing Core Lint!

stefan@stefans:/tmp$ V=6.4.2 ; ghc-$V -V ; ghc-$V -e 'seq icA ()' A.hs ; ghc-$V -dcore-lint -e 'seq icA ()' A.hs
The Glorious Glasgow Haskell Compilation System, version 6.4.2
*** Exception: Segmentation fault
*** Exception: Segmentation fault
stefan@stefans:/tmp$ V=6.6 ; ghc-$V -V ; ghc-$V -e 'seq icA ()' A.hs ; ghc-$V -dcore-lint -e 'seq icA ()' A.hs
The Glorious Glasgow Haskell Compilation System, version 6.6
mkCase1: null alts tpl_X6{v} [lid] main:A.icA{v rFP} [gid]
Segmentation fault
mkCase1: null alts tpl_X6{v} [lid] main:A.icA{v rFP} [gid]
ghc-6.6: panic! (the 'impossible' happened)
  (GHC version 6.6 for i386-unknown-linux):
        compileExpr
    <no location info>:
        In the expression: base:GHC.Err.error{(w) v 06} [gid]
                             @ base:GHC.Base.(){(w) tc 40} "Impossible alternative"
        Argument value doesn't match argument type:
        Fun type:
            [base:GHC.Base.Char{(w) tc 3o}] -> base:GHC.Base.(){(w) tc 40}
        Arg type: base:GHC.Prim.Addr#{(w) tc 33}
        Arg: "Impossible alternative"

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

stefan@stefans:/tmp$ V=6.7 ; ghc-$V -V ; ghc-$V -e 'seq icA ()' A.hs ; ghc-$V -dcore-lint -e 'seq icA ()' A.hs
The Glorious Glasgow Haskell Compilation System, version 6.7
mkCase1: null alts tpl_B1{v} [lid] main:A.icA{v rq2} [gid]
Segmentation fault
mkCase1: null alts tpl_B1{v} [lid] main:A.icA{v rq2} [gid]
ghc-6.7: panic! (the 'impossible' happened)
  (GHC version 6.7 for i386-unknown-linux):
        compileExpr
    <no location info>:
        In the expression: base:GHC.Err.error{(w) v 06} [gid]
                             @ base:GHC.Base.(){(w) tc 40} "Impossible alternative"
        Argument value doesn't match argument type:
        Fun type:
            [base:GHC.Base.Char{(w) tc 3o}] -> base:GHC.Base.(){(w) tc 40}
        Arg type: base:GHC.Prim.Addr#{(w) tc 33}
        Arg: "Impossible alternative"

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

stefan@stefans:/tmp$ V=6.7.20070213 ; ghc-$V -V ; ghc-$V -e 'seq icA ()' A.hs ; ghc-$V -dcore-lint -e 'seq icA ()' A.hs
The Glorious Glasgow Haskell Compilation System, version 6.7.20070213
mkCase: null alts tpl_B1{v} [lid] main:A.icA{v rsd} [gid]
Segmentation fault
mkCase: null alts tpl_B1{v} [lid] main:A.icA{v rsd} [gid]
ghc-6.7.20070213: panic! (the 'impossible' happened)
  (GHC version 6.7.20070213 for i386-unknown-linux):
        compileExpr
    <no location info>:
        In the expression: base:GHC.Err.error{(w) v 06} [gid]
                             @ base:GHC.Base.(){(w) tc 40} "Impossible alternative"
        Argument value doesn't match argument type:
        Fun type:
            [base:GHC.Base.Char{(w) tc 3o}] -> base:GHC.Base.(){(w) tc 40}
        Arg type: base:GHC.Prim.Addr#{(w) tc 33}
        Arg: "Impossible alternative"

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

stefan@stefans:/tmp$ V=6.7.20070223 ; ghc-$V -V ; ghc-$V -e 'seq icA ()' A.hs ; ghc-$V -dcore-lint -e 'seq icA ()' A.hs
The Glorious Glasgow Haskell Compilation System, version 6.7.20070223
mkCase: null alts tpl_B1{v} [lid] main:A.icA{v rs9} [gid]
Segmentation fault
mkCase: null alts tpl_B1{v} [lid] main:A.icA{v rs9} [gid]
ghc-6.7.20070223: panic! (the 'impossible' happened)
  (GHC version 6.7.20070223 for i386-unknown-linux):
        compileExpr
    <no location info>:
        In the expression: base:GHC.Err.error{(w) v 06} [gid]
                             @ base:GHC.Base.(){(w) tc 40} "Impossible alternative"
        Argument value doesn't match argument type:
        Fun type:
            [base:GHC.Base.Char{(w) tc 3o}] -> base:GHC.Base.(){(w) tc 40}
        Arg type: base:GHC.Prim.Addr#{(w) tc 33}
        Arg: "Impossible alternative"

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

stefan@stefans:/tmp$ V=6.7.20070323 ; ghc-$V -V ; ghc-$V -e 'seq icA ()' A.hs ; ghc-$V -dcore-lint -e 'seq icA ()' A.hs
The Glorious Glasgow Haskell Compilation System, version 6.7.20070323
mkCase: null alts tpl_B1{v} [lid] main:A.icA{v rs4} [gid]
Segmentation fault
mkCase: null alts tpl_B1{v} [lid] main:A.icA{v rs4} [gid]
ghc-6.7.20070323: panic! (the 'impossible' happened)
  (GHC version 6.7.20070323 for i386-unknown-linux):
        compileExpr
    <no location info>:
        In the expression: base:GHC.Err.error{(w) v 06} [gid]
                             @ base:GHC.Base.(){(w) tc 40} "Impossible alternative"
        Argument value doesn't match argument type:
        Fun type:
            [base:GHC.Base.Char{(w) tc 3o}] -> base:GHC.Base.(){(w) tc 40}
        Arg type: base:GHC.Prim.Addr#{(w) tc 33}
        Arg: "Impossible alternative"

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

stefan@stefans:/tmp$ cat A.hs
{-# OPTIONS_GHC -fglasgow-exts #-}
module A(II(..), icA) where

data II a where II :: II Int

class IC a where ic :: II a

instance IC Int where ic = II

newtype A = A Int deriving(IC)

icA = (ic :: II A)

[igloo]

Looks like a bug all right; thanks for the report!

[simonpj]

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.