Skip to content

Require "forall" in definitions of polymorphic types

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.

Edited by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information