Note [forall-or-nothing rule]

Language/Haskell/Syntax/Type.hs:448 compiler 1 ticket

Free variables in signatures are usually bound in an implicit 'forall' at the
beginning of user-written signatures. However, if the signature has an
explicit, invisible forall at the beginning, this is disabled. This is referred
to as the forall-or-nothing rule.

The idea is nested foralls express something which is only expressible
explicitly, while a top level forall could (usually) be replaced with an
implicit binding. Top-level foralls alone ("forall.") are therefore an
indication that the user is trying to be fastidious, so we don't implicitly
bind any variables.

Note that this rule only applies to outermost /in/visible 'forall's, and not
outermost visible 'forall's. See #18660 for more on this point.

Here are some concrete examples to demonstrate the forall-or-nothing rule in
action:

  type F1 :: a -> b -> b                    -- Legal; a,b are implicitly quantified.
                                            Equivalently: forall a b. a -> b -> b

  type F2 :: forall a b. a -> b -> b        -- Legal; explicitly quantified

  type F3 :: forall a. a -> b -> b          -- Illegal; the forall-or-nothing rule says that
                                            if you quantify a, you must also quantify b

  type F4 :: forall a -> b -> b             -- Legal; the top quantifier (forall a) is a /visible/
                                            quantifier, so the "nothing" part of the forall-or-nothing
                                            rule applies, and b is therefore implicitly quantified.
                                            Equivalently: forall b. forall a -> b -> b

  type F5 :: forall b. forall a -> b -> c   -- Illegal; the forall-or-nothing rule says that
                                            if you quantify b, you must also quantify c

  type F6 :: forall a -> forall b. b -> c   -- Legal: just like F4.

For a complete list of all places where the forall-or-nothing rule applies, see
"The `forall`-or-nothing rule" section of the GHC User's Guide.

Any type that obeys the forall-or-nothing rule is represented in the AST with
an HsOuterTyVarBndrs:

* If the type has an outermost, invisible 'forall', it uses HsOuterExplicit,
  which contains a list of the explicitly quantified type variable binders in
  `hso_bndrs`. After typechecking, HsOuterExplicit also stores a list of the
  explicitly quantified `InvisTVBinder`s in
  `hso_xexplicit :: XHsOuterExplicit GhcTc`.

* Otherwise, it uses HsOuterImplicit. HsOuterImplicit is used for different
  things depending on the phase:

  * After parsing, it does not store anything in particular.
  * After renaming, it stores the implicitly bound type variable `Name`s in
    `hso_ximplicit :: XHsOuterImplicit GhcRn`.
  * After typechecking, it stores the implicitly bound `TyVar`s in
    `hso_ximplicit :: XHsOuterImplicit GhcTc`.

  NB: this implicit quantification is purely lexical: we bind any
      type or kind variables that are not in scope. The type checker
      may subsequently quantify over further kind variables.
      See Note [Binding scoped type variables] in GHC.Tc.Gen.Sig.

HsOuterTyVarBndrs GhcTc is used in the typechecker as an intermediate data type
for storing the outermost TyVars/InvisTVBinders in a type.
See GHC.Tc.Gen.HsType.bindOuterTKBndrsX for an example of this.

References 1

Referenced by 7