Template variable unbound in rewrite rule

I'm getting GHC panic on GHC 8.0.1, GHC 8.2.1-rc1, and GHC 8.2.1-rc2. I think this error can somehow be related to #10924 (closed) or #13410 (closed) .

On all three versions of compiler it builds fine with -O1 or -O0. With -O2 it crashes with the following error:

[1 of 1] Compiling Numeric.Dimensions.Dim ( Dim.hs, Dim.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.2.0.20170507 for x86_64-unknown-linux):
	Template variable unbound in rewrite rule
  Variable: ipv_s1e7
  Rule "SC:concatDim0"
  Rule bndrs: [ipv_s1ee, ipv_s1ed, ipv_s1ef, ys_a19R, ipv_s1e4,
               ipv_s1e6, sc_s1fF, sc_s1fG, sc_s1fH, sc_s1fI, sc_s1fE, ipv_s1e7]
  LHS args: [TYPE: (ipv1_s1e6 |> ([Nth:0 (Sym ipv2)])_N),
             TYPE: ys_a19R, sc_s1fE,
             :*
               @ [Nat]
               @ ys_a19R
               @ ipv_s1ed
               @ ipv_s1ee
               @ ipv1_s1ef
               @~ (sc_s1fF :: ([Nat] :: *) ~# ([ipv_s1ed] :: *))
               @~ (sc_s1fG
                   :: (ys_a19R :: [Nat])
                      ~#
                      (ConsDim ipv_s1ee ipv2_s1ef :: [ipv1_s1ed]))
               sc_s1fH
               sc_s1fI]
  Actual args: [TYPE: (ipv1_X1eZ |> ([Nth:0 (Sym ipv2)])_N),
                TYPE: ys_a19R,
                ipv_s1ea
                `cast` ((Dim
                           ([Nth:0 (Sym ipv)])_N (Sym (Coh <ipv>_N ([Nth:0 (Sym ipv)])_N)))_R
                        :: (Dim ipv1_X1eZ :: *)
                           ~R#
                           (Dim (ipv1_X1eZ |> ([Nth:0 (Sym ipv2)])_N) :: *)),
                :*
                  @ [Nat]
                  @ ys_a19R
                  @ ipv_s1ed
                  @ ipv_s1ee
                  @ ipv1_s1ef
                  @~ (sc_s1fF :: ([Nat] :: *) ~# ([ipv_s1ed] :: *))
                  @~ (sc_s1fG
                      :: (ys_a19R :: [Nat])
                         ~#
                         (ConsDim ipv_s1ee ipv2_s1ef :: [ipv1_s1ed]))
                  sc_s1fH
                  sc_s1fI]
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1134:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
        pprPanic, called at compiler/specialise/Rules.hs:584:19 in ghc:Rules

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

Here is a minimal example I could come up with. Function concatDim is what causes the panic.

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeFamilyDependencies    #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

module Numeric.Dimensions.Dim (Dim (..), concatDim) where

import           Data.Type.Equality      ((:~:)(..))
import           GHC.TypeLits  (Nat, TypeError, ErrorMessage (..))
import           Unsafe.Coerce (unsafeCoerce)


-- | Type-level dimensionality
data Dim (ns :: k) where
  D   :: Dim '[]
  (:*) :: forall (n::Nat) (ns::[k]) . Dim n -> Dim ns -> Dim (ConsDim n ns)
  Dn :: forall (n :: Nat) . Dim (n :: Nat)
infixr 5 :*

-- | Either known or unknown at compile-time natural number
data XNat = XN Nat | N Nat
-- | Unknown natural number, known to be not smaller than the given Nat
type XN (n::Nat) = 'XN n
-- | Known natural number
type N (n::Nat) = 'N n

-- | List concatenation
type family (as :: [k]) ++ (bs :: [k]) :: [k] where
    (++) '[] bs = bs
    (++) as '[] = as
    (++) (a ': as) bs = a ': (as ++ bs)
infixr 5 ++

type family Head (xs :: [k]) :: k where
    Head (x ': xs) = x
    Head '[]       = TypeError ( 'Text
      "Head -- empty type-level list."
     )

type family Tail (xs :: [k]) :: [k] where
    Tail (x ': xs) = xs
    Tail '[]       = TypeError ( 'Text
      "Tail -- empty type-level list."
     )

-- | Unify usage of XNat and Nat.
--   This is useful in function and type definitions.
--   Mainly used in the definition of Dim.
type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l where
    ConsDim (x :: Nat) (xs :: [Nat])  = x    ': xs
    ConsDim (x :: Nat) (xs :: [XNat]) = N x  ': xs
    ConsDim (XN m)     (xs :: [XNat]) = XN m ': xs

concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim (xs ++ ys)
concatDim D ys         = ys
concatDim xs D         = xs
concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs ': (Tail xs ++ ys)) of
      Refl -> x :* concatDim xs ys

I am a little bit suspicious about unsafeCoerce Refl, but it worked in all other places so far. So if you find it not a bug but my incorrect usage of unsafeCoerce, please explain me why :)

UPDATE 28.06.2017: Interestingly, the two variants below compile fine with -O2:

concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim (xs ++ ys)
concatDim D ys         = ys
concatDim xs D         = xs
concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs ': (Tail xs ++ ys)) of
      Refl -> x :* concatDim xs ys
{-# NOINLINE concatDim #-}

concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim (xs ++ ys)
concatDim D ys         = ys
concatDim xs D         = xs
concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs ': (Tail xs ++ ys)) of
      Refl -> x :* concatDim (undefined :: Dim (Tail xs)) ys