[GHC] #14847: Inferring dependent kinds for non-recursive types

[GHC]

#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