Fix the treatment of 'closed' definitions

The IdBindingInfo field of ATcId serves two purposes

- to control generalisation when we have -XMonoLocalBinds
- to check for floatability when dealing with (static e)

These are related, but not the same, and they'd becomme confused.
Trac #13804 showed this up via an example like this:

  f periph = let sr :: forall a. [a] -> [a]
                 sr = if periph then reverse else id

                 sr2 = sr
                 -- The question: is sr2 generalised?
                 -- It should be, because sr has a type sig
                 -- even though it has periph free
             in
             (sr2 [True], sr2 "c")

Here sr2 should be generalised, despite the free var 'periph'
in 'sr' because 'sr' has a closed type signature.

I documented all this very carefully this time, in TcRnTypes:
  Note [Meaning of IdBindingInfo]
  Note [Bindings with closed types: ClosedTypeId]

7 files changed, 263 insertions, 178 deletions

diff --git a/compiler/main/StaticPtrTable.hs b/compiler/main/StaticPtrTable.hs
index f61714db61..ff0d47e4b1 100644
--- a/compiler/main/StaticPtrTable.hs
+++ b/compiler/main/StaticPtrTable.hs
@@ -64,15 +64,9 @@ Here is a running example:
   body are stored in AST at the location of the static form.
 
 * The typechecker verifies that all free variables occurring in the
-  static form are closed (see Note [Bindings with closed types] in
-  TcRnTypes).  In our example, 'k' is closed, even though it is bound
-  in a nested let, we are fine.
-
-  The typechecker also surrounds the static form with a call to
-  `GHC.StaticPtr.fromStaticPtr`.
-
-   f x = let k = map toUpper
-         in ...fromStaticPtr (static k)...
+  static form are floatable to top level (see Note [Meaning of
+  IdBindingInfo] in TcRnTypes).  In our example, 'k' is floatable, even
+  though it is bound in a nested let, we are fine.
 
 * The desugarer replaces the static form with an application of the
   function 'makeStatic' (defined in module GHC.StaticPtr.Internal of
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 0c8d9108cc..7b01ababcd 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -409,7 +409,7 @@ tcValBinds top_lvl binds sigs thing_inside
                 -- declared with complete type signatures
                 -- Do not extend the TcIdBinderStack; instead
                 -- we extend it on a per-rhs basis in tcExtendForRhs
-        ; tcExtendLetEnvIds top_lvl [(idName id, id) | id <- poly_ids] $ do
+        ; tcExtendSigIds top_lvl poly_ids $ do
             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
                    { thing <- thing_inside
                      -- See Note [Pattern synonym builders don't yield dependencies]
@@ -435,7 +435,8 @@ tcBindGroups _ _ _ [] thing_inside
 
 tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
   = do  { -- See Note [Closed binder groups]
-          closed <- isClosedBndrGroup $ snd group
+          type_env <- getLclTypeEnv
+        ; let closed = isClosedBndrGroup type_env (snd group)
         ; (group', (groups', thing))
                 <- tc_group top_lvl sig_fn prag_fn group closed $
                    tcBindGroups top_lvl sig_fn prag_fn groups thing_inside
@@ -501,8 +502,9 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
 
     go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTcId, thing)
     go (scc:sccs) = do  { (binds1, ids1) <- tc_scc scc
-                        ; (binds2, thing) <- tcExtendLetEnv top_lvl closed ids1
-                                                            (go sccs)
+                        ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn
+                                                            closed ids1 $
+                                             go sccs
                         ; return (binds1 `unionBags` binds2, thing) }
     go []         = do  { thing <- thing_inside; return (emptyBag, thing) }
 
@@ -545,7 +547,7 @@ tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
                                       NonRecursive NonRecursive
                                       closed
                                       [lbind]
-       ; thing <- tcExtendLetEnv top_lvl closed ids thing_inside
+       ; thing <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside
        ; return (binds1, thing) }
 
 ------------------------
@@ -563,7 +565,7 @@ mkEdges sig_fn binds
     -- as explained in Note [Deterministic SCC] in Digraph.
   where
     no_sig :: Name -> Bool
-    no_sig n = noCompleteSig (sig_fn n)
+    no_sig n = not (hasCompleteSig sig_fn n)
 
     keyd_binds = bagToList binds `zip` [0::BKey ..]
 
@@ -1297,7 +1299,7 @@ tcMonoBinds _ sig_fn no_gen binds
 
         ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
                                        | (n,id) <- rhs_id_env]
