[GHC] #14042: Datatypes cannot use a type family in their return kind

[GHC]

#14042: Datatypes cannot use a type family in their return kind
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 >  I wonder if we can just omit the check entirely, as long as we check
 the types of data constructors

 Ah yes, that sounds more plausible.  And now the whole thing makes more
 sense.  Even today with
 {{{
 data family T a :: *
 data instance T Int = T1 Bool
 }}}
 we desugar to a new type constructor `TInt :: *`, declared thus
 {{{
 data TInt = T1 Bool

 axiom ax1 :: TInt  ~R  T Int
 }}}
 and occurrences of the original user data constructor `T1` is converted to
 occurrences of the wrapper
 {{{
 $WT1 :: Bool -> T Int
 $WT1 x = T1 x |> ax1
 }}}
 Now I suppose that if we instead had
 {{{
 data family T a :: F a -- For some type family F
 }}}
 (which is what Ryan suggests), and we can prove `co :: F Int ~ *`, then
 perhaps we'd get
 {{{
 axiom ax1 :: (TInt :: *)  ~R  ((T Int |> co) :: *)
 }}}
 or something like that?   In other words, we relax the checks on the data
 ''family'' but add checks on the data ''constructors'', including putting
 the extra proof (e.g. `co :: F Int ~ *` in somewhere.  I'm not sure of the
 details, but there is enough desugaring around data families and their
 data instances that it looks entirely possible.

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