Higher-rank kinds

Taken from Data.Eq.Type.Hetero.

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

{-# 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 (closed): 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

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

Trac metadata

Trac field	Value
Version	8.6.1-beta1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture