The following program compiles without issue on GHC 8.6.3:

{-# 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