[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):

 I was wrong in detail but I think right in principle.  Consider
 {{{
 data Maybe a where
   Nothing :: Maybe a
 }}}
 The two `a`'s have nothing to do with each other. We could equally well
 write
 {{{
     data Maybe a where
       Nothing :: Maybe b
 or
     data Maybe a where
       Nothing :: forall b. Maybe b
 or
     data Maybe :: * -> * where
       Nothing :: Maybe a
 }}}
 Now consider your exmaple:
 {{{
 data SMaybe :: (k -> *) -> Maybe k -> * where
   SNothing :: forall (s :: k -> *). SMaybe s Nothing
 }}}
 The `k` in the `SNothing` is nothing to do with the `k` in the header,
 just like the `Maybe` case above.   So we could also write
 {{{
     data SMaybe :: (k -> *) -> Maybe k -> * where
       SNothing :: forall (s :: kk -> *). SMaybe s Nothing
 or
     data SMaybe :: (k -> *) -> Maybe k -> * where
       SNothing :: forall kk. forall (s :: kk -> *). SMaybe s Nothing
 }}}
 Actually we can't write the latter because we don't yet support explicit
 kind foralls, but morally we could.

 When kind-checking `SMaybe`, if we initially give it the ''monomorphic''
 kind
 {{{
    SMaybe :: (kappa -> *) -> Maybe kappa -> *
 }}}
 where `kappa` is a kind unification variable, then if we kind-check the
 type of `SNothing` we'll have a problem because `SMaybe` is insufficiently
 polymorphic to kind-check the type
 {{{
    forall kk. forall (s::kk -> *).  SMaybe s Nothing
 }}}
 We could hack our way round this, perhpas by (in effect) not kind-
 genrealising the type of `SNothing`.   But it seems smelly.  I'd be
 interested in what Stephanie and Dimitrios think.

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