[GHC] #16371: GHC should be more forgiving with visible dependent quantification in visible type applications

[GHC]

#16371: GHC should be more forgiving with visible dependent quantification in
visible type applications
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.9
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  VisibleDependentQuantification     |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC HEAD currently rejects the following code:

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

 import Data.Kind
 import Data.Proxy

 f :: forall k a. 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
    |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 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:

 {{{#!hs
 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:

 {{{#!hs
 {-# 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16371>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler