[GHC] #6049: Kind variable generalization error in GADTs

[GHC]

#6049: Kind variable generalization error in GADTs
----------------------------------------+-----------------------------------
    Reporter:  goldfire                 |       Owner:                           
        Type:  bug                      |      Status:  new                      
    Priority:  normal                   |   Milestone:                           
   Component:  Compiler (Type checker)  |     Version:  7.5                      
    Keywords:  PolyKinds                |          Os:  Unknown/Multiple         
Architecture:  Unknown/Multiple         |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                  |    Testcase:                           
   Blockedby:                           |    Blocking:                           
     Related:                           |  
----------------------------------------+-----------------------------------

Comment(by simonpj):

 Actually I think it's harder than I thought to "hack around".  Suppose we
 had
 {{{
 data SMaybe :: (k -> *) -> Maybe k -> * where
       SNothing :: Int
                -> (forall kk. forall (ss :: kk -> *). SMaybe ss Nothing)
                -> SMaybe s a
 }}}
 I have used a nested forall, so now really impossible (without lots of
 hackery) to make this work with a kind-monomorphic `SMaybe`.

 This can't really happen unless we have explicit kind-foralls, but sooner
 or later we will.

 I think the simplest path is to say that for GADT-style syntax you must
 give the kind of the type constructor in the header; and if you don't
 you'll get `* -> * -> *`, ie not even higher kinds.  This would mean that
 some existing programs would need a kind signature.
 {{{
 data T a b where
   MkT :: a b -> T a b
 }}}
 would need signatures, thus
 {{{
     data T (a : * -> *) b where
       MkT :: a b -> T a b
 or
     data T :: (* -> *) -> * -> * where
       MkT :: a b -> T a b
 or
     data T :: (k -> *) -> k -> * where
       MkT :: a b -> T a b
 }}}
 But it would enforce good practice (put those kind signatures in!  And I
 suppose that this new behaviour could be enabled by `-XPolyKinds`.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6049#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler