Panic when promoted GADT arguments cross module boundaries

This seems to only happen when the importing module is compiled in a separate invocation of GHC from the module containing the GADT. That is, it happens with ghc -c-ing the two separately, or with --make, when only the importing module has been changed since last time. Cleaning between each compile seems to be a workaround, but that’s a massive pain. :)

Sample code & GHC's reaction:

{-# LANGUAGE KindSignatures, TypeOperators, DataKinds, GADTs #-}
module A where

data List (xs :: [*]) where
  N    :: List '[]
  (:>) :: x -> List xs -> List (x ': xs)

{-# LANGUAGE GADTs, TypeOperators #-}
module B where
import A

foo :: List (x ': xs) -> x
foo (x :> _) = x

$ ghc -c A.hs
$ ghc -c B.hs
ghc: panic! (the 'impossible' happened)
  (GHC version 7.4.1 for x86_64-apple-darwin):
	tyThingTyCon Data constructor `ghc-prim:GHC.Types.:{(w) d 64}'

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

(As an aside, it’s kind of annoying that TypeOperators isn’t automatically implied by DataKinds, but that’s not important really.)

Trac metadata

Trac field	Value
Version	7.4.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	andy@adradh.org.uk
Operating system
Architecture