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