[GHC] #14352: Higher-rank kind ascription oddities

[GHC]

#14352: Higher-rank kind ascription oddities
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC accepts these two definitions:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Proxy

 f :: forall (x :: forall a. a -> Int). Proxy x
 f = Proxy

 g :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)
 g = Proxy
 }}}

 However, it does not accept this one, which (AFAICT) should be equivalent
 to the two above:

 {{{#!hs
 h :: forall x. Proxy (x :: forall b. b -> Int)
 h = Proxy
 }}}

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

 Bug.hs:13:23: error:
     • Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’
     • In the first argument of ‘Proxy’, namely
         ‘(x :: forall b. b -> Int)’
       In the type signature:
         h :: forall x. Proxy (x :: forall b. b -> Int)
    |
 13 | h :: forall x. Proxy (x :: forall b. b -> Int)
    |                       ^
 }}}

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