[GHC] #6137: Different behaviour between a GADT and a data family with regards to kind unification

[GHC]

#6137: Different behaviour between a GADT and a data family with regards to kind
unification
------------------------------+---------------------------------------------
 Reporter:  dreixel           |          Owner:                         
     Type:  bug               |         Status:  new                    
 Priority:  normal            |      Component:  Compiler (Type checker)
  Version:  7.5               |       Keywords:  PolyKinds              
       Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple       
  Failure:  None/Unknown      |       Testcase:                         
Blockedby:                    |       Blocking:                         
  Related:                    |  
------------------------------+---------------------------------------------
 We have discussed this before, but I don't remember if this was classified
 as a bug or as a "known feature" of GADTs. Given the following code:
 {{{
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE GADTs #-}

 data Sum a b = L a | R b

 data Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where
   LL :: a i -> Sum1 a b (L i)
   RR :: b i -> Sum1 a b (R i)

 data Code i o = F (Code (Sum i o) o)
 }}}

 An interpretation for `Code` using a data family works:
 {{{
 data family In (f :: Code i o) :: (i -> *) -> (o -> *)

 data instance In (F f) r o where
   In :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o
 }}}

 However, if we try to use a GADT instead...
 {{{
 data In' (f :: Code i o) :: (i -> *) -> (o -> *) where
   In' :: In' f (Sum1 r (In' (F f) r)) o -> In' (F f) r o
 }}}

 ... GHC complains:
 {{{
     Kind mis-match
     The first argument of `F' should have kind `Code (Sum k0 k1) k1',
     but `f' has kind `Code i o'
     In the type `In' f (Sum1 r (In' (F f) r)) o'
     In the definition of data constructor In'
     In the data declaration for In'
 }}}

 Is there a good reason for the difference in behaviour? If so, is this
 something we should document?

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