panic with kind polymorphism

{-# LANGUAGE ExistentialQuantification, PolyKinds,
DataKinds, RankNTypes, GADTs, TypeOperators #-}
module Bug where
import Data.Type.Equality

data WrappedType = forall a. WrapType a;

matchReflK :: forall (a :: ka) (b :: kb) (r :: *).
  ('WrapType a :~: 'WrapType b) -> (('WrapType a ~ 'WrapType b) => r) -> r;
matchReflK Refl r = r;

give this:

Bug.hs:8:15:
    Couldn't match kind ‘ka’ with ‘kb’
      ‘ka’ is untouchable
        inside the constraints ('WrapType a ~ 'WrapType b)
        bound by the type signature for
                   matchReflK :: ('WrapType a ~ 'WrapType b) => r
        at Bug.hs:(8,15)-(9,74)ghc: panic! (the 'impossible' happened)
  (GHC version 7.10.1 for x86_64-unknown-linux):
	No skolem info: ka_aqv[sk]

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

I actually think GHC should accept this (and furthermore infer ka ~ kb).

Trac metadata

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