I wonder if we can just omit the check entirely, as long as we check
#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): 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