GHC should be more forgiving with visible dependent quantification in visible type applications

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.

Trac metadata

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