#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