#7873: A poly-kinded newtype existential crisis ---------------------------------+------------------------------------------ Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ---------------------------------+------------------------------------------ Changes (by simonpj): * difficulty: => Unknown Comment: Richard (goldfire) has it right. GHC puts the "forall k" at the outer level, if not told otherwise. Hence indeed the original `Magic` gets the type {{{ newtype Magic = Magic (forall p a. p a -> Int) -- Magic :: forall (k:BOX). (forall (p :: k -> *) (a :: k). p a -> Int) -- -> Magic }}} How can we "tell it otherwise". GHC has no notation for explicit kind quantification at the moment. We knew that we wanted ''implicit'' kind quantification, thus: {{{ data T (f :: k -> *) (a :: k) = MkT (f a ) }}} and that's the ''only'' kind quantification that's currently supported. The rule is that the kind-forall is wrapped immediately around the type- forall that binds it. Hence Richard's solution {{{ newtype Magic = Magic (forall p (a :: k). p a -> Int) -- Magic :: (forall (k:BOX) (p:k->*) (a:k). p a -> Int) -- -> Magic }}} Mind you, having written all this I find there's a bug in this kind quantification stuff, so that's not what happens right now, I'm afraid. Am fixing. I wish we had a simpler, clearer surface syntax for kind quantification; but the implicit version is so useful that I doubt we'll give it up. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7873#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler