Infer less polymorphic types for local bindings by default.
An ML-style language usually generalises the type of any ``let``\-bound or
``where``\-bound variable, so that it is as polymorphic as possible. With the
extension :extension:`MonoLocalBinds` GHC implements a slightly more conservative
policy, using the following rules:
An ML-style language usually generalises the type of any let-bound or where-bound variable, so that it is as polymorphic as possible. With the extension :extension:`MonoLocalBinds` GHC implements a slightly more conservative policy, for reasons descibed in Section 4.2 of `"OutsideIn(X): Modular type inference with local assumptions”<https://www.microsoft.com/en-us/research/publication/outsideinx-modular-type-inference-with-local-assumptions/>`__,
- A *binding group* is a strongly-connected component in the graph in which the nodes are let-bindings,
and there is an edge from a let-binding B to the binding for each of the free variables in B's RHS.
Before computing the strongly-connected components, any dependencies from variables with
complete type signatures are removed.
The extension :extension:`MonoLocalBinds` is implied by :extension:`TypeFamilies`
and :extension:`GADTs`. You can switch it off again with
:extension:`NoMonoLocalBinds <MonoLocalBinds>` but type inference becomes
less predictable if you do so. (Read the paper!)
- With :extension:`MonoLocalBinds`, a binding group is *generalised* if and only if
To a first approximation, with :extension:`MonoLocalBinds` *top-level bindings are
generalised, but local (i.e. nested) bindings are not*. The idea is
that, at top level, the type environment has no free type variables,
and so the difficulties described in these papers do not arise. But
GHC implements a slightly more complicated rule, for two reasons:
- Each of its free variables (excluding the variables bound by the group itself)
is either *imported* or *closed* (see next bullet), or
* The Monomorphism Restriction can cause even top-level bindings not to be generalised, and hence even the top-level type environment can have free type variables.
* For stylistic reasons, programmers sometimes write local bindings that make no use of local variables, so the binding could equally well be top-level. It seems reasonable to generalise these.
- Any of its binders has a partial type signature (see :ref:`partial-type-signatures`).
Adding a partial type signature ``f :: _``, (or, more generally, ``f :: _ => _``)
provides a per-binding way to ask GHC to
perform let-generalisation, even though :extension:`MonoLocalBinds` is on.
So here are the exact rules used by MonoLocalBinds.
With MonoLocalBinds, a binding group will be *generalised* if and only if
NB: even if the binding is generalised, it may still be affected by the
monomorphism restriction, which reduces generalisation
* Each of its free variables (excluding the variables bound by the group itself) is closed (see next bullet), or
* Any of its binders has a partial type signature (see Partial Type Signatures). Adding a partial type signature ``f :: _``, (or, more generally, ``f :: _ => _``) provides a per-binding way to ask GHC to perform let-generalisation, even though MonoLocalBinds is on.
- A variable is *closed* if and only if
- the variable is let-bound, and
A variable ``f`` is called *closed* if and only if
- one of the following holds:
* The variable ``f`` is imported from another module, or
- the variable has an explicit, complete (i.e. not partial) type signature
that has no free type variables, or
* The variable ``f`` is let-bound, and one of the following holds:
* ``f`` has an explicit, complete (i.e. not partial) type signature that has no free type variables, or
* its binding group is generalised over all its free type variables, so that ``f``'s type has no free type variables.
- its binding group is fully generalised, so it has a closed type
The key idea is that: *if a variable is closed, then its type definitely has no free type variables*.
Note that a signature like ``f :: a -> a`` is equivalent to ``f :: forall a. a->a``,
assuming ``a`` is not in scope, and hence is closed.
Note that:
* A signature like f :: a -> a is equivalent to ``f :: forall a. a -> a``, assuming ``a`` is not in scope. Hence ``f`` is closed, since it has a complete type signature with no free variables.
For example, consider ::
* Even if the binding is generalised, it may not be generalised over all its free type variables, either because it mentions locally-bound variables, or because of the monomorphism restriction (Haskell Report, Section 4.5.5)
f x = x + 1
g x = let h y = f y * 2
k z = z+x
in h x + k x
Example 1 ::
Here ``f`` is generalised because it has no free variables; and its
binding group is unaffected by the monomorphism restriction; and hence
``f`` is closed. The same reasoning applies to ``g``, except that it has
one closed free variable, namely ``f``. Similarly ``h`` is closed, *even
though it is not bound at top level*, because its only free variable
``f`` is closed. But ``k`` is not closed, because it mentions ``x``
which is not closed (because it is not let-bound).
f1 x = x+1
f2 y = f1 (y*2)
Notice that a top-level binding that is affected by the monomorphism
restriction is not closed, and hence may in turn prevent generalisation
of bindings that mention it.
``f1`` has free variable ``(+)``, but it is imported and hence closd. So ``f1``'s binding is generalised. As a result, its type ``f1 :: forall a. Num a => a -> a`` has no free type variables, so ``f1`` is closed. Hence ``f2``'s binding is generalised (since its free variables, ``f1`` and ``(*)`` are both closed).
The rationale for this more conservative strategy is given in `the
