#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