Heterogeneous type equality evidence ignored

Either that or I am missing something...

Consider the following,

{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
             TypeOperators, ViewPatterns #-}

module Test where

data TypeRep (a :: k) where
  TypeCon :: String -> TypeRep a
  TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)

data TypeRepX where
  TypeRepX :: TypeRep a -> TypeRepX

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

trArrow :: TypeRep (->)
trArrow = undefined

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

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

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

buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
  case typeRepKind f of
    TRFun arg _ ->
      case eqTypeRep arg x of
        Just HRefl ->
          TypeRepX $ TypeApp f x

This fails with,

$ ghc Test.hs -fprint-explicit-kinds
[1 of 1] Compiling Test             ( Test.hs, Test.o )

Test.hs:38:30: error:
    • Expected kind ‘TypeRep (k1 -> res) a’,
        but ‘f’ has kind ‘TypeRep k a’
    • In the first argument of ‘TypeApp’, namely ‘f’
      In the second argument of ‘($)’, namely ‘TypeApp f x’
      In the expression: TypeRepX $ TypeApp f x
    • Relevant bindings include
        arg :: TypeRep * arg (bound at Test.hs:35:11)

That is, the typechecker doesn't believe that f's type (why is it saying "kind" here?), TypeRep k a, will unify with TypeRep (k1 -> res) a, despite the TRFun pattern match, which should have brought into scope that k ~ (arg -> res).

This was tested with a recent snapshot from ghc-8.0 (23baff79).

Am I missing something here or is this a bug?

Trac metadata

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