#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