#14847: Inferring dependent kinds for non-recursive types -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this {{{ data Proxy k (a :: k) = MkProxy data Proxy2 k a = MkP (Proxy k a) }}} which is discussed in [http://downloads.haskell.org/~ghc/master/users- guide/glasgow_exts.html#inferring-dependency-in-datatype-declarations a corner of the user manual]. Surprisingly, we reject `Proxy2` -- but there is nothing difficult about inferring its kind. There would be if it was recursive -- but it isn't. Simple solution: for non-recursive type declarations (we do SCC analysis so we know which these are) do not call `getInitialKinds`; instead, just infer the kind of the definition! Simple. Warning: is this recursive? {{{ data Proxy2 k a where MkP :: Proxy k a -> Proxy2 k a }}} Presumably no more than the other definition. But currently we need `Proxy2` in the environment during kind inference, because we kind-check the result type. That seems jolly odd and inconsistent. Needs more thought. Similar questions for {{{ data T a where T :: Int -> T Bool type family F a where F Int = True F _ = False }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14847 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler