[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 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 at . Otherwise,
 returns
 -- @Nothing at .
 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