[GHC] #16188: GHC HEAD-only panic (buildKindCoercion)

[GHC]

#16188: GHC HEAD-only panic (buildKindCoercion)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.7
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program compiles without issue on GHC 8.6.3:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind (Type)
 import Data.Type.Bool (type (&&))

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 type family Apply (f :: a ~> b) (x :: a) :: b
 data family Sing :: forall k. k -> Type

 data instance Sing :: Bool -> Type where
   SFalse :: Sing False
   STrue  :: Sing True

 (%&&) :: forall (x :: Bool) (y :: Bool).
          Sing x -> Sing y -> Sing (x && y)
 SFalse %&& _ = SFalse
 STrue  %&& a = a

 data RegExp :: Type -> Type where
   App :: RegExp t -> RegExp t -> RegExp t

 data instance Sing :: forall t. RegExp t -> Type where
   SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)

 data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
 type instance Apply ReNotEmptySym0 r = ReNotEmpty r

 type family ReNotEmpty (r :: RegExp t) :: Bool where
   ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2

 sReNotEmpty :: forall t (r :: RegExp t).
                Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
 sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2

 blah :: forall (t :: Type) (re :: RegExp t).
         Sing re -> ()
 blah (SApp sre1 sre2)
   = case (sReNotEmpty sre1, sReNotEmpty sre2) of
       (STrue, STrue) -> ()
 }}}

 However, it panics on GHC HEAD:

 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.7.20190114 for x86_64-unknown-linux):
         buildKindCoercion
   Any
   ReNotEmpty re2_a1hm
   Bool
   t_a1hg
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in
 ghc:Outputable
         pprPanic, called at compiler/types/Coercion.hs:2427:9 in
 ghc:Coercion
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler