[GHC] #7880: Require "forall" in definitions of polymorphic types

[GHC]

#7880: Require "forall" in definitions of polymorphic types
---------------------------------+------------------------------------------
    Reporter:  monoidal          |       Owner:                             
        Type:  bug               |      Status:  new                        
    Priority:  normal            |   Milestone:                             
   Component:  Compiler          |     Version:  7.6.3                      
    Keywords:                    |          Os:  Unknown/Multiple           
Architecture:  Unknown/Multiple  |     Failure:  GHC accepts invalid program
  Difficulty:  Unknown           |    Testcase:                             
   Blockedby:                    |    Blocking:                             
     Related:                    |  
---------------------------------+------------------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Old description:

> With rank-n-types, we can write
>
> {{{
> data T1 = T (() => a)
> type T2 = () => a
> }}}
>
> but
>
> {{{
> data T1' = T' a
> type T2' = a
> }}}
>
> gives an error.
>
> I think this behavior is very odd. I propose the following simple rule:
> such variables in type and data declarations should never be implicitly
> quantified; i.e. they have to be introduced using "forall". Since above
> types require RankNTypes anyway, there is little harm in requiring
> "forall", and in my opinion it's good to inform the reader that a type
> uses universal quantification. More complicated example, from lens:
>
> {{{
> type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f
> t
> }}}
>
> By the way, GHC's documentation is outdated regarding this issue:
> http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/other-type-
> extensions.html point 7.12.5.1. states that "`data T a = MkT (Either a b)
> (b -> b)`" is equivalent to "`data T a = MkT (forall b. Either a b)
> (forall b. b -> b)`" - since at least GHC 7.2 the former gives an error.

New description:

 With rank-n-types, we can write

 {{{
 data T1 = T (() => a)
 type T2 = () => a
 }}}

 but

 {{{
 data T1' = T' a
 type T2' = a
 }}}

 gives an error.

 I think this behavior is very odd. I propose the following simple rule:
 such variables in type and data declarations should never be implicitly
 quantified; i.e. they have to be introduced using "forall". Since above
 types require RankNTypes anyway, there is little harm in requiring
 "forall", and in my opinion it's good to inform the reader that a type
 uses universal quantification. More complicated example, from lens:

 {{{
 type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
 }}}

 By the way, GHC's documentation is outdated regarding this issue:
 http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/other-type-
 extensions.html point 7.12.5.1. states that
 {{{
 data T a = MkT (Either a b)           (b -> b)
 data T a = MkT (forall b. Either a b) (forall b. b -> b)
 }}}
 are equipvalent, but since at least GHC 7.2 the former gives an error.

--

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