Fix #18145 and also avoid needless work with implicit vars

 - `forAllOrNothing` now is monadic, so we can trace whether we bind
   an explicit `forall` or not.

 - #18145 arose because the free vars calculation was needlessly
   complex. It is now greatly simplified.

 - Replaced some other implicit var code with `filterFreeVarsToBind`.

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>

5 files changed, 117 insertions, 78 deletions

diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index 1b3b601e23..35e683652e 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,
-        forAllOrNothing, nubL, elemRdr
+        forAllOrNothing, nubL
   ) where
 
 import GHC.Prelude
@@ -65,7 +65,7 @@ import GHC.Data.FastString
 import GHC.Data.Maybe
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List          ( nubBy, partition, (\\), find )
+import Data.List          ( nubBy, partition, find )
 import Control.Monad      ( unless, when )
 
 #include "HsVersions.h"
@@ -164,13 +164,13 @@ rn_hs_sig_wc_type :: HsSigWcTypeScoping -> HsDocContext -> Maybe SDoc
                   -> RnM (a, FreeVars)
 rn_hs_sig_wc_type scoping ctxt inf_err hs_ty thing_inside
   = do { check_inferred_vars ctxt inf_err hs_ty
-       ; free_vars <- extractFilteredRdrTyVarsDups hs_ty
+       ; free_vars <- filterInScopeM (extractHsTyRdrTyVarsDups hs_ty)
        ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
-             implicit_bndrs = case scoping of
-               AlwaysBind       -> tv_rdrs
-               BindUnlessForall -> forAllOrNothing (isLHsForAllTy hs_ty) tv_rdrs
-               NeverBind        -> []
+       ; implicit_bndrs <- case scoping of
+           AlwaysBind       -> pure tv_rdrs
+           BindUnlessForall -> forAllOrNothing (isLHsForAllTy hs_ty) tv_rdrs
+           NeverBind        -> pure []
        ; rnImplicitBndrs implicit_bndrs $ \ vars ->
     do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
        ; (res, fvs2) <- thing_inside wcs vars hs_ty'
@@ -178,7 +178,7 @@ rn_hs_sig_wc_type scoping ctxt inf_err hs_ty thing_inside
 
 rnHsWcType :: HsDocContext -> LHsWcType GhcPs -> RnM (LHsWcType GhcRn, FreeVars)
 rnHsWcType ctxt (HsWC { hswc_body = hs_ty })
-  = do { free_vars <- extractFilteredRdrTyVars hs_ty
+  = do { free_vars <- filterInScopeM (extractHsTyRdrTyVars hs_ty)
        ; (nwc_rdrs, _) <- partition_nwcs free_vars
        ; (wcs, hs_ty', fvs) <- rnWcBody ctxt nwc_rdrs hs_ty
        ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = hs_ty' }
@@ -278,22 +278,6 @@ extraConstraintWildCardsAllowed env
       StandaloneKindSigCtx {} -> False  -- See Note [Wildcards in standalone kind signatures] in GHC/Hs/Decls
       _                   -> False
 
--- | Finds free type and kind variables in a type,
---     without duplicates, and
---     without variables that are already in scope in LocalRdrEnv
---   NB: this includes named wildcards, which look like perfectly
---       ordinary type variables at this point
-extractFilteredRdrTyVars :: LHsType GhcPs -> RnM FreeKiTyVarsNoDups
-extractFilteredRdrTyVars hs_ty = filterInScopeM (extractHsTyRdrTyVars hs_ty)
-
--- | Finds free type and kind variables in a type,
---     with duplicates, but
---     without variables that are already in scope in LocalRdrEnv
---   NB: this includes named wildcards, which look like perfectly
---       ordinary type variables at this point
-extractFilteredRdrTyVarsDups :: LHsType GhcPs -> RnM FreeKiTyVarsWithDups
-extractFilteredRdrTyVarsDups hs_ty = filterInScopeM (extractHsTyRdrTyVarsDups hs_ty)
-
 -- | When the NamedWildCards extension is enabled, partition_nwcs
 -- removes type variables that start with an underscore from the
 -- FreeKiTyVars in the argument and returns them in a separate list.
@@ -340,9 +324,12 @@ rnHsSigType :: HsDocContext
 -- that cannot have wildcards
 rnHsSigType ctx level inf_err (HsIB { hsib_body = hs_ty })
   = do { traceRn "rnHsSigType" (ppr hs_ty)
-       ; vars <- extractFilteredRdrTyVarsDups hs_ty
+       ; rdr_env <- getLocalRdrEnv
        ; check_inferred_vars ctx inf_err hs_ty
-       ; rnImplicitBndrs (forAllOrNothing (isLHsForAllTy hs_ty) vars) $ \ vars ->
+       ; vars0 <- forAllOrNothing (isLHsForAllTy hs_ty)
+           $ filterInScope rdr_env
+           $ extractHsTyRdrTyVarsDups hs_ty
+       ; rnImplicitBndrs vars0 $ \ vars ->
     do { (body', fvs) <- rnLHsTyKi (mkTyKiEnv ctx level RnTypeBody) hs_ty
 
        ; return ( HsIB { hsib_ext = vars
@@ -361,7 +348,7 @@ rnHsSigType ctx level inf_err (HsIB { hsib_body = hs_ty })
 -- therefore an indication that the user is trying to be fastidious, so
 -- we don't implicitly bind any variables.
 
--- | See Note [forall-or-nothing rule]. This tiny little function is used
+-- | See @Note [forall-or-nothing rule]@. This tiny little function is used
 -- (rather than its small body inlined) to indicate that we are implementing
 -- that rule.
 forAllOrNothing :: Bool
@@ -372,10 +359,14 @@ forAllOrNothing :: Bool
                 --  we want to bring both 'a' and 'b' into scope, hence False
                 -> FreeKiTyVarsWithDups
                 -- ^ Free vars of the type
-                -> FreeKiTyVarsWithDups
-forAllOrNothing True  _   = []
-forAllOrNothing False fvs = fvs
-
+                -> RnM FreeKiTyVarsWithDups
+forAllOrNothing has_outer_forall fvs = case has_outer_forall of
+  True -> do
+    traceRn "forAllOrNothing" $ text "has explicit outer forall"
+    pure []
+  False -> do
+    traceRn "forAllOrNothing" $ text "no explicit forall. implicit binders:" <+> ppr fvs
+    pure fvs
 
 rnImplicitBndrs :: FreeKiTyVarsWithDups
                 -- ^ Surface-syntax free vars that we will implicitly bind.
@@ -878,21 +869,20 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
 
        ; let -- See Note [bindHsQTyVars examples] for what
              -- all these various things are doing
-             bndrs, kv_occs, implicit_kvs :: [Located RdrName]
+             bndrs, implicit_kvs :: [Located RdrName]
              bndrs        = map hsLTyVarLocName hs_tv_bndrs
-             kv_occs      = nubL (bndr_kv_occs ++ body_kv_occs)
-                                 -- Make sure to list the binder kvs before the
-                                 -- body kvs, as mandated by
-                                 -- Note [Ordering of implicit variables]
-             implicit_kvs = filter_occs bndrs kv_occs
+             implicit_kvs = nubL $ filterFreeVarsToBind bndrs $
+               bndr_kv_occs ++ body_kv_occs
              del          = deleteBys eqLocated
-             all_bound_on_lhs = null ((body_kv_occs `del` bndrs) `del` bndr_kv_occs)
+             body_remaining = (body_kv_occs `del` bndrs) `del` bndr_kv_occs
+             all_bound_on_lhs = null body_remaining
 
        ; traceRn "checkMixedVars3" $
-           vcat [ text "kv_occs" <+> ppr kv_occs
-                , text "bndrs"   <+> ppr hs_tv_bndrs
+           vcat [ text "bndrs"   <+> ppr hs_tv_bndrs
                 , text "bndr_kv_occs"   <+> ppr bndr_kv_occs
-                , text "wubble" <+> ppr ((kv_occs \\ bndrs) \\ bndr_kv_occs)
+                , text "body_kv_occs"   <+> ppr body_kv_occs
+                , text "implicit_kvs"   <+> ppr implicit_kvs
+                , text "body_remaining" <+> ppr body_remaining
                 ]
 
        ; implicit_kv_nms <- mapM (newTyVarNameRn mb_assoc) implicit_kvs
@@ -904,17 +894,6 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
                               , hsq_explicit  = rn_bndrs })
                       all_bound_on_lhs } }
 
-  where
-    filter_occs :: [Located RdrName]   -- Bound here
-                -> [Located RdrName]   -- Potential implicit binders
-                -> [Located RdrName]   -- Final implicit binders
-    -- Filter out any potential implicit binders that are either
-    -- already in scope, or are explicitly bound in the same HsQTyVars
-    filter_occs bndrs occs
-      = filterOut is_in_scope occs
-      where
-        is_in_scope locc = locc `elemRdr` bndrs
-
 {- Note [bindHsQTyVars examples]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have
@@ -943,7 +922,7 @@ Then:
 * Order is not important in these lists.  All we are doing is
   bring Names into scope.
 
-Finally, you may wonder why filter_occs removes in-scope variables
+Finally, you may wonder why filterFreeVarsToBind removes in-scope variables
 from bndr/body_kv_occs.  How can anything be in scope?  Answer:
 HsQTyVars is /also/ used (slightly oddly) for Haskell-98 syntax
 ConDecls
@@ -1654,9 +1633,15 @@ type FreeKiTyVarsWithDups = FreeKiTyVars
 -- | A 'FreeKiTyVars' list that contains no duplicate variables.
 type FreeKiTyVarsNoDups   = FreeKiTyVars
 
+-- | Filter out any type and kind variables that are already in scope in the
+-- the supplied LocalRdrEnv. Note that this includes named wildcards, which
+-- look like perfectly ordinary type variables at this point.
 filterInScope :: LocalRdrEnv -> FreeKiTyVars -> FreeKiTyVars
 filterInScope rdr_env = filterOut (inScope rdr_env . unLoc)
 
+-- | Filter out any type and kind variables that are already in scope in the
+-- the environment's LocalRdrEnv. Note that this includes named wildcards,
+-- which look like perfectly ordinary type variables at this point.
 filterInScopeM :: FreeKiTyVars -> RnM FreeKiTyVars
 filterInScopeM vars
   = do { rdr_env <- getLocalRdrEnv
@@ -1812,12 +1797,13 @@ extract_hs_tv_bndrs :: [LHsTyVarBndr flag GhcPs]
 --     'a' is bound by the forall
 --     'b' is a free type variable
 --     'e' is a free kind variable
-extract_hs_tv_bndrs tv_bndrs acc_vars body_vars
-  | null tv_bndrs = body_vars ++ acc_vars
-  | otherwise = filterOut (`elemRdr` tv_bndr_rdrs) (bndr_vars ++ body_vars) ++ acc_vars
+extract_hs_tv_bndrs tv_bndrs acc_vars body_vars = new_vars ++ acc_vars
+  where
+    new_vars
+      | null tv_bndrs = body_vars
+      | otherwise = filterFreeVarsToBind tv_bndr_rdrs $ bndr_vars ++ body_vars
     -- NB: delete all tv_bndr_rdrs from bndr_vars as well as body_vars.
     -- See Note [Kind variable scoping]
-  where
     bndr_vars = extract_hs_tv_bndrs_kvs tv_bndrs
     tv_bndr_rdrs = map hsLTyVarLocName tv_bndrs
 
@@ -1848,5 +1834,16 @@ extract_tv tv acc =
 nubL :: Eq a => [Located a] -> [Located a]
 nubL = nubBy eqLocated
 
-elemRdr :: Located RdrName -> [Located RdrName] -> Bool
-elemRdr x = any (eqLocated x)
+-- | Filter out any potential implicit binders that are either
+-- already in scope, or are explicitly bound in the binder.
+filterFreeVarsToBind :: FreeKiTyVars
+                     -- ^ Explicitly bound here
+                     -> FreeKiTyVarsWithDups
+                     -- ^ Potential implicit binders
+                     -> FreeKiTyVarsWithDups
+                     -- ^ Final implicit binders
+filterFreeVarsToBind bndrs = filterOut is_in_scope
+    -- Make sure to list the binder kvs before the body kvs, as mandated by
+    -- Note [Ordering of implicit variables]
+  where
+    is_in_scope locc = any (eqLocated locc) bndrs
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index c7c648bd87..6c071217f8 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -59,7 +59,7 @@ import GHC.Types.Basic  ( pprRuleName, TypeOrKind(..) )
 import GHC.Data.FastString
 import GHC.Types.SrcLoc as SrcLoc
 import GHC.Driver.Session
-import GHC.Utils.Misc   ( debugIsOn, filterOut, lengthExceeds, partitionWith )
+import GHC.Utils.Misc   ( debugIsOn, lengthExceeds, partitionWith )
 import GHC.Driver.Types ( HscEnv, hsc_dflags )
 import GHC.Data.List.SetOps ( findDupsEq, removeDups, equivClasses )
 import GHC.Data.Graph.Directed ( SCC, flattenSCC, flattenSCCs, Node(..)
@@ -664,7 +664,9 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
 
 rnFamInstEqn :: HsDocContext
              -> AssocTyFamInfo
-             -> [Located RdrName]    -- Kind variables from the equation's RHS
+             -> [Located RdrName]
+             -- ^ Kind variables from the equation's RHS to be implicitly bound
+             -- if no explicit forall.
              -> FamInstEqn GhcPs rhs
              -> (HsDocContext -> rhs -> RnM (rhs', FreeVars))
              -> RnM (FamInstEqn GhcRn rhs', FreeVars)
@@ -683,20 +685,36 @@ 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'.
-         -- 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
-             bnd_vars = map hsLTyVarLocName bndrs
-             payload_kvars = filterOut (`elemRdr` (bnd_vars ++ imp_vars)) rhs_kvars
-             -- Make sure to filter out the kind variables that were explicitly
-             -- bound in the type patterns.
-       ; payload_kvar_names <- mapM (newTyVarNameRn mb_cls) payload_kvars
 
-         -- all names not bound in an explicit forall
-       ; let all_imp_var_names = imp_var_names ++ payload_kvar_names
+         -- all_imp_vars represent the implicitly bound type variables. This is
+         -- empty if we have an explicit `forall` (see
+         -- Note [forall-or-nothing rule] in GHC.Rename.HsType), which means
+         -- ignoring:
+         --
+         -- - pat_kity_vars_with_dups, the variables mentioned in the LHS of
+         --   the equation, and
+         -- - rhs_kvars, the kind variables mentioned in an outermost kind
+         --   signature on the RHS of the equation. (See
+         --   Note [Implicit quantification in type synonyms] in
+         --   GHC.Rename.HsType for why these are implicitly quantified in the
+         --   absence of an explicit forall).
+         --
+         -- For example:
+         --
+         -- @
+         -- type family F a b
+         -- type instance forall a b c. F [(a, b)] c = a -> b -> c
+         --   -- all_imp_vars = []
+         -- type instance F [(a, b)] c = a -> b -> c
+         --   -- all_imp_vars = [a, b, c]
+         -- @
+       ; all_imp_vars <- forAllOrNothing (isJust mb_bndrs) $
+           -- No need to filter out explicit binders (the 'mb_bndrs = Just
+           -- explicit_bndrs' case) because there must be none if we're going
+           -- to implicitly bind anything, per the previous comment.
+           nubL $ pat_kity_vars_with_dups ++ rhs_kvars
+       ; all_imp_var_names <- mapM (newTyVarNameRn mb_cls) all_imp_vars
 
              -- All the free vars of the family patterns
              -- with a sensible binding location
@@ -2096,14 +2114,14 @@ rnConDecl decl@(ConDeclGADT { con_names   = names
           -- That order governs the order the implicitly-quantified type
           -- variable, and hence the order needed for visible type application
           -- See #14808.
-              free_tkvs = extractHsTvBndrs explicit_tkvs $
-                          extractHsTysRdrTyVarsDups (theta ++ arg_tys ++ [res_ty])
+        ; implicit_bndrs <- forAllOrNothing explicit_forall
+            $ extractHsTvBndrs explicit_tkvs
+            $ extractHsTysRdrTyVarsDups (theta ++ arg_tys ++ [res_ty])
 
-              ctxt    = ConDeclCtx new_names
+        ; let ctxt    = ConDeclCtx new_names
               mb_ctxt = Just (inHsDocContext ctxt)
 
-        ; traceRn "rnConDecl" (ppr names $$ ppr free_tkvs $$ ppr explicit_forall )
-        ; rnImplicitBndrs (forAllOrNothing explicit_forall free_tkvs) $ \ implicit_tkvs ->
+        ; rnImplicitBndrs implicit_bndrs $ \ 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/testsuite/tests/rename/should_fail/T18145.hs b/testsuite/tests/rename/should_fail/T18145.hs
new file mode 100644
index 0000000000..f991f3b19c
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T18145.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+
+module T18145 where
+
+type family A :: k
+type instance forall. A = Nothing :: Maybe a -- 'a' should be out of scope
+
+class Foo x where
+  type B x :: Maybe a
+  type forall x. B x = Nothing :: Maybe a -- 'a' should be out of scope
+
+instance Foo [x] where
+  type forall. B [x] = Nothing :: Maybe a -- 'a' should be out of scope
diff --git a/testsuite/tests/rename/should_fail/T18145.stderr b/testsuite/tests/rename/should_fail/T18145.stderr
new file mode 100644
index 0000000000..606ad0f695
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T18145.stderr
@@ -0,0 +1,6 @@
+
+T18145.hs:10:44: error: Not in scope: type variable ‘a’
+
+T18145.hs:14:41: error: Not in scope: type variable ‘a’
+
+T18145.hs:17:41: error: Not in scope: type variable ‘a’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 179ff13560..27b359dec1 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -153,3 +153,4 @@ test('T16504', normal, compile_fail, [''])
 test('T14548', normal, compile_fail, [''])
 test('T16610', normal, compile_fail, [''])
 test('T17593', normal, compile_fail, [''])
+test('T18145', normal, compile_fail, [''])