[GHC] #14645: Allow type family in data family return kind

[GHC]

#14645: Allow type family in data family return kind
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.4.1-alpha1
      Resolution:                    |             Keywords:  TypeInType,
                                     |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Let's translate to FC.   Here's the example
 {{{
 type family TF (x :: Type) :: Type
 data family DF (x :: Type) :: TF x

 type instance TF Bool = Type -> Type

 data instance DF Bool (a :: Type) = T1 a | T2
 }}}
 The translation to FC might look like this
 {{{
 axiom ax1 :: TF Bool ~ (Type -> Type)

 data DFBool a = T1 a | T2   -- An ordinary algebraic data type
   -- T1 :: a -> DFBool a

 axiom ax2 :: DFBool ~ DF Bool |> ax1

 $WT1 :: forall a. a -> DF Bool a
 $WT1 = /\a. \(x::a). T1 x |> ax2 a
   -- ax2 a :: DFBool a ~ ((DF Bool) |> ax1) a
 }}}

 The kind coercion `|> ax1` in the kind of `axiom ax2` is essential to make
 axiom `ax2` homogeneously kinded; both sides have kind `Type -> Type`.

 Does that look right?

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