GitLab

The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality ((:~:))

type SameKind (a :: k) (b :: k) = (() :: Constraint)

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

data WhyCongSym1 (x :: Type) :: forall (a :: x)
                                       (y :: Type)
                                       (z :: x).
                                Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type

data WhyCongSym0 :: forall (x :: Type)
                           (a :: x)
                           (y :: Type)
                           (z :: x).
                    Type ~> Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
  where
    WhyCongSym0KindInference :: forall x arg.
                                SameKind (Apply WhyCongSym0 arg) (WhyCongSym1 arg) =>
                                WhyCongSym0 x

$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.2.2 for x86_64-unknown-linux):
        updateRole
  WhyCongSym0
  arg_a1A6[sk:1]
  [a1A5 :-> 4, a2Cy :-> 0, a2Cz :-> 1, a2CA :-> 2, a2CB :-> 3]
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls