#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

#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: | ---------------------------------+------------------------------------------ Comment(by monoidal): Both in current GHC and in this proposal `f` means {{{ f :: forall a. (Num a => a -> a) -> Int }}} This is rather intuitive; if we write {{{ g :: (Num a => a -> a) -> a }}} then it's clear that "forall a" should apply outside the parentheses. It would be a bit strange if changing "Int" to "a" changed the place where we the implicit quantifier appears. So, as far as I know, implicit quantification already occurs only at the top level of type expressions, and this change would only reject programs that use => for implicit quantification in type definitions (which is easy to fix by adding "forall"). -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7880#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | ---------------------------------+------------------------------------------ Comment(by simonpj): That is true but seems horribly ad hoc. It would be simpler and more uniform just to say that "=>" doesn't trigger an implicit quantification point. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7880#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler