Something is amiss with quantification in pattern synonym type signatures

Consider this program,

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeInType #-}

module Test where

data AType (a :: k) where
    AMaybe :: AType Maybe
    AInt :: AType Int
    AApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). AType a -> AType b -> AType (a b)

pattern PApp :: () => (fun ~ a b) => AType a -> AType b -> AType fun
--pattern PApp :: forall k (fun :: k) k1 (a :: k1 -> k) (b :: k1).
--            () => (fun ~ a b) => AType a -> AType b -> AType fun
pattern PApp fun arg <- AApp fun arg

I would have thought that the two type signatures would be equivalent. However, when I use the quantified signature GHC complains with,

hi.hs:14:34: error:
    • Expected kind ‘AType a’, but ‘fun’ has kind ‘AType a1’
    • In the declaration for pattern synonym ‘PApp’
    • Relevant bindings include
        arg :: AType b1 (bound at hi.hs:14:34)
        fun :: AType a1 (bound at hi.hs:14:30)

Moreover, if I use the un-quantified signature and ask GHCi for the full type signature, it gives me the precisely the quantified type that it rejected previously,

λ> :info PApp
pattern PApp :: forall k (fun :: k) k1 (a :: k1
                                             -> k) (b :: k1). () => fun ~ a b => AType a
                                                                                 -> AType b
                                                                                 -> AType fun
  	-- Defined at hi.hs:14:1

Very odd.

Trac metadata

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