Add `forAllOrNothing` function with note

3 files changed, 46 insertions, 31 deletions

diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index ab25334938..537b2a47f0 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -29,7 +29,7 @@ module GHC.Rename.HsType (
         extractHsTysRdrTyVarsDups,
         extractRdrKindSigVars, extractDataDefnKindVars,
         extractHsTvBndrs, extractHsTyArgRdrKiTyVarsDup,
-        nubL, elemRdr
+        forAllOrNothing, nubL, elemRdr
   ) where
 
 import GHC.Prelude
@@ -128,11 +128,11 @@ rn_hs_sig_wc_type scoping ctxt
   = do { free_vars <- extractFilteredRdrTyVarsDups hs_ty
        ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
-             bind_free_tvs = case scoping of
-                               AlwaysBind       -> True
-                               BindUnlessForall -> not (isLHsForAllTy hs_ty)
-                               NeverBind        -> False
-       ; rnImplicitBndrs bind_free_tvs tv_rdrs $ \ vars ->
+             implicit_bndrs = case scoping of
+               AlwaysBind       -> tv_rdrs
+               BindUnlessForall -> forAllOrNothing (isLHsForAllTy hs_ty) tv_rdrs
+               NeverBind        -> []
+       ; rnImplicitBndrs implicit_bndrs $ \ vars ->
     do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
        ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = ib_ty' }
              ib_ty'  = HsIB { hsib_ext = vars
@@ -302,35 +302,51 @@ rnHsSigType :: HsDocContext
 rnHsSigType ctx level (HsIB { hsib_body = hs_ty })
   = do { traceRn "rnHsSigType" (ppr hs_ty)
        ; vars <- extractFilteredRdrTyVarsDups hs_ty
-       ; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars ->
+       ; rnImplicitBndrs (forAllOrNothing (isLHsForAllTy hs_ty) vars) $ \ vars ->
     do { (body', fvs) <- rnLHsTyKi (mkTyKiEnv ctx level RnTypeBody) hs_ty
 
        ; return ( HsIB { hsib_ext = vars
                        , hsib_body = body' }
                 , fvs ) } }
 
-rnImplicitBndrs :: Bool    -- True <=> bring into scope any free type variables
-                           -- E.g.  f :: forall a. a->b
-                           --  we do not want to bring 'b' into scope, hence False
-                           -- But   f :: a -> b
-                           --  we want to bring both 'a' and 'b' into scope
+-- Note [forall-or-nothing rule]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- Free variables in signatures are usually bound in an implicit
+-- 'forall' at the beginning of user-written signatures. However, if the
+-- signature has an explicit forall at the beginning, this is disabled.
+--
+-- The idea is nested foralls express something which is only
+-- expressible explicitly, while a top level forall could (usually) be
+-- replaced with an implicit binding. Top-level foralls alone ("forall.") are
+-- therefore an indication that the user is trying to be fastidious, so
+-- we don't implicitly bind any variables.
+
+-- | See note Note [forall-or-nothing rule]. This tiny little function is used
+-- (rather than its small body inlined) to indicate we implementing that rule.
+forAllOrNothing :: Bool
+                -- ^ True <=> explicit forall
+                -- E.g.  f :: forall a. a->b
+                --  we do not want to bring 'b' into scope, hence True
+                -- But   f :: a -> b
+                --  we want to bring both 'a' and 'b' into scope, hence False
+                -> FreeKiTyVarsWithDups
+                -- ^ Free vars of the type
                 -> FreeKiTyVarsWithDups
-                                   -- Free vars of hs_ty (excluding wildcards)
-                                   -- May have duplicates, which is
-                                   -- checked here
+forAllOrNothing True  _   = []
+forAllOrNothing False fvs = fvs
+
+
+rnImplicitBndrs :: FreeKiTyVarsWithDups
+                -- ^ Surface-syntax free vars that we will implicitly bind.
+                -- May have duplicates, which is checked here
                 -> ([Name] -> RnM (a, FreeVars))
                 -> RnM (a, FreeVars)
-rnImplicitBndrs bind_free_tvs
-                fvs_with_dups
+rnImplicitBndrs implicit_vs_with_dups
                 thing_inside
-  = do { let fvs = nubL fvs_with_dups
-             -- implicit_vs are the surface-syntax free vars that are in fact
-             -- actually captured by implicit bindings
-             implicit_vs | bind_free_tvs = fvs
-                         | otherwise     = []
+  = do { let implicit_vs = nubL implicit_vs_with_dups
 
        ; traceRn "rnImplicitBndrs" $
-         vcat [ ppr fvs_with_dups, ppr fvs, ppr implicit_vs ]
+         vcat [ ppr implicit_vs_with_dups, ppr implicit_vs ]
 
        ; loc <- getSrcSpanM
        ; vars <- mapM (newLocalBndrRn . L loc . unLoc) implicit_vs
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 346a1cae99..a4ca8a5165 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -73,7 +73,7 @@ import Control.Arrow ( first )
 import Data.List ( mapAccumL )
 import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
-import Data.Maybe ( isNothing, fromMaybe, mapMaybe )
+import Data.Maybe ( isNothing, isJust, fromMaybe, mapMaybe )
 import qualified Data.Set as Set ( difference, fromList, toList, null )
 import Data.Function ( on )
 
@@ -681,11 +681,9 @@ rnFamInstEqn doc atfi rhs_kvars
              -- Use the "...Dups" form because it's needed
              -- below to report unused binder on the LHS
 
-         -- Implicitly bound variables, empty if we have an explicit 'forall' according
-         -- to the "forall-or-nothing" rule.
-       ; let imp_vars = case mb_bndrs of
-               Nothing -> nubL pat_kity_vars_with_dups
-               Just _ -> []
+         -- Implicitly bound variables, empty if we have an explicit 'forall'.
+         -- See Note [forall-or-nothing rule] in GHC.Rename.HsType.
+       ; let imp_vars = nubL $ forAllOrNothing (isJust mb_bndrs) pat_kity_vars_with_dups
        ; imp_var_names <- mapM (newTyVarNameRn mb_cls) imp_vars
 
        ; let bndrs = fromMaybe [] mb_bndrs
@@ -2099,7 +2097,7 @@ rnConDecl decl@(ConDeclGADT { con_names   = names
               mb_ctxt = Just (inHsDocContext ctxt)
 
         ; traceRn "rnConDecl" (ppr names $$ ppr free_tkvs $$ ppr explicit_forall )
-        ; rnImplicitBndrs (not explicit_forall) free_tkvs $ \ implicit_tkvs ->
+        ; rnImplicitBndrs (forAllOrNothing explicit_forall free_tkvs) $ \ implicit_tkvs ->
           bindLHsTyVarBndrs ctxt mb_ctxt Nothing explicit_tkvs $ \ explicit_tkvs ->
     do  { (new_cxt, fvs1)    <- rnMbContext ctxt mcxt
         ; (new_args, fvs2)   <- rnConDeclDetails (unLoc (head new_names)) ctxt args
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 7b9d1192bd..4f6b4f5887 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -2734,7 +2734,8 @@ Now, it's impossible for a Specified variable not to occur
 at all in the kind -- after all, it is Specified so it must have
 occurred.  (It /used/ to be possible; see tests T13983 and T7873.  But
 with the advent of the forall-or-nothing rule for kind variables,
-those strange cases went away.)
+those strange cases went away. See Note [forall-or-nothing rule] in
+GHC.Rename.HsType.)
 
 But one might worry about
     type v k = *