Type applications in patterns fails in cases involving polymorphic/higher-order kinds

Summary

Type applications in patterns fails in certain cases involving polymorphic kinds, see the example program below:

Steps to reproduce

{-# LANGUAGE GADTs, RankNTypes, PolyKinds, TypeApplications,
             ScopedTypeVariables #-}

import Data.Kind (Type)

data T where
  MkT :: forall (f :: forall k. k -> Type).
    f Int -> f Maybe -> T

k :: T -> ()
k (MkT @f (x :: f Int) (y :: f Maybe)) = ()

Here, f must be polykinded in order for the signature patterns to make sense. If the compiler chooses k ~ Type in order to make f Int kind-check, then f Maybe will result in an error.

This presently results in:

TyAppPat_HigherOrderKind.hs:11:32: error:
    • Expecting one more argument to ‘Maybe’
      Expected a type, but ‘Maybe’ has kind ‘* -> *’
    • In the first argument of ‘f’, namely ‘Maybe’
      In the type ‘f Maybe’
      In a pattern type signature: f Maybe

Expected behavior

This program should compile, and f should be bound to the type (forall k. k -> Type).

Environment

• GHC version used: HEAD.