Here's an (unfortunately rather large) program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main (main) where

import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import Unsafe.Coerce (unsafeCoerce)

main :: IO ()
main = print $ traversableComposition @(M1 U1) @() @() @() @U1 @U1
                                      sPureFun sPureFun (SM1 SU1)

-----

sPureFun :: forall f a. SApplicative f => Sing (PureSym0 :: a ~> f a)
sPureFun = singFun1 @PureSym0 sPure

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

data (.@#@$$$) :: forall a b c. (b ~> c) -> (a ~> b) -> a ~> c
type instance Apply (f .@#@$$$ g) x = Apply f (Apply g x)

newtype instance Sing (f :: k1 ~> k2) =
  SLambda (forall t. Sing t -> Sing (Apply f t))

type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f

type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))

-----

data U1 p = U1
data instance Sing (z :: U1 p) where
  SU1 :: Sing 'U1

newtype M1 f p = M1 (f p)
data instance Sing (z :: M1 f p) where
  SM1 :: Sing x -> Sing ('M1 x)
data M1Sym0 :: forall k (f :: k -> Type) (p :: k). f p ~> M1 f p
type instance Apply M1Sym0 x = 'M1 x

newtype Compose f g x = Compose (f (g x))
data ComposeSym0 :: forall k1 k2 (f :: k2 -> Type) (g :: k1 -> k2) (x :: k1).
                    f (g x) ~> Compose f g x
type instance Apply ComposeSym0 x = 'Compose x
data instance Sing (z :: Compose f g a) where
  SCompose :: Sing x -> Sing ('Compose x)

instance (PFunctor f, PFunctor g) => PFunctor (Compose f g) where
  type Fmap h ('Compose x) = 'Compose (Fmap (FmapSym1 h) x)
instance (SFunctor f, SFunctor g) => SFunctor (Compose f g) where
  sFmap :: forall a b (h :: a ~> b) (x :: Compose f g a).
           Sing h -> Sing x -> Sing (Fmap h x)
  sFmap sh (SCompose sx) = SCompose (sFmap (singFun1 @(FmapSym1 h) (sFmap sh)) sx)

instance (PApplicative f, PApplicative g) => PApplicative (Compose f g) where
  type Pure x = 'Compose (Pure (Pure x))
  type 'Compose h <*> 'Compose x = 'Compose (Fmap (<*>@#@$) h <*> x)
instance (SApplicative f, SApplicative g) => SApplicative (Compose f g) where
  sPure sx = SCompose (sPure (sPure sx))
  SCompose sh %<*> SCompose sx = SCompose (sFmap (singFun2 @(<*>@#@$) (%<*>)) sh %<*> sx)

instance PFunctor U1 where
  type Fmap _ _ = 'U1
instance SFunctor U1 where
  sFmap _ _ = SU1
instance VFunctor U1 where
  fmapCompose _ _ SU1 = Refl

instance PFunctor f => PFunctor (M1 f) where
  type Fmap g ('M1 x) = 'M1 (Fmap g x)
instance SFunctor f => SFunctor (M1 f) where
  sFmap sg (SM1 sx) = SM1 (sFmap sg sx)
instance VFunctor f => VFunctor (M1 f) where
  fmapCompose sg sh (SM1 x) | Refl <- fmapCompose sg sh x = Refl

instance PApplicative U1 where
  type Pure _ = 'U1
  type _ <*> _ = 'U1
instance SApplicative U1 where
  sPure _ = SU1
  _ %<*> _ = SU1
instance VApplicative U1 where
  applicativeHomomorphism _ _ = Refl
  applicativeFmap _ _ = Refl

instance PTraversable U1 where
  type Traverse _ _ = Pure 'U1
instance STraversable U1 where
  sTraverse _ _ = sPure SU1
instance VTraversable U1 where
  traversableComposition :: forall p q r (f :: Type -> Type) (g :: Type -> Type)
                                   (h :: p ~> f q) (i :: q ~> g r) (x :: U1 p).
                            (VApplicative f, VApplicative g)
                         => Sing h -> Sing i -> Sing x
                         ->     Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
                            :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))
  traversableComposition _ si _
    | Refl <- applicativeHomomorphism @f sTraverseI sU1q
    , Refl <- applicativeFmap @f sTraverseI (sPure sU1q)
    = Refl
    where
      sTraverseI :: Sing (TraverseSym1 i :: U1 q ~> g (U1 r))
      sTraverseI = singFun1 (sTraverse si)

      sU1q :: Sing ('U1 :: U1 q)
      sU1q = SU1

instance PTraversable f => PTraversable (M1 f) where
  type Traverse g ('M1 x) = Fmap M1Sym0 (Traverse g x)
instance STraversable f => STraversable (M1 f) where
  sTraverse sg (SM1 sx) = sFmap (singFun1 @M1Sym0 SM1) (sTraverse sg sx)
instance VTraversable f => VTraversable (M1 f) where
  traversableComposition :: forall p q r (cf :: Type -> Type) (cg :: Type -> Type)
                                   (h :: p ~> cf q) (i :: q ~> cg r) (x :: M1 f p).
                            (VApplicative cf, VApplicative cg)
                         => Sing h -> Sing i -> Sing x
                         ->     Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
                            :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))
  traversableComposition sh si (SM1 (sfp :: Sing fp))
    | Refl <- traversableComposition sh si sfp
    , Refl <- fmapCompose @cf (singFun1 @(FmapSym1 M1Sym0) (sFmap sM1Fun))
                              sTraverseIFun sTraverseHIp
    , Refl <- --     Fmap (FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i) (Traverse h fp)
              -- :~: Fmap (TraverseSym1 i .@#@$$$ M1Sym0) (Traverse h fp)
              Refl @FmapSym0
                `apply` funExt @(f q) @(cg (M1 f r))
                               @(FmapSym1 M1Sym0 .@#@$$$ TraverseSym1 i)
                               @(TraverseSym1 i .@#@$$$ M1Sym0)
                               lemma
                `apply` Refl @(Traverse h fp)
    , Refl <- fmapCompose @cf sTraverseIFun sM1Fun sTraverseHIp
    = Refl
    where
      lemma :: forall (z :: f q). Sing z
            -> Fmap M1Sym0 (Traverse i z) :~: Traverse i (Apply M1Sym0 z)
      lemma _ = Refl

      sM1Fun :: forall z. Sing (M1Sym0 :: f z ~> M1 f z)
      sM1Fun = singFun1 SM1

      sTraverseHIp :: Sing (Traverse h fp)
      sTraverseHIp = sTraverse sh sfp

      sTraverseIFun :: forall hk. STraversable hk
                    => Sing (TraverseSym1 i :: hk q ~> cg (hk r))
      sTraverseIFun = singFun1 (sTraverse si)

-----

class PFunctor (f :: Type -> Type) where
  type Fmap (g :: a ~> b) (x :: f a) :: f b
data FmapSym0 :: forall f a b. (a ~> b) ~> f a ~> f b
data FmapSym1 :: forall f a b. (a ~> b) -> f a ~> f b
type instance Apply  FmapSym0 f    = FmapSym1 f
type instance Apply (FmapSym1 f) x = Fmap f x
class SFunctor (f :: Type -> Type) where
  sFmap :: forall a b (g :: a ~> b) (x :: f a).
           Sing g -> Sing x -> Sing (Fmap g x)
class (PFunctor f, SFunctor f) => VFunctor f where
  fmapCompose :: forall a b c (g :: b ~> c) (h :: a ~> b) (x :: f a).
                 Sing g -> Sing h -> Sing x
              -> Fmap g (Fmap h x) :~: Fmap (g .@#@$$$ h) x

class PFunctor f => PApplicative f where
  type Pure (x :: a) :: f a
  type (g :: f (a ~> b)) <*> (x :: f a) :: f b
infixl 4 <*>
data PureSym0 :: forall (f :: Type -> Type) a. a ~> f a
type instance Apply PureSym0 x = Pure x
data (<*>@#@$)  :: forall (f :: Type -> Type) a b. f (a ~> b) ~> f a ~> f b
data (<*>@#@$$) :: forall (f :: Type -> Type) a b. f (a ~> b) -> f a ~> f b
type instance Apply  (<*>@#@$)  f    = (<*>@#@$$) f
type instance Apply ((<*>@#@$$) f) x = f <*> x
class SFunctor f => SApplicative f where
  sPure :: forall a (x :: a).
           Sing x -> Sing (Pure x :: f a)

  (%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).
            Sing g -> Sing x -> Sing (g <*> x)
class (PApplicative f, SApplicative f, VFunctor f) => VApplicative f where
  applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).
                             Sing g -> Sing x
                          -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
  applicativeFmap :: forall a b (g :: a ~> b) (x :: f a).
                     Sing g -> Sing x
                  -> Fmap g x :~: (Pure g <*> x)

class PFunctor t => PTraversable t where
  type Traverse (g :: a ~> f b) (x :: t a) :: f (t b)
data TraverseSym1 :: forall t f a b. (a ~> f b) -> t a ~> f (t b)
type instance Apply (TraverseSym1 f) x = Traverse f x
class SFunctor t => STraversable t where
  sTraverse :: forall f a b (g :: a ~> f b) (x :: t a).
               SApplicative f
            => Sing g -> Sing x -> Sing (Traverse g x)
class (PTraversable t, STraversable t, VFunctor t) => VTraversable t where
  traversableComposition :: forall a b c (f :: Type -> Type) (g :: Type -> Type)
                                   (h :: a ~> f b) (i :: b ~> g c) (x :: t a).
                            (VApplicative f, VApplicative g)
                         => Sing h -> Sing i -> Sing x
                         ->     Traverse (ComposeSym0 .@#@$$$ FmapSym1 i .@#@$$$ h) x
                            :~: 'Compose (Fmap (TraverseSym1 i) (Traverse h x))

-----

funExt :: forall a b (f :: a ~> b) (g :: a ~> b).
          (forall (x :: a). Sing x
                         -> Apply f x :~: Apply g x)
       -> f :~: g
funExt _ = axiom

apply :: f :~: g -> a :~: b -> Apply f a :~: Apply g b
apply Refl Refl = Refl

axiom :: a :~: b
axiom = unsafeCoerce Refl

When compiled without optimization, this program prints "Refl", as you would expect:

$ /opt/ghc/8.6.3/bin/ghc -O0 Bug.hs -fforce-recomp
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...
$ ./Bug 
Refl

However, when compiled with optimizations, it starts failing at runtime!

$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...

$ ./Bug 
Bug: Impossible case alternative

This behavior can be observed on all versions of GHC from 8.2.2 to HEAD.

Interestingly, this program passes -dcore-lint on GHC 8.4.4 through HEAD, but on GHC 8.2.2, it fails -dcore-lint:

$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...

$ /opt/ghc/8.2.2/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    In a case alternative: (Refl cobox_a1UV :: (FmapSym0 :: (TyFun
                                                               (f1_X2dk b_a2aC
                                                                ~> g_a2aF (M1 f1_X2dk c_a2aD))
                                                               (f_a2aE (f1_X2dk b_a2aC)
                                                                ~> f_a2aE (g_a2aF (M1
                                                                                     f1_X2dk
                                                                                     c_a2aD)))
                                                             -> *))
                                               ~#
                                               (FmapSym0 :: (TyFun
                                                               (f1_X2dk b_a2aC
                                                                ~> g_a2aF (M1 f1_X2dk c_a2aD))
                                                               (f_a2aE (f1_X2dk b_a2aC)
                                                                ~> f_a2aE (g_a2aF (M1
                                                                                     f1_X2dk
                                                                                     c_a2aD)))
                                                             -> *)))
    No alternatives for a case scrutinee in head-normal form: ($WRefl
                                                                 @ Any @ Any)
                                                              `cast` (((:~:)
                                                                         (UnsafeCo nominal Any (f b
                                                                                                ~> g (M1
                                                                                                        f
                                                                                                        c)))
                                                                         (UnsafeCo nominal Any (FmapSym1
                                                                                                  M1Sym0
                                                                                                .@#@$$$ TraverseSym1
                                                                                                          i))
                                                                         (UnsafeCo nominal Any (TraverseSym1
                                                                                                  i
                                                                                                .@#@$$$ M1Sym0)))_R
                                                                      :: ((Any :~: Any) :: *)
                                                                         ~R#
                                                                         (((FmapSym1 M1Sym0
                                                                            .@#@$$$ TraverseSym1
                                                                                      i_a2aH)
                                                                           :~: (TraverseSym1 i_a2aH
                                                                                .@#@$$$ M1Sym0)) :: *))

(The full Core Lint error is absolutely enormous, so I'll post it as a separate attachment.)

The one thing about this program that might be considered strange is the use of axiom = unsafeCoerce Refl. I believe this should be a perfectly safe use of unsafeCoerce, but nevertheless, there is always the possibility that GHC is doing something unsightly when optimizing it. As one curiosity, if you mark axiom as NOINLINE, then the program produces a different result:

$ /opt/ghc/8.6.3/bin/ghc -O Bug.hs -fforce-recomp -dcore-lint
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
Linking Bug ...

$ ./Bug 

The program simply prints a newline, for some odd reason. (It doesn't appear to throw an exception either, since echo $? yields 0.)