[GHC] #6093: Kind polymorphism fails with recursive type definition using different kind

[GHC]

#6093: Kind polymorphism fails with recursive type definition using different kind
----------------------------------------+-----------------------------------
    Reporter:  Ashley Yakeley           |       Owner:                           
        Type:  bug                      |      Status:  new                      
    Priority:  normal                   |   Milestone:                           
   Component:  Compiler (Type checker)  |     Version:  7.4.1                    
    Keywords:                           |          Os:  Unknown/Multiple         
Architecture:  Unknown/Multiple         |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                  |    Testcase:                           
   Blockedby:                           |    Blocking:                           
     Related:                           |  
----------------------------------------+-----------------------------------
Changes (by simonpj):

 * cc: dimitris@…, sweirich@… (added)
  * difficulty:  => Unknown


Comment:

 To be clear, you are hoping for this, where I have made kind
 quantification and kind arguments explicit:
 {{{
 data R :: k -> * where
   MkR :: forall k. forall (f :: * -> k). R (*->k) f -> R k (f ())
 }}}

 However, just as Hindley-Milner only allows monomorphic recursion for
 inferred types, so GHC only allows ''kind-monomorphic recursion'' for
 inferred kinds. So your example is behaving just as expected.

 At the value level, a type signature is enought to allow polymorphic
 recursion. So you might hope that this would work:
 {{{
  data R :: k -> * where
     MkR :: R f -> R (f ())
 }}}
 But it doesn't yet work, because there isn't a clear notion of when a type
 constructor has a type signature (yet anyway), whereas it's totally clear
 at the value level.  So currently there is no equivalent of "you can get
 polymorphic recursion if you give a type signature".

 Do you have a real application in mind or were you just playing?

 Simon

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