Visible kind application defeats type family with higher-rank result kind

After #15740 (closed), GHC now (correctly) rejects this program:

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

import Data.Kind

data SBool :: Bool -> Type
type family F :: forall k. k -> Type where
  F = SBool

$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20190115: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:12:7: error:
    • Expected kind ‘forall k. k -> *’,
        but ‘SBool’ has kind ‘Bool -> *’
    • In the type ‘SBool’
      In the type family declaration for ‘F’
   |
12 |   F = SBool
   |       ^^^^^

However, there's a very simple way to circumvent this: add a visible kind application to F's equation.

type family F :: forall k. k -> Type where
  F @Bool = SBool

If I understand things correctly, GHC shouldn't allow this.

Trac metadata

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