[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 goldfire):

 I'm wondering why you want a datatype instead of a data family. A data
 family makes grand sense here. But I'm still stuck on how a datatype could
 work this way.

 For example:

 {{{#!hs
 bar :: Foo n -> ...
 bar f = case f of
   MkFoo0 -> ...
   MkFoo1 x -> ...
   MkFoo2 x y -> ...
 }}}

 What are the types of `x` and `y`? I suppose they're existential... but
 they certainly don't look it from the declaration. And, if we discover
 that `f` is `MkFoo1`, say, then we learn that type of `bar` is ill-kinded.
 Indeed, perhaps the fact that `Foo n :: Type` tells us that `n ~ Z`
 without any pattern matches. (NB: `MkFun` really ''is'' injective, even if
 GHC can't know it.) Given this fact, I don't know how you could construct
 a function where there is more than one possible constructor for `Foo`.

 Also, I like to think about GADTs in terms of their desugaring to uniform
 datatypes with equality constraints. How would `Foo` desugar?

 {{{#!hs
 Foo :: forall (args :: Nat). MkFun args
 MkFoo0 :: forall (args :: Nat). args ~ Z => Foo args
 MkFoo1 :: forall (args :: Nat).
           forall (a :: Type).  -- existential??
           args ~ S Z => a -> Foo args
 }}}

 I've left off the last constructor, as it doesn't illustrate much more.
 The problem is that, in this formulation, the final result type must
 always be `Foo args`. That's what uniform means. But, here, `Foo args` is
 ill-kinded there. So I really have no idea what this construct means.

 My bottom line (supported more by my first line of argument than my
 second): you really want a data family, and we should close this ticket in
 favor of #14645. The only advantage of a datatype over a data family is
 that one pattern match of a datatype can cover a multitude of cases -- but
 you don't actually achieve that here. Furthermore, despite my comment:13,
 I have a much better picture of how to implement this idea for data
 families than I do for datatypes.

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