Always generalise top-level bindings

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

5 files changed, 70 insertions, 30 deletions

diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 404a5a55d2..fb5d98b457 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -413,8 +413,8 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
     tc_scc (AcyclicSCC bind) = tc_sub_group NonRecursive [bind]
     tc_scc (CyclicSCC binds) = tc_sub_group Recursive    binds
 
-    tc_sub_group rec_tc binds =
-      tcPolyBinds sig_fn prag_fn Recursive rec_tc closed binds
+    tc_sub_group rec_tc binds = tcPolyBinds top_lvl sig_fn prag_fn
+                                            Recursive rec_tc closed binds
 
 recursivePatSynErr
   :: SrcSpan -- ^ The location of the first pattern synonym binding
@@ -437,7 +437,7 @@ tc_single _top_lvl sig_fn prag_fn
        }
 
 tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
-  = do { (binds1, ids) <- tcPolyBinds sig_fn prag_fn
+  = do { (binds1, ids) <- tcPolyBinds top_lvl sig_fn prag_fn
                                       NonRecursive NonRecursive
                                       closed
                                       [lbind]
@@ -474,7 +474,7 @@ mkEdges sig_fn binds
                                      , bndr <- collectHsBindBinders CollNoDictBinders bind ]
 
 ------------------------
-tcPolyBinds :: TcSigFun -> TcPragEnv
+tcPolyBinds :: TopLevelFlag -> TcSigFun -> TcPragEnv
             -> RecFlag         -- Whether the group is really recursive
             -> RecFlag         -- Whether it's recursive after breaking
                                -- dependencies based on type signatures
@@ -493,7 +493,7 @@ tcPolyBinds :: TcSigFun -> TcPragEnv
 -- Knows nothing about the scope of the bindings
 -- None of the bindings are pattern synonyms
 
-tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list
+tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list
   = setSrcSpan loc                              $
     recoverM (recoveryCode binder_names sig_fn) $ do
         -- Set up main recover; take advantage of any type sigs
@@ -501,7 +501,7 @@ tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list
     { traceTc "------------------------------------------------" Outputable.empty
     ; traceTc "Bindings for {" (ppr binder_names)
     ; dflags   <- getDynFlags
-    ; let plan = decideGeneralisationPlan dflags bind_list closed sig_fn
+    ; let plan = decideGeneralisationPlan dflags top_lvl closed sig_fn bind_list
     ; traceTc "Generalisation plan" (ppr plan)
     ; result@(_, poly_ids) <- case plan of
          NoGen              -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
@@ -1651,12 +1651,12 @@ instance Outputable GeneralisationPlan where
   ppr (CheckGen _ s) = text "CheckGen" <+> ppr s
 
 decideGeneralisationPlan
-   :: DynFlags -> [LHsBind GhcRn] -> IsGroupClosed -> TcSigFun
-   -> GeneralisationPlan
-decideGeneralisationPlan dflags lbinds closed sig_fn
+   :: DynFlags -> TopLevelFlag -> IsGroupClosed -> TcSigFun
+   -> [LHsBind GhcRn] -> GeneralisationPlan
+decideGeneralisationPlan dflags top_lvl closed sig_fn lbinds
   | has_partial_sigs                         = InferGen (and partial_sig_mrs)
   | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig
-  | do_not_generalise closed                 = NoGen
+  | do_not_generalise                        = NoGen
   | otherwise                                = InferGen mono_restriction
   where
     binds = map unLoc lbinds
@@ -1672,16 +1672,21 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
             <- mapMaybe sig_fn (collectHsBindListBinders CollNoDictBinders lbinds)
         , let (mtheta, _) = splitLHsQualTy (hsSigWcType hs_ty) ]
 
-    has_partial_sigs   = not (null partial_sig_mrs)
+    has_partial_sigs = not (null partial_sig_mrs)
 
     mono_restriction  = xopt LangExt.MonomorphismRestriction dflags
                      && any restricted binds
 
-    do_not_generalise (IsGroupClosed _ True) = False
+    do_not_generalise
+      | isTopLevel top_lvl             = False
+        -- See Note [Always generalise top-level bindings]
+
+      | IsGroupClosed _ True <- closed = False
         -- The 'True' means that all of the group's
         -- free vars have ClosedTypeId=True; so we can ignore
         -- -XMonoLocalBinds, and generalise anyway
-    do_not_generalise _ = xopt LangExt.MonoLocalBinds dflags
+
+      | otherwise = xopt LangExt.MonoLocalBinds dflags
 
     -- With OutsideIn, all nested bindings are monomorphic
     -- except a single function binding with a signature
@@ -1756,6 +1761,21 @@ isClosedBndrGroup type_env binds
                -- These won't be in the local type env.
                -- Ditto class method etc from the current module
 
+{- Note [Always generalise top-level bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is very confusing to apply NoGen to a top level binding. Consider (#20123):
+   module M where
+     x = 5
+     f y = (x, y)
+
+The MR means that x=5 is not generalise, so f's binding is no Closed.  So we'd
+be tempted to use NoGen. But that leads to f :: Any -> (Integer, Any), which
+is plain stupid.
+
+NoGen is good when we have call sites, but not at top level, where the
+function may be exported.  And it's easier to grok "MonoLocalBinds" as
+applying to, well, local bindings.
+-}
 
 {- *********************************************************************
 *                                                                      *
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.
diff --git a/testsuite/tests/typecheck/should_compile/T21023.hs b/testsuite/tests/typecheck/should_compile/T21023.hs
new file mode 100644
index 0000000000..322ba786b1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21023.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE MonoLocalBinds #-}
+
+module T21023( f ) where
+     x = 5
+     f v = (v,x)
diff --git a/testsuite/tests/typecheck/should_compile/T21023.stderr b/testsuite/tests/typecheck/should_compile/T21023.stderr
new file mode 100644
index 0000000000..fa7034f598
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21023.stderr
@@ -0,0 +1,5 @@
+TYPE SIGNATURES
+  f :: forall {a}. a -> (a, Integer)
+  x :: Integer
+Dependent modules: []
+Dependent packages: [base-4.16.0.0]
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 6d9ae4c566..24574892e7 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -819,3 +819,5 @@ test('FloatFDs', normal, compile, [''])
 test('ImplicitParamFDs', normal, compile, [''])
 test('T18406b', normal, compile, ['-ddump-tc -fprint-explicit-foralls -dsuppress-uniques -fprint-typechecker-elaboration'])
 test('T18529', normal, compile, ['-ddump-tc -fprint-explicit-foralls -dsuppress-uniques -fprint-typechecker-elaboration'])
+test('T21023', normal, compile, ['-ddump-types'])
+