-        ; binds' <- tcExtendLetEnvIds NotTopLevel rhs_id_env $
+        ; binds' <- tcExtendRecIds rhs_id_env $
                     mapM (wrapLocM tcRhs) tc_binds
 
         ; return (listToBag binds', mono_infos) }
@@ -1617,7 +1619,7 @@ decideGeneralisationPlan
 decideGeneralisationPlan dflags lbinds closed sig_fn
   | has_partial_sigs                         = InferGen (and partial_sig_mrs)
   | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig
-  | mono_local_binds closed                  = NoGen
+  | do_not_generalise closed                 = NoGen
   | otherwise                                = InferGen mono_restriction
   where
     binds = map unLoc lbinds
@@ -1638,8 +1640,11 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
     mono_restriction  = xopt LangExt.MonomorphismRestriction dflags
                      && any restricted binds
 
-    mono_local_binds ClosedGroup = False
-    mono_local_binds _           = xopt LangExt.MonoLocalBinds dflags
+    do_not_generalise (IsGroupClosed _ True) = 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
 
     -- With OutsideIn, all nested bindings are monomorphic
     -- except a single function binding with a signature
@@ -1661,46 +1666,56 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
         -- No args => like a pattern binding
         -- Some args => a function binding
 
-    no_sig n = noCompleteSig (sig_fn n)
+    no_sig n = not (hasCompleteSig sig_fn n)
 
-isClosedBndrGroup :: Bag (LHsBind GhcRn) -> TcM IsGroupClosed
-isClosedBndrGroup binds = do
-    type_env <- getLclTypeEnv
-    if foldUFM (is_closed_ns type_env) True fv_env
-      then return ClosedGroup
-      else return $ NonClosedGroup fv_env
+isClosedBndrGroup :: TcTypeEnv -> Bag (LHsBind GhcRn) -> IsGroupClosed
+isClosedBndrGroup type_env binds
+  = IsGroupClosed fv_env type_closed
   where
+    type_closed = allUFM (nameSetAll is_closed_type_id) fv_env
+
     fv_env :: NameEnv NameSet
     fv_env = mkNameEnv $ concatMap (bindFvs . unLoc) binds
 
     bindFvs :: HsBindLR GhcRn idR -> [(Name, NameSet)]
-    bindFvs (FunBind { fun_id = f, bind_fvs = fvs })
-       = [(unLoc f, fvs)]
+    bindFvs (FunBind { fun_id = L _ f, bind_fvs = fvs })
+       = let open_fvs = filterNameSet (not . is_closed) fvs
+         in [(f, open_fvs)]
     bindFvs (PatBind { pat_lhs = pat, bind_fvs = fvs })
-       = [(b, fvs) | b <- collectPatBinders pat]
+       = let open_fvs = filterNameSet (not . is_closed) fvs
+         in [(b, open_fvs) | b <- collectPatBinders pat]
     bindFvs _
        = []
 
-    is_closed_ns :: TcTypeEnv -> NameSet -> Bool -> Bool
-    is_closed_ns type_env ns b = b && nameSetAll (is_closed_id type_env) ns
-        -- ns are the Names referred to from the RHS of this bind
+    is_closed :: Name -> ClosedTypeId
+    is_closed name
+      | Just thing <- lookupNameEnv type_env name
+      = case thing of
+          AGlobal {}                     -> True
+          ATcId { tct_info = ClosedLet } -> True
+          _                              -> False
+
+      | otherwise
+      = True  -- The free-var set for a top level binding mentions
+
 
-    is_closed_id :: TcTypeEnv -> Name -> Bool
-    -- See Note [Bindings with closed types] in TcRnTypes
-    is_closed_id type_env name
+    is_closed_type_id :: Name -> Bool
+    -- We're already removed Global and ClosedLet Ids
+    is_closed_type_id name
       | Just thing <- lookupNameEnv type_env name
       = case thing of
-          ATcId { tct_info = ClosedLet } -> True  -- This is the key line
-          ATcId {}                       -> False
-          ATyVar {}                      -> False -- In-scope type variables
-          AGlobal {}                     -> True  --    are not closed!
-          _                              -> pprPanic "is_closed_id" (ppr name)
+          ATcId { tct_info = NonClosedLet _ cl } -> cl
+          ATcId { tct_info = NotLetBound }       -> False
+          ATyVar {}                              -> False
+               -- In-scope type variables are not closed!
+          _ -> pprPanic "is_closed_id" (ppr name)
+
       | otherwise
-      = True
-        -- The free-var set for a top level binding mentions
-        -- imported things too, so that we can report unused imports
-        -- These won't be in the local type env.
-        -- Ditto class method etc from the current module
+      = True   -- The free-var set for a top level binding mentions
+               -- imported things too, so that we can report unused imports
+               -- These won't be in the local type env.
+               -- Ditto class method etc from the current module
+
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index 8d00eaad76..935ad3dcb7 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -28,7 +28,7 @@ module TcEnv(
         -- Local environment
         tcExtendKindEnv, tcExtendKindEnvList,
         tcExtendTyVarEnv, tcExtendTyVarEnv2,
-        tcExtendLetEnv, tcExtendLetEnvIds,
+        tcExtendLetEnv, tcExtendSigIds, tcExtendRecIds,
         tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2,
         tcExtendIdBndrs, tcExtendLocalTypeEnv,
         isTypeClosedLetBndr,
@@ -101,7 +101,7 @@ import Encoding
 import FastString
 import ListSetOps
 import Util
-import Maybes( MaybeErr(..) )
+import Maybes( MaybeErr(..), orElse )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.IORef
@@ -420,40 +420,51 @@ isTypeClosedLetBndr :: Id -> Bool
 -- See Note [Bindings with closed types] in TcRnTypes
 isTypeClosedLetBndr = noFreeVarsOfType . idType
 
-tcExtendLetEnv :: TopLevelFlag -> IsGroupClosed -> [TcId] -> TcM a -> TcM a
--- Used for both top-level value bindings and and nested let/where-bindings
--- Adds to the TcIdBinderStack too
-tcExtendLetEnv top_lvl closed_group ids thing_inside
-  = tcExtendIdBndrs [TcIdBndr id top_lvl | id <- ids] $
-    tcExtendLetEnvIds' top_lvl closed_group
-                       [(idName id, id) | id <- ids]
-                       thing_inside
-
-tcExtendLetEnvIds :: TopLevelFlag -> [(Name, TcId)] -> TcM a -> TcM a
--- Used for both top-level value bindings and and nested let/where-bindings
+tcExtendRecIds :: [(Name, TcId)] -> TcM a -> TcM a
+-- Used for binding the recurive uses of Ids in a binding
+-- both top-level value bindings and and nested let/where-bindings
 -- Does not extend the TcIdBinderStack
-tcExtendLetEnvIds top_lvl
-  = tcExtendLetEnvIds' top_lvl ClosedGroup
+tcExtendRecIds pairs thing_inside
+  = tc_extend_local_env NotTopLevel
+          [ (name, ATcId { tct_id   = let_id
+                         , tct_info = NonClosedLet emptyNameSet False })
+          | (name, let_id) <- pairs ] $
+    thing_inside
 
-tcExtendLetEnvIds' :: TopLevelFlag -> IsGroupClosed
-                   -> [(Name,TcId)] -> TcM a
-                   -> TcM a
--- Used for both top-level value bindings and and nested let/where-bindings
+tcExtendSigIds :: TopLevelFlag -> [TcId] -> TcM a -> TcM a
+-- Used for binding the Ids that have a complete user type signature
 -- Does not extend the TcIdBinderStack
-tcExtendLetEnvIds' top_lvl closed_group pairs thing_inside
+tcExtendSigIds top_lvl sig_ids thing_inside
   = tc_extend_local_env top_lvl
-      [ (name, ATcId { tct_id = let_id
-                     , tct_info = case closed_group of
-                         ClosedGroup
-                           | isTypeClosedLetBndr let_id -> ClosedLet
-                           | otherwise -> NonClosedLet emptyNameSet False
-                         NonClosedGroup fvs ->
-                           NonClosedLet
-                             (maybe emptyNameSet id $ lookupNameEnv fvs name)
-                             (isTypeClosedLetBndr let_id)
-                     })
-      | (name, let_id) <- pairs ] $
+          [ (idName id, ATcId { tct_id   = id
+                              , tct_info = info })
+          | id <- sig_ids
+          , let closed = isTypeClosedLetBndr id
+                info   = NonClosedLet emptyNameSet closed ]
+     thing_inside
+
+
+tcExtendLetEnv :: TopLevelFlag -> TcSigFun -> IsGroupClosed
+                  -> [TcId] -> TcM a -> TcM a
+-- Used for both top-level value bindings and and nested let/where-bindings
+-- Adds to the TcIdBinderStack too
+tcExtendLetEnv top_lvl sig_fn (IsGroupClosed fvs fv_type_closed)
+               ids thing_inside
+  = tcExtendIdBndrs [TcIdBndr id top_lvl | id <- ids] $
+    tc_extend_local_env top_lvl
+          [ (idName id, ATcId { tct_id   = id
+                              , tct_info = mk_tct_info id })
+          | id <- ids ]
     thing_inside
+  where
+    mk_tct_info id
+      | type_closed && isEmptyNameSet rhs_fvs = ClosedLet
+      | otherwise                             = NonClosedLet rhs_fvs type_closed
+      where
+        name        = idName id
+        rhs_fvs     = lookupNameEnv fvs name `orElse` emptyNameSet
+        type_closed = isTypeClosedLetBndr id &&
+                      (fv_type_closed || hasCompleteSig sig_fn name)
 
 tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
 -- For lambda-bound and case-bound Ids
@@ -470,14 +481,13 @@ tcExtendIdEnv2 :: [(Name,TcId)] -> TcM a -> TcM a
 tcExtendIdEnv2 names_w_ids thing_inside
   = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
                     | (_,mono_id) <- names_w_ids ] $
-    do  { tc_extend_local_env NotTopLevel
-                              [ (name, ATcId { tct_id = id
-                                             , tct_info = NotLetBound })
-                              | (name,id) <- names_w_ids] $
-          thing_inside }
-
-tc_extend_local_env :: TopLevelFlag -> [(Name, TcTyThing)]
-                    -> TcM a -> TcM a
+    tc_extend_local_env NotTopLevel
+            [ (name, ATcId { tct_id = id
+                           , tct_info    = NotLetBound })
+            | (name,id) <- names_w_ids]
+    thing_inside
+
+tc_extend_local_env :: TopLevelFlag -> [(Name, TcTyThing)] -> TcM a -> TcM a
 tc_extend_local_env top_lvl extra_env thing_inside
 -- Precondition: the argument list extra_env has TcTyThings
 --               that ATcId or ATyVar, but nothing else
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 8d59303883..ed435ed1e8 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -40,7 +40,7 @@ module TcRnTypes(
         -- Typechecker types
         TcTypeEnv, TcIdBinderStack, TcIdBinder(..),
         TcTyThing(..), PromotionErr(..),
-        IdBindingInfo(..),
+        IdBindingInfo(..), ClosedTypeId, RhsNames,
         IsGroupClosed(..),
         SelfBootInfo(..),
         pprTcTyThingCategory, pprPECategory, CompleteMatch(..),
@@ -60,9 +60,9 @@ module TcRnTypes(
         ArrowCtxt(..),
 
         -- TcSigInfo
-        TcSigInfo(..), TcIdSigInfo(..),
+        TcSigFun, TcSigInfo(..), TcIdSigInfo(..),
         TcIdSigInst(..), TcPatSynInfo(..),
-        isPartialSig,
+        isPartialSig, hasCompleteSig,
 
         -- Canonical constraints
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
@@ -805,8 +805,11 @@ data TcLclEnv           -- Changes as we move inside an expression
         tcl_tclvl      :: TcLevel,         -- Birthplace for new unification variables
 
         tcl_th_ctxt    :: ThStage,         -- Template Haskell context
-        tcl_th_bndrs   :: ThBindEnv,       -- Binding level of in-scope Names
-                                           -- defined in this module (not imported)
+        tcl_th_bndrs   :: ThBindEnv,       -- and binder info
+            -- The ThBindEnv records the TH binding level of in-scope Names
+            -- defined in this module (not imported)
+            -- We can't put this info in the TypeEnv because it's needed
+            -- (and extended) in the renamer, for untyed splices
 
         tcl_arrow_ctxt :: ArrowCtxt,       -- Arrow-notation context
 
@@ -840,6 +843,14 @@ data TcLclEnv           -- Changes as we move inside an expression
         tcl_errs :: TcRef Messages              -- Place to accumulate errors
     }
 
+type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, MsgDoc))
+        -- Monadic so that we have a chance
+        -- to deal with bound type variables just before error
+        -- message construction
+
+        -- Bool:  True <=> this is a landmark context; do not
+        --                 discard it when trimming for display
+
 type TcTypeEnv = NameEnv TcTyThing
 
 type ThBindEnv = NameEnv (TopLevelFlag, ThLevel)
