I want to run the following past you (using Visible Kind Applications but may be unrelated). The following compiles

{-# Language DataKinds           #-}
{-# Language KindSignatures      #-}
{-# Language TypeFamilies        #-}
{-# Language AllowAmbiguousTypes #-}

import Data.Kind

type G = Bool -> Type

data Fun :: G

class F (bool :: Bool) where
  type Not bool :: Bool
  foo :: Fun (Not bool)

but quantifying Bool invisibly all of a sudden I can't use Not

{-# Language DataKinds           #-}
{-# Language RankNTypes          #-}
{-# Language TypeApplications    #-}
{-# Language PolyKinds           #-}
{-# Language KindSignatures      #-}
{-# Language TypeFamilies        #-}
{-# Language AllowAmbiguousTypes #-}

import Data.Kind

type G = forall (b :: Bool). Type

data Fun :: G

class F (bool :: Bool) where
  type Not bool :: Bool
  foo :: Fun @(Not bool)

$ ghc-stage2 --interactive -ignore-dot-ghci 739_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 739_bug.hs, interpreted )

739_bug.hs:17:16: error:
    • Type constructor ‘Not’ cannot be used here
        (it is defined and used in the same recursive group)
    • In the first argument of ‘Fun’, namely ‘(Not bool)’
      In the type signature: foo :: Fun @(Not bool)
      In the class declaration for ‘F’
   |
17 |   foo :: Fun @(Not bool)
   |                ^^^
Failed, no modules loaded.

Is this restriction warranted