[GHC] #7873: A poly-kinded newtype existential crisis

[GHC]

#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