@@ -1042,9 +1053,10 @@ data ArrowCtxt   -- Note [Escaping the arrow scope]
 data TcTyThing
   = AGlobal TyThing             -- Used only in the return type of a lookup
 
-  | ATcId   {           -- Ids defined in this module; may not be fully zonked
-        tct_id     :: TcId,
-        tct_info :: IdBindingInfo }   -- See Note [Bindings with closed types]
+  | ATcId           -- Ids defined in this module; may not be fully zonked
+      { tct_id   :: TcId
+      , tct_info :: IdBindingInfo   -- See Note [Meaning of IdBindingInfo]
+      }
 
   | ATyVar  Name TcTyVar        -- The type variable to which the lexically scoped type
                                 -- variable is bound. We only need the Name
@@ -1086,31 +1098,130 @@ instance Outputable TcTyThing where     -- Debugging only
    ppr (ATcTyCon tc)    = text "ATcTyCon" <+> ppr tc <+> dcolon <+> ppr (tyConKind tc)
    ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
 
--- | Describes how an Id is bound.
+-- | IdBindingInfo describes how an Id is bound.
 --
 -- It is used for the following purposes:
---
 -- a) for static forms in TcExpr.checkClosedInStaticForm and
--- b) to figure out when a nested binding can be generalised (in
---    TcBinds.decideGeneralisationPlan).
+-- b) to figure out when a nested binding can be generalised,
+--    in TcBinds.decideGeneralisationPlan.
 --
