#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