Can't parse `forall j -> @m k`

I was originally startled to discover that this typechecks:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
module Bug where

import Data.Kind

type family F1 (k :: Type) :: k where {}

type family F2 :: forall (k :: Type) -> k where
  F2 = F1

However, it turns out that this is actually fine. If you run :info F2 in GHCi with -fprint-explicit-matchabilities -fprint-explicit-kinds enabled, it will reveal the full story:

λ> :set -fprint-explicit-matchabilities -fprint-explicit-kinds 
λ> :info F2
type F2 :: forall {t :: GHC.Types.Matchability}. forall k ->{t} k
type family F2 @{t} where
    F2 @{'GHC.Types.Unmatchable} = F1
        -- Defined at Bug.hs:11:1

All that's going on is that the F2 = F1 implicitly matches t to be Unmatchable. That's fine, although I like to be explicit about this sort of thing in type families. When I tried to make this explicit:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
module Bug where

import Data.Kind

type family F1 (k :: Type) :: k where {}

type family F2 :: forall t. forall (k :: Type) -> @t k where
  F2 @{Unmatchable} = F1

It no longer parses!

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:12:51: error: parse error on input ‘@’
   |
12 | type family F2 :: forall t. forall (k :: Type) -> @t k where
   |                                                   ^

Would it be difficult to make this parse?