#15628 closed bug (duplicate)
Higher-rank kinds
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.6.1-beta1 |
Keywords: | ImpredicativeTypes | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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: 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
Change History (4)
comment:1 Changed 12 months ago by
comment:2 follow-up: 3 Changed 12 months ago by
I should have known. I can close it or label it with imprediativity,
I still find it mysterious that
-- works newtype Bar = Bar (forall (f :: FOO). ())
adding a Proxy
induces an existential variable x
seemingly without introducing quantification, but this is maybe a problem with my intuition? Or at least something rings odd about this (then again higher-rank kinds are odd and interesting)
-- oops, you are actually writing -- Proxy @(x -> Type) (f @x) newtype Bar = Bar (forall (f :: FOO). Proxy f -> ())
comment:3 Changed 12 months ago by
Keywords: | ImpredicativeTypes added |
---|---|
Resolution: | → duplicate |
Status: | new → closed |
Replying to Iceland_jack:
adding a
Proxy
induces an existential variablex
seemingly without introducing quantification
It does introduce quantification, and it's precisely because GHC can't support impredicative polymorphism at the moment. When you write:
newtype Bar = Bar (forall (f :: forall xx. xx -> Type). Proxy f -> ())
Then if we display all arguments visibly, this is what you are trying to write:
newtype Bar = Bar (forall (f :: forall xx. xx -> Type). Proxy @(forall xx. xx -> Type) f -> ())
You can't instantiate Proxy
's first argument with forall xx. xx -> Type
since it is a polytype, and that would be impredicative. Therefore, GHC has to pick something to instantiate xx
with in order to avoid impredicativity. Since we're in a data type, GHC bails out by creating an existentially quantified variable x
and using that to instantiate the higher-rank kind:
newtype Bar = forall x. Bar (forall (f :: x -> Type). Proxy @(x -> Type) (f @x) -> ())
But Bar
is a newtype, and therefore can't have existentials, leading to your error.
As simonpj notes in comment:1, this ticket is really asking for impredicative polymorphism. There is already a raft of tickets about this topic, so I'll opt to close this one.
comment:4 Changed 12 months ago by
Just chiming in that I agree with the other analysis. I think GHC is doing the right thing here, given that it can't do impredicative instantiation.
Instantiating a polymorphic type variable with a polytype (or polykind) is called "imprediative polymorphism" and is a swamp. GHC just does not have a decent story at the moment. But I think that is what you are asking for.
But see https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/ (PLDI'18).