GADT bug with -O2

Reported by Daniel Gorín in http://www.haskell.org/pipermail/glasgow-haskell-users/2007-September/013178.html

This module:

{-# OPTIONS_GHC -fglasgow-exts #-}
module T where

data T a where T :: T a -> T [a]

class C a where
  f :: a -> ()

instance C (T [a]) where
  f (T x@(T _)) = f x

gives a compiler panic when compiled with -O2. With -dcore-lint we get:

$ ghc -c -O2 e.hs -dcore-lint
rm: cannot remove `e.o': No such file or directory
rm: cannot remove `e.hi': No such file or directory
*** Core Lint Errors: in result of SpecConstr ***
<no location info>:
    [in body of lambda with binder co_a5Z :: [a_a5t] ~ [a_a5X]]
    a_a5X is out of scope
*** Offending Program ***
Rec {
$sa_s6U :: forall a_a5t a_a60.
           ([a_a5t] ~ [a_a5X], a_a5t ~ [a_a60]) =>
           T.T a_a60 -> ()
[]
$sa_s6U =
  \ (@ a_a5t) (@ co_a5Z) (@ a_a60) (@ co_a62) (ds_d69 [Just B] :: T.T a_a60) ->
    case (T.T @ a_a5t @ a_a60 @ co_a62 ds_d69)
         `cast` (trans
                   (T.T (right co_a5Z)) (trans (T.T (right (sym co_a5Z))) (T.T co_a62))
                 :: T.T a_a5t ~ T.T [a_a60])
    of wild_B1 [Just B] { T.T @ a_a5X @ co_X68 ds_d67 [Just X] ->
    case ds_d67 `cast` (T.T (right (sym co_X68)) :: T.T a_a5X ~ T.T a_a60)
    of wild_Xc [Just X] { T.T @ a_X6c @ co_X6f ds_X6n [Just B] ->
    a_s6j
      @ a_X6c
      (wild_Xc
       `cast` (trans
                 (T.T (right co_X68)) (trans (T.T (right (sym co_X68))) (T.T co_X6f))
               :: T.T a_a60 ~ T.T [a_X6c]))
    }
    }
a_s6j [LoopBreaker Nothing] :: forall a_a5t. T.T [a_a5t] -> ()
[Arity 1
 Str: DmdType Sb
 RULES: "SC:a_s6j0" [0]
            forall {@ a_a5t @ co_a5Z @ a_a60 @ co_a62 ds_d69 [Just B] :: T.T a_a60}
              a_s6j @ a_a60
                    ((T.T @ a_a5t @ a_a60 @ co_a62 ds_d69)
                     `cast` (trans
                               (T.T (right co_a5Z)) (trans (T.T (right (sym co_a5Z))) (T.T co_a62))
                             :: T.T a_a5t ~ T.T [a_a60]))
              = $sa_s6U @ a_a5t @ co_a5Z @ a_a60 @ co_a62 ds_d69]
a_s6j =
  \ (@ a_a5t) (ds_X6c :: T.T [a_a5t]) ->
    case ds_X6c of wild_B1 [Just B] { T.T @ a_a5X @ co_a5Z ds_d67 [Just X] ->
    case ds_d67 `cast` (T.T (right (sym co_a5Z)) :: T.T a_a5X ~ T.T a_a5t)
    of wild_Xc [Just X] { T.T @ a_a60 @ co_a62 ds_d69 [Just B] ->
    a_s6j
      @ a_a60
      (wild_Xc
       `cast` (trans
                 (T.T (right co_a5Z)) (trans (T.T (right (sym co_a5Z))) (T.T co_a62))
               :: T.T a_a5t ~ T.T [a_a60]))
    }
    }
end Rec }

T.$f1 :: forall a_a5t. T.C (T.T [a_a5t])
[Exported]
[Arity 1
 Str: DmdType Sb]
T.$f1 =
  \ (@ a_a5t) ->
    (a_s6j @ a_a5t)
    `cast` (sym ((T.:Co:TC) (T.T [a_a5t]))
            :: T.T [a_a5t] -> () ~ (T.:TC) (T.T [a_a5t]))

*** End of Offense ***


<no location info>: 
Compilation had errors

This is a regression since 6.6.

Trac metadata

Trac field	Value
Version	6.8
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Unknown
Architecture	Unknown