More improvement to MonoLocalBinds documentationwip/T19497

1 files changed, 35 insertions, 50 deletions

diff --git a/docs/users_guide/exts/let_generalisation.rst b/docs/users_guide/exts/let_generalisation.rst
index d966579377..c6de6454aa 100644
--- a/docs/users_guide/exts/let_generalisation.rst
+++ b/docs/users_guide/exts/let_generalisation.rst
@@ -11,72 +11,57 @@ Let-generalisation
 
     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/>`__,
+and a `related blog post
+<https://www.haskell.org/ghc/blog/20100930-LetGeneralisationInGhc7.html>`__.
 
--  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
-   (`Haskell Report, Section 4.5.5 <http://www.haskell.org/onlinereport/decls.html#sect4.5.5>`__)
+*   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
-papers <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf>`__
-"Let should not be generalised" and "Modular type inference with local
-assumptions", and a related `blog post
-<https://www.haskell.org/ghc/blog/20100930-LetGeneralisationInGhc7.html>`__.
+These comments apply whether the bindings for ``f1`` and ``f2`` are at top level or nested.
 
-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 papers!)
+Example 2 ::
 
+    f3 x = let g y = x+y in ....
 
+The binding for ``g`` has a free variable ``x`` that is lambda-bound, and hence not closed.  So ``g``\'s binding is not generalised.