Typechecker assertion failure

I've seen this program both fail with a typechecker assertion and Core lint violations with various GHC versions,

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeInType #-}

module Hi where

import Data.Kind (Type)

data (:~~:) a b where
    HRefl :: a :~~: a

data TypeRep (a :: k) where
    TrTyCon :: String -> TypeRep k -> TypeRep (a :: k)
    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
               TypeRep (a :: k1 -> k2)
            -> TypeRep (b :: k1)
            -> TypeRep (a b)

class Typeable (a :: k) where
    typeRep :: TypeRep a

data TypeRepX where
    TypeRepX :: forall k (a :: k). TypeRep a -> TypeRepX

eqTypeRep :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep = undefined

typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined

funResultTy :: TypeRepX -> TypeRepX -> Maybe TypeRepX
funResultTy (TypeRepX f) (TypeRepX x)
  | Just HRefl <- (typeRep :: TypeRep Type) `eqTypeRep` typeRepKind f
  , TRFun arg res <- f
  , Just HRefl <- arg `eqTypeRep` x
  = Just (TypeRepX res)
  | otherwise
  = Nothing

trArrow :: TypeRep (->)
trArrow = undefined

pattern TRFun :: forall fun. ()
              => forall arg res. (fun ~ (arg -> res))
              => TypeRep arg
              -> TypeRep res
              -> TypeRep fun
pattern TRFun arg res <- TrApp (TrApp (eqTypeRep trArrow -> Just HRefl) arg) res

The most recent type checker error is,

$ ~/ghc/ghc-testing/inplace/bin/ghc-stage2 -dcore-lint ~/Hi.hs
[1 of 1] Compiling Hi               ( /home/ben/Hi.hs, /home/ben/Hi.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20160315 for x86_64-unknown-linux):
        tcTyVarDetails cobox_a1Nm :: k_a1N4[ssk] ~# Type

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

Trac metadata

Trac field	Value
Version	8.0.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture