[GHC] #14795: Data type return kinds don't obey the forall-or-nothing rule

[GHC]

#14795: Data type return kinds don't obey the forall-or-nothing rule
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC accepts       |  Unknown/Multiple
  invalid program                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Hm. After thinking about this some more, I'm not 100% convinced that this
 is an inconsistent design.

 The issue is that the `forall`-or-nothing rule applies to //top-level//
 type signatures. But data type return kinds are not truly top-level, as
 they can mention type variables bound before it. For instance, in this
 example:

 {{{#!hs
 data Foo2 (x :: b) :: forall a. a -> b -> Type
 }}}

 Here, the explicit return kind is only a small part of `Foo2`'s kind. The
 full shebang would be (using an [https://github.com/ghc-proposals/ghc-
 proposals/pull/54 explicit kind signature]):

 {{{#!hs
 type Foo2 :: forall b. b -> forall a. a -> b -> Type
 }}}

 In that sense, data type return kinds don't need to satisfy the `forall
 `-or-nothing rule, since they're not actually the thing at the top level.

 A similar phenomenon occurs at the term level. GHC accepts this:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}

 f :: (forall a. a -> b -> Int)
 f _ _ = 42
 }}}

 That's because in some sense, `(forall a. a -> b -> Int)` isn't the real
 top-level type signature here. The //real// top-level type signature is
 revealed if you query GHCi:

 {{{
 λ> :type +v f
 f :: forall b a. a -> b -> Int
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14795#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler