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.

mentioned in issue #4426 (closed)

changed weight to 5

added Tbug Trac import labels

changed the description

I have some sympathy with this, but what about

f :: (Num a => a -> a) -> Int

Which of these does it mean?

f :: (forall a. Num a => a -> a) -> Int
f :: forall a. (Num a => a -> a) -> Int

Your proposal is (in effect) that "=>" does not trigger an implicit "forall"; only the top level of a type does that. I think that's probably very sensible, but it's a breaking change, and I don't know how much code, if any, would break.

Simon

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").

My understanding of monoidal's original proposal is that the change would affect only the right-hand sides of type and data declarations. Thus, Simon's case falls outside the scope of the proposal. Is this right?

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.

I believe internally we would change treatment of => everywhere, but the effect would be visible only in type and data declarations, since normal definitions would use implicit quantification as they do it currently.

closed

I see this exact proposal was created earlier: #4426 (closed).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

added Pnormal label