#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 RyanGlScott): I tried giving this a go, but quickly became stuck. I'll dump my progress here in case anyone finds it useful. * The first step is revising a validity check to allow type families to appear in data family return kinds. You'll need a predicate which checks if a type is a type family application: {{{#!hs -- | Returns @'Just' (fam_tc, args)@ if the argument 'Type' is a type family -- constructor @fam_tc@ applied to some arguments @args@. Otherwise, returns -- @Nothing@. tcGetTyFamTyConApp_maybe :: Type -> Maybe (TyCon, [Type]) tcGetTyFamTyConApp_maybe ty | Just ty' <- tcView ty = tcGetTyFamTyConApp_maybe ty' tcGetTyFamTyConApp_maybe (TyConApp fam_tc args) | isTypeFamilyTyCon fam_tc = Just (fam_tc, args) tcGetTyFamTyConApp_maybe _ = Nothing }}} Then you'll need to change `tcFamDecl1` to use this: {{{#!diff ; checkTc (tcIsStarKind final_res_kind - || isJust (tcGetCastedTyVar_maybe final_res_kind)) + || isJust (tcGetCastedTyVar_maybe final_res_kind) + || isJust (tcGetTyFamTyConApp_maybe final_res_kind)) (badKindSig False res_kind) }}} * The next step is to figure out where to grab the type family instance axiom from when typechecking data family instances (in `tcDataFamInstDecl`). My first inclination was to change `tcDataKindSig` to return a `CoAxiom` resulting from the return kind signature. However, this doesn't always work. For instance, in the example from comment:3, the return kind of the `DF Bool (a :: Type)` instance is simply `Type` by the type you get to `tcDataKindSig` (instead of something like `TF Bool`), which makes it essentially impossible to grab a type family axiom from. This makes me suspect that we need to grab this type family axiom earlier, perhaps when typechecking the type family patterns (in `tcFamTyPats`). At this point, I became lost. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14645#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler