[GHC] #15628: Higher-rank kinds
#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
#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 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15628#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I should have known. I can close it or label it with imprediativity, I still find it mysterious that {{{#!hs -- 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) {{{#!hs -- oops, you are actually writing -- Proxy @(x -> Type) (f @x) newtype Bar = Bar (forall (f :: FOO). Proxy f -> ()) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15628#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15628: Higher-rank kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: duplicate | Keywords: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => ImpredicativeTypes * status: new => closed * resolution: => duplicate Comment: Replying to [comment:2 Iceland_jack]:
adding a `Proxy` induces an existential variable `x` 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: {{{#!hs 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: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15628#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15628: Higher-rank kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: duplicate | Keywords: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15628#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC