GHC HEAD currently rejects the following code:

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Kind
import Data.Proxy

f :: forall k (a :: k). Proxy a
f = Proxy

g :: forall (a :: forall x -> x -> Type). Proxy a
g = f @(forall x -> x -> Type) @a

GHCi, version 8.9.20190227: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:14:6: error:
    • Illegal visible, dependent quantification in the type of a term:
        forall x -> x -> *
      (GHC does not yet support this)
    • In the type signature:
        g :: forall (a :: forall x -> x -> Type). Proxy a
   |
14 | g :: forall (a :: forall x -> x -> Type). Proxy a
   |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This test is implemented in TcValidity.vdqAllowed.

But GHC is being too conservative here. forall x -> x -> * isn't the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.

The immediate reason that this happens is because of this code:

vdqAllowed (TypeAppCtxt {}) = False

Unfortunately, fixing this bug isn't as simply as changing False to True. If you do that, then GHC becomes too forgiving and allows things like this:

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

lol :: forall a. a
lol = undefined

t2 = lol @(forall a -> a -> a)

Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.