Pattern signature not inferred

Should this pattern synonym declaration fail,

{-# Language DataKinds, TypeOperators, PolyKinds, GADTs, PatternSynonyms #-}

import Data.Kind

data NS f as where
 Here :: f a -> NS f (a:as)

data NP :: (k -> Type) -> ([k] -> Type) where
 Nil :: NP f '[]

pattern HereNil = Here Nil

$ ghci -ignore-dot-ghci hs/457.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/457.hs, interpreted ) [flags changed]

hs/457.hs:11:19: error:
    • Could not deduce: f ~~ NP f0
      from the context: (as ~ (a1 : as1), GHC.Types.Any ~ '[])
        bound by the signature for pattern synonym ‘HereNil’
        at hs/457.hs:11:1-26
      ‘f’ is a rigid type variable bound by
        the signature for pattern synonym ‘HereNil’
        at hs/457.hs:11:1-26
      Expected type: NS f as
        Actual type: NS (NP f0) ('[] : as0)
    • In the expression: Here Nil
      In an equation for ‘HereNil’: HereNil = Here Nil
    • Relevant bindings include
        $bHereNil :: NS f as (bound at hs/457.hs:11:9)
   |
11 | pattern HereNil = Here Nil
   |                   ^^^^^^^^

hs/457.hs:11:24: error:
    • Kind mismatch: cannot unify (f :: a -> *) with:
        NP a0 :: [GHC.Types.Any] -> *
      Their kinds differ.
      Expected type: f a1
        Actual type: NP a0 GHC.Types.Any
    • In the pattern: Nil
      In the pattern: Here Nil
      In the declaration for pattern synonym ‘HereNil’
   |
11 | pattern HereNil = Here Nil
   |                        ^^^
Failed, no modules loaded.
Prelude> 

It can be given a pattern signature, my question is can this not be inferred

-- pattern HereNil :: NS (NP f) ('[]:as)
pattern HereNil :: () => (nil_as ~ ('[]:as)) => NS (NP f) nil_as
pattern HereNil = Here Nil

Trac metadata

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