Note [forall-or-nothing rule]
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
- Binding scoped type variables GHC.Tc.Gen.Sig
Referenced by 7
- Language.Haskell.Syntax.Type call site ×2
- No nested foralls or contexts in instance types GHC.Hs.Type
- Ambiguous kind vars GHC.Tc.Validity
- HsType binders Language.Haskell.Syntax.Type
- Pattern signature binders and scoping Language.Haskell.Syntax.Type
- Lexically scoped type variables Language.Haskell.Syntax.Type