--- See Note [Meaning of IdBindingInfo].
-data IdBindingInfo
+data IdBindingInfo -- See Note [Meaning of IdBindingInfo and ClosedTypeId]
     = NotLetBound
     | ClosedLet
-    | NonClosedLet NameSet Bool
+    | NonClosedLet
+         RhsNames        -- Used for (static e) checks only
+         ClosedTypeId    -- Used for generalisation checks
+                         -- and for (static e) checks
 
--- Note [Meaning of IdBindingInfo]
---
--- @NotLetBound@ means that the Id is not let-bound (e.g. it is bound in a
--- lambda-abstraction or in a case pattern).
---
--- @ClosedLet@ means that the Id is let-bound, it is closed and its type is
--- closed as well.
---
--- @NonClosedLet fvs type-closed@ means that the Id is let-bound but it is not
--- closed. The @fvs@ set contains the free variables of the rhs. The type-closed
--- flag indicates if the type of Id is closed.
+-- | IsGroupClosed describes a group of mutually-recursive bindings
+data IsGroupClosed
+  = IsGroupClosed
+      (NameEnv RhsNames)  -- Free var info for the RHS of each binding in the goup
+                          -- Used only for (static e) checks
+
+      ClosedTypeId        -- True <=> all the free vars of the group are
+                          --          imported or ClosedLet or
+                          --          NonClosedLet with ClosedTypeId=True.
+                          --          In particular, no tyvars, no NotLetBound
+
+type RhsNames = NameSet   -- Names of variables, mentioned on the RHS of
+                          -- a definition, that are not Global or ClosedLet
+
+type ClosedTypeId = Bool
+  -- See Note [Meaning of IdBindingInfo and ClosedTypeId]
+
+{- Note [Meaning of IdBindingInfo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+NotLetBound means that
+  the Id is not let-bound (e.g. it is bound in a
+  lambda-abstraction or in a case pattern)
+
+ClosedLet means that
+   - The Id is let-bound,
+   - Any free term variables are also Global or ClosedLet
+   - Its type has no free variables (NB: a top-level binding subject
+     to the MR might have free vars in its type)
+   These ClosedLets can definitely be floated to top level; and we
+   may need to do so for static forms.
+
+   Property:   ClosedLet
+             is equivalent to
+               NonClosedLet emptyNameSet True
+
+(NonClosedLet (fvs::RhsNames) (cl::ClosedTypeId)) means that
+   - The Id is let-bound
+
+   - The fvs::RhsNames contains the free names of the RHS,
+     excluding Global and ClosedLet ones.
+
+   - For the ClosedTypeId field see Note [Bindings with closed types]
+
+For (static e) to be valid, we need for every 'x' free in 'e',
+x's binding must be floatable to top level.  Specifically:
+   * x's RhsNames must be non-empty
+   * x's type has no free variables
+See Note [Grand plan for static forms] in StaticPtrTable.hs.
+This test is made in TcExpr.checkClosedInStaticForm.
+Actually knowing x's RhsNames (rather than just its emptiness
+or otherwise) is just so we can produce better error messages
+
+Note [Bindings with closed types: ClosedTypeId]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  f x = let g ys = map not ys
+        in ...
+
+Can we generalise 'g' under the OutsideIn algorithm?  Yes,
+because all g's free variables are top-level; that is they themselves
+have no free type variables, and it is the type variables in the
+environment that makes things tricky for OutsideIn generalisation.
+
+Here's the invariant:
+   If an Id has ClosedTypeId=True (in its IdBindingInfo), then
+   the Id's type is /definitely/ closed (has no free type variables).
+   Specifically,
+       a) The Id's acutal type is closed (has no free tyvars)
+       b) Either the Id has a (closed) user-supplied type signature
+          or all its free varaibles are Global/ClosedLet
+             or NonClosedLet with ClosedTypeId=True.
+          In particular, none are NotLetBound.
+
+Why is (b) needed?   Consider
+    \x. (x :: Int, let y = x+1 in ...)
+Initially x::alpha.  If we happen to typecheck the 'let' before the
+(x::Int), y's type will have a free tyvar; but if the other way round
+it won't.  So we treat any let-bound variable with a free
+non-let-bound variable as not ClosedTypeId, regardless of what the
+free vars of its type actually are.
+
+But if it has a signature, all is well:
+   \x. ...(let { y::Int; y = x+1 } in
+           let { v = y+2 } in ...)...
+Here the signature on 'v' makes 'y' a ClosedTypeId, so we can
+generalise 'v'.
+
+Note that:
+
+  * A top-level binding may not have ClosedTypeId=True, if it suffers
+    from the MR
+
+  * A nested binding may be closed (eg 'g' in the example we started
+    with). Indeed, that's the point; whether a function is defined at
+    top level or nested is orthogonal to the question of whether or
+    not it is closed.
+
+  * A binding may be non-closed because it mentions a lexically scoped
+    *type variable*  Eg
+        f :: forall a. blah
+        f x = let g y = ...(y::a)...
+
+Under OutsideIn we are free to generalise an Id all of whose free
+variables have ClosedTypeId=True (or imported).  This is an extension
+compared to the JFP paper on OutsideIn, which used "top-level" as a
+proxy for "closed".  (It's not a good proxy anyway -- the MR can make
+a top-level binding with a free type variable.)
+-}
 
 instance Outputable IdBindingInfo where
   ppr NotLetBound = text "NotLetBound"
