#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 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by simonpj: Old description:

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 }}}

New description: 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 }}} See also: * #14451 * #12088 * #9427 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14847#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference| -------------------------------------+------------------------------------- Comment (by RyanGlScott): I think commit 2257a86daa72db382eb927df12a718669d5491f8 (`Taming the Kind Inference Monster`) fixed this ticket, since the following now compiles after that commit: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where data Proxy k (a :: k) = MkProxy data Proxy2 k a = MkP (Proxy k a) data Proxy2' k a where MkP' :: Proxy k a -> Proxy2' k a 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#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference| -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"91c4e71f633ebc81671fbfc752fc35b84883e744/ghc" 91c4e71f/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="91c4e71f633ebc81671fbfc752fc35b84883e744" Tests Trac #14847 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14847#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler