[GHC] #15628: Higher-rank kinds

[GHC]

#15628: Higher-rank kinds
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1-beta1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Taken from
 [https://github.com/ekmett/eq/blob/master/src/Data/Eq/Type/Hetero.hs#L73
 Data.Eq.Type.Hetero].

 `(:==)` (called `HEq` to avoid unnecessary extensions) fails if you add a
 `Proxy x ->` argument.

 {{{#!hs
 {-# Language RankNTypes, KindSignatures, PolyKinds, GADTs, DataKinds #-}

 import Data.Kind
 import Data.Proxy

 newtype HEq :: forall j. j -> forall k. k -> Type where
  HEq
   :: (forall (x::forall xx. xx -> Type). Proxy x -> x a -> x b)
   -> HEq a b
 }}}
 {{{
 $ ~/code/latestghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci
 398.hs
 GHCi, version 8.7.20180828: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 398.hs, interpreted )

 398.hs:7:2: error:
     • A newtype constructor cannot have existential type variables
       HEq :: forall j k xx (a :: j) (b :: k).
              (forall (x :: forall xx1. xx1 -> *). Proxy x -> x a -> x b)
              -> HEq a b
     • In the definition of data constructor ‘HEq’
       In the newtype declaration for ‘HEq’
   |
 7 |  HEq
   |  ^^^...
 Failed, no modules loaded.
 Prelude>
 }}}

 It compiles fine without `Proxy x ->`. Now my question is what existential
 type variable does `HEq` have, `-fprint-explicit-kinds` shows that `Proxy`
 is actually being instantiated at `(xx -> Type)` and not `(forall xx. xx
 -> Type)`

 {{{
 398.hs:10:2: error:
     • A newtype constructor cannot have existential type variables
       HEq :: forall j k xx (a :: j) (b :: k).
              (forall (x :: forall xx1. xx1 -> *).
               Proxy (xx -> *) (x xx) -> x j a -> x k b)
              -> HEq j a k b
     • In the definition of data constructor ‘HEq’
       In the newtype declaration for ‘HEq’
    |
 10 |  HEq
    |  ^^^...
 }}}

 so I suppose my question is, can we instantiate `Proxy` at a higher-rank
 kind? (#12045: `Proxy @FOO`)

 {{{
 >> type FOO = (forall xx. xx -> Type)
 >> :kind (Proxy :: FOO -> Type)

 <interactive>:1:2: error:
     • Expected kind ‘FOO -> *’, but ‘Proxy’ has kind ‘k0 -> *’
     • In the type ‘(Proxy :: FOO -> Type)’
 }}}

 It is possible to create a bespoke `Proxy`

 {{{#!hs
 type FOO = (forall x. x -> Type)

 data BespokeProxy :: FOO -> Type where
   BespokeProxy :: forall (c :: FOO). BespokeProxy c

 newtype HEq :: forall j. j -> forall k. k -> Type where
  HEq
   :: (forall (x::forall xx. xx -> Type). BespokeProxy x -> x a -> x b)
   -> HEq a b
 }}}

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