Make the forall-or-nothing rule only apply to invisible foralls
Currently, the forall
-or-nothing rule is defined (according to the GHC User's Guide) as: if a type has an outermost, explicit forall
, then all of the type variables in the type must be explicitly quantified. This does not say anything about whether the forall
is visible or invisible, and indeed, GHC currently applies this rule equally to both forms of forall
s. As a consequence, the following will be rejected:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Foo where
type F :: forall a -> b -> b
type F x y = y
While the forall
-or-nothing rule has long been established for invisible forall
s, it's less clear that it should apply to visible forall
s like in the program above. @rae lays out the case against the forall
-or-nothing rule applying to visible forall
s quite clearly in #16762 (comment 297270):
- Listing variables in a visible
forall
has a concrete, unignorable impact on the type. So if a visibleforall
triggers forall-or-nothing, users will almost certainly have to write a second, invisibleforall
to deal with an unscoped variables.- A user who explicitly wants forall-or-nothing can always write
forall.
at the top of every type.- A user who explicitly wants to manually scope all type variables can enable
-XNoImplicitForAll
. (https://github.com/ghc-proposals/ghc-proposals/pull/285, which is not yet implemented, as far as I know)
The consensus reached after discussion in #16762 (closed) is to revise the forall
-or-nothing rule to only apply to invisible forall
s. Although this changes the semantics of the language ever-so-slightly, I would argue that this falls below the bar needed for a GHC proposal, since:
- It it strictly backwards-compatible, as no current programs will break under the new scheme.
- Since visible
forall
s can only be used in kinds, the only way one can observe this behavior is to write a standalone kind signature. And standalone kind signatures are an experimental feature that is subject to change, as mentioned in the GHC 8.10.1 release notes.
A knock-on benefit of making this change is that it will make implementing a fix for #16762 (closed) much easier. The full details aren't terribly important, but read #16762 (comment 294998) if you want to know more.