[GHC] #7939: RHS of associated type not kind-checked

[GHC]

#7939: RHS of associated type not kind-checked
------------------------------------------+---------------------------------
  Reporter:  goldfire                     |          Owner:  goldfire        
      Type:  bug                          |         Status:  new             
  Priority:  normal                       |      Milestone:                  
 Component:  Compiler                     |        Version:  7.7             
Resolution:                               |       Keywords:                  
        Os:  Unknown/Multiple             |   Architecture:  Unknown/Multiple
   Failure:  GHC accepts invalid program  |     Difficulty:  Unknown         
  Testcase:  ghci/scripts/T7939           |      Blockedby:                  
  Blocking:                               |        Related:                  
------------------------------------------+---------------------------------

Comment(by goldfire):

 In response to monoidal's most recent comment:

 I'm fine with your definition for {{{A}}}. It is deeply strange-looking, I
 agree, but if we make the kind applications explicit, it's quite normal:

 {{{
 type family A (k :: BOX) :: k
 type instance A * = Double
 type instance A (* -> *) = Maybe
 }}}

 As for the GADT example, I find that more interesting. Let's make
 everything more explicit:

 {{{
 type family A (k :: BOX) :: k
 type instance A * = Bool

 type family B (k :: BOX) :: k
 type instance B (* -> *) = Maybe

 data D :: forall (k :: BOX). k -> * where
   D1 :: forall (k :: BOX). D k (A k)
   D2 :: forall (k :: BOX). D k (B k)
 }}}

 Now, {{{D}}} doesn't look GADT-like in its kind parameter, which is always
 just {{{k}}}. The difference between the version that works and the
 version that doesn't is that pattern-matching on the version that works
 does ''not'' refine information about the kind {{{k}}}. In fact, you can
 see this easily because you can write more instances for either {{{A}}} or
 {{{B}}} showing that the kind argument is not really fixed by this
 construction.

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