Always generalise top-level bindingswip/T21023

Fix #21023 by always generalising top-level binding; change
the documentation of -XMonoLocalBinds to match.

1 files changed, 25 insertions, 17 deletions

diff --git a/docs/users_guide/exts/let_generalisation.rst b/docs/users_guide/exts/let_generalisation.rst
index 6dc556b016..536f608543 100644
--- a/docs/users_guide/exts/let_generalisation.rst
+++ b/docs/users_guide/exts/let_generalisation.rst
@@ -24,44 +24,52 @@ To a first approximation, with :extension:`MonoLocalBinds` *top-level bindings a
 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:
-
-* 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.
+GHC implements a slightly more complicated rule because,
+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.
 
 So here are the exact rules used by MonoLocalBinds.
 With MonoLocalBinds, a binding group will be *generalised* if and only if
 
-*   Each of its free variables (excluding the variables bound by the group itself) is closed (see next bullet), or
+*   It is a top-level binding group, or
+*   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 ``f`` is called *closed* if and only if
+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)
+
+*Closed variables*.  The key idea is that: *if a variable is closed, then its type definitely has no free type variables*.  A variable ``f`` is called *closed* if and only if
 
 * The variable ``f`` is imported from another module, 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.
 
-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.  Hence ``f`` is closed, since it has a complete type signature with no free variables.
-
-* 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)
+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.
 
 Example 1 ::
 
-    f1 x = x+1
-    f2 y = f1 (y*2)
+    g v = ...
+        where
+          f1 x = x+1
+          f2 y = f1 (y*2)
 
-``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).
-
-These comments apply whether the bindings for ``f1`` and ``f2`` are at top level or nested.
+``f1`` has free variable ``(+)``, but it is imported and hence closed.  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).
 
 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.
+
+*Top-level bindings*.  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.  However, top-level bindings
+are nevertheless always generalised. To see why, consider ::
+
+   module M( f ) where
+     x = 5
+     f v = (v,x)
+
+The binding ``x=5`` falls under the Monomorphism Restriction, so that binding is not generalised, and hence ``f``'s binding is not closed.  If, as a result, we did not generalise ``f``, we would end up exporting ``f :: Any -> (Any, Integer)``, defaulting ``x``'s type to `Integer` and ``v``'s type to ``Any``.  This is counter-intuitive and undesirable, so we always generalise top-level bindings.