Skip to content

GitLab

GHC
GHC
Closed
Opened by Ryan Scott@RyanGlScottMaintainer

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 foralls. 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 foralls, it's less clear that it should apply to visible foralls like in the program above. @rae lays out the case against the forall-or-nothing rule applying to visible foralls quite clearly in #16762 (comment 297270):

  • Listing variables in a visible forall has a concrete, unignorable impact on the type. So if a visible forall triggers forall-or-nothing, users will almost certainly have to write a second, invisible forall 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 foralls. 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 foralls 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.