Perplexing levity polymorphism issue

I would have expected this to compile since the levity polymorphism patch (along with D2038) was merged, but sadly it seems the typechecker isn't quite clever enough yet (or perhaps I'm the not clever one),

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

module Test where

import Data.Kind
import GHC.Exts

data TypeRep (a :: k) where
  TypeCon :: String -> TypeRep a
  TypeApp :: forall k1 k2 (f :: k1 -> k2) (x :: k1). TypeRep f -> TypeRep x -> TypeRep (f x)
  TypeFun :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). TypeRep a -> TypeRep b -> TypeRep (a -> b)

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

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

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

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

toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
toApp (SomeTypeRep f) (SomeTypeRep a)
  | TypeFun arg res <- typeRepKind f
  , Just HRefl <- arg `eqTypeRep` typeRepKind a
  = Just $ SomeTypeRep (TypeApp f a)
toApp _ _ = Nothing