#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