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 |