@@ -1118,14 +1229,6 @@ instance Outputable IdBindingInfo where
   ppr (NonClosedLet fvs closed_type) =
     text "TopLevelLet" <+> ppr fvs <+> ppr closed_type
 
--- | Tells if a group of binders is closed.
---
--- When it is not closed, it provides a map of binder ids to the free vars
--- in their right-hand sides.
---
-data IsGroupClosed = ClosedGroup
-                   | NonClosedGroup (NameEnv NameSet)
-
 instance Outputable PromotionErr where
   ppr ClassPE        = text "ClassPE"
   ppr TyConPE        = text "TyConPE"
@@ -1155,58 +1258,6 @@ pprPECategory NoDataKindsDC  = text "Data constructor"
 pprPECategory NoTypeInTypeTC = text "Type constructor"
 pprPECategory NoTypeInTypeDC = text "Data constructor"
 
-{- Note [Bindings with closed types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
-  f x = let g ys = map not ys
-        in ...
-
-Can we generalise 'g' under the OutsideIn algorithm?  Yes,
-because all g's free variables are top-level; that is they themselves
-have no free type variables, and it is the type variables in the
-environment that makes things tricky for OutsideIn generalisation.
-
-Definition:
-   A variable is "closed", and has tct_info set to TopLevel,
-iff
-   a) all its free variables are imported, or are let-bound and closed
-   b) generalisation is not restricted by the monomorphism restriction
-
-Invariant: a closed variable has no free type variables in its type.
-Why? Assume (induction hypothesis) that closed variables have closed
-types, and that we have a new binding f = e, satisfying (a) and (b).
-Then since monomorphism restriction does not apply, and there are no
-free type variables, we can fully generalise, so its type will be closed.
-
-Under OutsideIn we are free to generalise a closed let-binding.
-This is an extension compared to the JFP paper on OutsideIn, which
-used "top-level" as a proxy for "closed".  (It's not a good proxy
-anyway -- the MR can make a top-level binding with a free type
-variable.)
-
-Note that:
-  * A top-level binding may not be closed, if it suffers from the MR
-
-  * A nested binding may be closed (eg 'g' in the example we started with)
-    Indeed, that's the point; whether a function is defined at top level
-    or nested is orthogonal to the question of whether or not it is closed
-
-  * A binding may be non-closed because it mentions a lexically scoped
-    *type variable*  Eg
-        f :: forall a. blah
-        f x = let g y = ...(y::a)...
-
--}
-
-type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, MsgDoc))
-        -- Monadic so that we have a chance
-        -- to deal with bound type variables just before error
-        -- message construction
-
-        -- Bool:  True <=> this is a landmark context; do not
-        --                 discard it when trimming for display
-
 {-
 ************************************************************************
 *                                                                      *
@@ -1365,6 +1416,8 @@ instance Outputable WhereFrom where
 -- TcSimplify uses them, and TcSimplify is fairly
 -- low down in the module hierarchy
 
+type TcSigFun  = Name -> Maybe TcSigInfo
+
 data TcSigInfo = TcIdSig     TcIdSigInfo
                | TcPatSynSig TcPatSynInfo
 
@@ -1503,6 +1556,12 @@ isPartialSig :: TcIdSigInst -> Bool
 isPartialSig (TISI { sig_inst_sig = PartialSig {} }) = True
 isPartialSig _                                       = False
 
+-- | No signature or a partial signature
+hasCompleteSig :: TcSigFun -> Name -> Bool
+hasCompleteSig sig_fn name
+  = case sig_fn name of
+      Just (TcIdSig (CompleteSig {})) -> True
+      _                               -> False
 
 
 {-
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 9cd8cfa690..803761b903 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -13,7 +13,7 @@ module TcSigs(
        TcPatSynInfo(..),
        TcSigFun,
 
-       isPartialSig, noCompleteSig, tcIdSigName, tcSigInfoName,
+       isPartialSig, hasCompleteSig, tcIdSigName, tcSigInfoName,
        completeSigPolyId_maybe,
 
        tcTySigs, tcUserTypeSig, completeSigFromId,
@@ -144,13 +144,6 @@ errors were dealt with by the renamer.
 *                                                                      *
 ********************************************************************* -}
 
-type TcSigFun  = Name -> Maybe TcSigInfo
-
--- | No signature or a partial signature
-noCompleteSig :: Maybe TcSigInfo -> Bool
-noCompleteSig (Just (TcIdSig (CompleteSig {}))) = False
-noCompleteSig _                                 = True
-
 tcIdSigName :: TcIdSigInfo -> Name
 tcIdSigName (CompleteSig { sig_bndr = id }) = idName id
 tcIdSigName (PartialSig { psig_name = n })  = n
diff --git a/testsuite/tests/typecheck/should_compile/T13804.hs b/testsuite/tests/typecheck/should_compile/T13804.hs
new file mode 100644
index 0000000000..86173fa70a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13804.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE RankNTypes, MonoLocalBinds #-}
+
+module T13804 where
+
+f periph = let sr :: forall a. [a] -> [a]
+               sr = if periph then reverse else id
+
+               sr2 = sr
+               -- The question: is sr2 generalised?
+               -- It should be, because sr has a type sig
+               -- even though it has periph free
+           in
+           (sr2 [True], sr2 "c")
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index c381fe107c..a9eb4ff5b1 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -562,3 +562,4 @@ test('T13333', normal, compile, [''])
 test('T13585', [extra_files(['T13585.hs', 'T13585a.hs', 'T13585b.hs'])], run_command, ['$MAKE -s --no-print-directory T13585'])
 test('T13651', normal, compile, [''])
 test('T13785', normal, compile, [''])
+test('T13804', normal, compile, [''])