#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