Use level numbers for generalisation

This fixes #15809, and is covered in
Note [Use level numbers for quantification] in TcMType.

This patch removes the "global tyvars" from the
environment, a nice little win.

12 files changed, 208 insertions, 247 deletions

diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index 533f137385..0ec0601521 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -56,9 +56,6 @@ module TcEnv(
         -- Defaults
         tcGetDefaultTys,
 
-        -- Global type variables
-        tcGetGlobalTyCoVars,
-
         -- Template Haskell stuff
         checkWellStaged, tcMetaTy, thLevel,
         topIdLvl, isBrackStage,
@@ -84,7 +81,6 @@ import PrelNames
 import TysWiredIn
 import Id
 import Var
-import VarSet
 import RdrName
 import InstEnv
 import DataCon ( DataCon )
@@ -108,7 +104,6 @@ import Encoding
 import FastString
 import ListSetOps
 import ErrUtils
-import Util
 import Maybes( MaybeErr(..), orElse )
 import qualified GHC.LanguageExtensions as LangExt
 
@@ -576,7 +571,7 @@ tc_extend_local_env top_lvl extra_env thing_inside
 -- as free in the types of extra_env.
   = do  { traceTc "tc_extend_local_env" (ppr extra_env)
         ; env0 <- getLclEnv
-        ; env1 <- tcExtendLocalTypeEnv env0 extra_env
+        ; let env1 = tcExtendLocalTypeEnv env0 extra_env
         ; stage <- getStage
         ; let env2 = extend_local_env (top_lvl, thLevel stage) extra_env env1
         ; setLclEnv env2 thing_inside }
@@ -594,52 +589,9 @@ tc_extend_local_env top_lvl extra_env thing_inside
             , tcl_th_bndrs = extendNameEnvList th_bndrs  -- We only track Ids in tcl_th_bndrs
                                  [(n, thlvl) | (n, ATcId {}) <- pairs] }
 
-tcExtendLocalTypeEnv :: TcLclEnv -> [(Name, TcTyThing)] -> TcM TcLclEnv
+tcExtendLocalTypeEnv :: TcLclEnv -> [(Name, TcTyThing)] -> TcLclEnv
 tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
-  | isEmptyVarSet extra_tvs
-  = return (lcl_env { tcl_env = extendNameEnvList lcl_type_env tc_ty_things })
-  | otherwise
-  = do { global_tvs <- readMutVar (tcl_tyvars lcl_env)
-       ; new_g_var  <- newMutVar (global_tvs `unionVarSet` extra_tvs)
-       ; return (lcl_env { tcl_tyvars = new_g_var
-                         , tcl_env = extendNameEnvList lcl_type_env tc_ty_things } ) }
-  where
-    extra_tvs = foldr get_tvs emptyVarSet tc_ty_things
-
-    get_tvs (_, ATcId { tct_id = id, tct_info = closed }) tvs
-      = case closed of
-          ClosedLet -> ASSERT2( is_closed_type, ppr id $$ ppr (idType id) )
-                       tvs
-          _other    -> tvs `unionVarSet` id_tvs
-        where
-           id_ty          = idType id
-           id_tvs         = tyCoVarsOfType id_ty
-           id_co_tvs      = closeOverKinds (coVarsOfType id_ty)
-           is_closed_type = not (anyVarSet isTyVar (id_tvs `minusVarSet` id_co_tvs))
-           -- We only care about being closed wrt /type/ variables
-           -- E.g. a top-level binding might have a type like
-           --          foo :: t |> co
-           -- where co :: * ~ *
-           -- or some other as-yet-unsolved kind coercion
-
-    get_tvs (_, ATyVar _ tv) tvs          -- See Note [Global TyVars]
-      = tvs `unionVarSet` tyCoVarsOfType (tyVarKind tv) `extendVarSet` tv
-
-    get_tvs (_, ATcTyCon tc) tvs = tvs `unionVarSet` tyCoVarsOfType (tyConKind tc)
-
-    get_tvs (_, AGlobal {})       tvs = tvs
-    get_tvs (_, APromotionErr {}) tvs = tvs
-
-        -- Note [Global TyVars]
-        -- It's important to add the in-scope tyvars to the global tyvar set
-        -- as well.  Consider
-        --      f (_::r) = let g y = y::r in ...
-        -- Here, g mustn't be generalised.  This is also important during
-        -- class and instance decls, when we mustn't generalise the class tyvars
-        -- when typechecking the methods.
-        --
-        -- Nor must we generalise g over any kind variables free in r's kind
-
+  = lcl_env { tcl_env = extendNameEnvList lcl_type_env tc_ty_things }
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 0f6f22c074..328290a2f8 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1849,7 +1849,7 @@ kcLHsQTyVars_Cusk name flav
 
        ; let inf_candidates = candidates `delCandidates` spec_req_tkvs
 
-       ; inferred <- quantifyTyVars emptyVarSet inf_candidates
+       ; inferred <- quantifyTyVars inf_candidates
                      -- NB: 'inferred' comes back sorted in dependency order
 
        ; scoped_kvs <- mapM zonkTyCoVarKind scoped_kvs
@@ -2289,26 +2289,24 @@ kindGeneralizeSome should_gen kind_or_type
          -- use the "Kind" variant here, as any types we see
          -- here will already have all type variables quantified;
          -- thus, every free variable is really a kv, never a tv.
-       ; dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) <- candidateQTyVarsOfKind kind_or_type
+       ; dvs <- candidateQTyVarsOfKind kind_or_type
 
-       ; let promote_kvs = filterVarSet (not . should_gen) $ dVarSetToVarSet kvs
-             promote_tvs = filterVarSet (not . should_gen) $ dVarSetToVarSet tvs
+       -- So 'dvs' are the variables free in kind_or_type, with a level greater
+       -- than the ambient level, hence candidates for quantification
+       -- Next: filter out the ones we don't want to generalize (specified by should_gen)
+       -- and promote them instead
 
-       ; (_, promoted) <- promoteTyVarSet (promote_kvs `unionVarSet` promote_tvs)
+       ; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen)
 
-       ; gbl_tvs <- tcGetGlobalTyCoVars  -- already zonked
-       ; let dvs' = dvs { dv_kvs = kvs `dVarSetMinusVarSet` promote_kvs
-                        , dv_tvs = tvs `dVarSetMinusVarSet` promote_tvs }
-       ; qkvs <- quantifyTyVars gbl_tvs dvs'
+       ; (_, promoted) <- promoteTyVarSet (dVarSetToVarSet to_promote)
+       ; qkvs <- quantifyTyVars dvs'
 
        ; traceTc "kindGeneralizeSome }" $
          vcat [ text "Kind or type:" <+> ppr kind_or_type
               , text "dvs:" <+> ppr dvs
               , text "dvs':" <+> ppr dvs'
-              , text "promote_kvs:" <+> pprTyVars (nonDetEltsUniqSet promote_kvs)
-              , text "promote_tvs:" <+> pprTyVars (nonDetEltsUniqSet promote_tvs)
+              , text "to_promote:" <+> pprTyVars (dVarSetElems to_promote)
               , text "promoted:" <+> pprTyVars (nonDetEltsUniqSet promoted)
-              , text "gbl_tvs:" <+> pprTyVars (nonDetEltsUniqSet gbl_tvs)
               , text "qkvs:" <+> pprTyVars qkvs ]
 
        ; return qkvs }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 198e9a258d..bc5e9ae244 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -820,7 +820,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
        -- check there too!
        ; let scoped_tvs = imp_tvs ++ exp_tvs
        ; dvs  <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
-       ; qtvs <- quantifyTyVars emptyVarSet dvs
+       ; qtvs <- quantifyTyVars dvs
 
        -- Zonk the patterns etc into the Type world
        ; (ze, qtvs)   <- zonkTyBndrs qtvs
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 2953a466ad..a0297c61f5 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -69,9 +69,9 @@ module TcMType (
   zonkTyCoVarsAndFVList,
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
-  CandidatesQTvs(..), delCandidates, candidateKindVars,
+  CandidatesQTvs(..), delCandidates, candidateKindVars, partitionCandidates,
   zonkAndSkolemise, skolemiseQuantifiedTyVar,
-  defaultTyVar, quantifyTyVars,
+  defaultTyVar, quantifyTyVars, isQuantifiableTv,
   zonkTcType, zonkTcTypes, zonkCo,
   zonkTyCoVarKind,
 
@@ -79,7 +79,6 @@ module TcMType (
   zonkId, zonkCoVar,
   zonkCt, zonkSkolemInfo,
 
-  tcGetGlobalTyCoVars,
   skolemiseUnboundMetaTyVar,
 
   ------------------------------
@@ -1029,14 +1028,17 @@ quantify over /kind/ variables when -XPolyKinds is on.  Without -XPolyKinds
 we default the kind variables to *.
 
 So, to support this defaulting, and only for that reason, when
-collecting the free vars of a type, prior to quantifying, we must keep
-the type and kind variables separate.
+collecting the free vars of a type (in candidateQTyVarsOfType and friends),
+prior to quantifying, we must keep the type and kind variables separate.
 
 But what does that mean in a system where kind variables /are/ type
 variables? It's a fairly arbitrary distinction based on how the
 variables appear:
 
   - "Kind variables" appear in the kind of some other free variable
+    or in the kind of a locally quantified type variable
+    (forall (a :: kappa). ...) or in the kind of a coercion
+    (a |> (co :: kappa1 ~ kappa2)).
 
      These are the ones we default to * if -XPolyKinds is off
 
@@ -1136,7 +1138,7 @@ That level must be strictly greater than the ambient TcLevel in order
 to treat it as naughty. We say "strictly greater than" because the call to
 candidateQTyVars is made outside the bumped TcLevel, as stated in the
 comment to candidateQTyVarsOfType. The level check is done in go_tv
-in collect_cant_qtvs. Skipping this check caused #16517.
+in collect_cand_qtvs. Skipping this check caused #16517.
 
 -}
 
@@ -1146,10 +1148,17 @@ data CandidatesQTvs
   --
   -- Invariants:
   --   * All variables are fully zonked, including their kinds
+  --   * All variables are at a level greater than the ambient level
+  --     See Note [Use level numbers for quantification]
   --
   -- This *can* contain skolems. For example, in `data X k :: k -> Type`
   -- we need to know that the k is a dependent variable. This is done
-  -- by collecting the candidates in the kind.
+  -- by collecting the candidates in the kind after skolemising. It also
+  -- comes up when generalizing a associated type instance, where instance
+  -- variables are skolems. (Recall that associated type instances are generalized
+  -- independently from their enclosing class instance, and the associated
+  -- type instance may be generalized by more, fewer, or different variables
+  -- than the class instance.)
   --
   = DV { dv_kvs :: DTyVarSet    -- "kind" metavariables (dependent)
        , dv_tvs :: DTyVarSet    -- "type" metavariables (non-dependent)
@@ -1159,9 +1168,8 @@ data CandidatesQTvs
          -- See Note [Dependent type variables]
 
        , dv_cvs :: CoVarSet
-         -- These are covars. We will *not* quantify over these, but
-         -- we must make sure also not to quantify over any cv's kinds,
-         -- so we include them here as further direction for quantifyTyVars
+         -- These are covars. Included only so that we don't repeatedly
+         -- look at covars' kinds in accumulator. Not used by quantifyTyVars.
     }
 
 instance Semi.Semigroup CandidatesQTvs where
@@ -1185,6 +1193,14 @@ instance Outputable CandidatesQTvs where
 candidateKindVars :: CandidatesQTvs -> TyVarSet
 candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
 
+partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (DTyVarSet, CandidatesQTvs)
+partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
+  = (extracted, dvs { dv_kvs = rest_kvs, dv_tvs = rest_tvs })
+  where
+    (extracted_kvs, rest_kvs) = partitionDVarSet pred kvs
+    (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs
+    extracted = extracted_kvs `unionDVarSet` extracted_tvs
+
 -- | Gathers free variables to use as quantification candidates (in
 -- 'quantifyTyVars'). This might output the same var
 -- in both sets, if it's used in both a type and a kind.
@@ -1282,28 +1298,33 @@ collect_cand_qtvs is_dep bound dvs ty
                  -- (which comes next) works correctly
 
            ; cur_lvl <- getTcLevel
-           ; if tcTyVarLevel tv `strictlyDeeperThan` cur_lvl &&
-                   -- this tyvar is from an outer context: see Wrinkle
-                   -- in Note [Naughty quantification candidates]
-
-                intersectsVarSet bound (tyCoVarsOfType tv_kind)
-
-             then -- See Note [Naughty quantification candidates]
-                  do { traceTc "Zapping naughty quantifier" $
-                         vcat [ ppr tv <+> dcolon <+> ppr tv_kind
-                              , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound)
-                              , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $
-                                                           tyCoVarsOfType tv_kind) ]
-
-                     ; writeMetaTyVar tv (anyTypeOfKind tv_kind)
-                     ; collect_cand_qtvs True bound dv tv_kind }
-
-             else do { let tv' = tv `setTyVarKind` tv_kind
-                           dv' | is_dep    = dv { dv_kvs = kvs `extendDVarSet` tv' }
-                               | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' }
-                               -- See Note [Order of accumulation]
-                     ; collect_cand_qtvs True emptyVarSet dv' tv_kind } }
-            -- Why emptyVarSet? See Note [Closing over free variable kinds] in TyCoRep
+           ; if |  tcTyVarLevel tv <= cur_lvl
+                -> return dv   -- this variable is from an outer context; skip
+                               -- See Note [Use level numbers ofor quantification]
+
+                |  intersectsVarSet bound (tyCoVarsOfType tv_kind)
+                   -- the tyvar must not be from an outer context, but we have
+                   -- already checked for this.
+                   -- See Note [Naughty quantification candidates]
+                -> do { traceTc "Zapping naughty quantifier" $
+                          vcat [ ppr tv <+> dcolon <+> ppr tv_kind
+                               , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound)
+                               , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $
+                                                            tyCoVarsOfType tv_kind) ]
+
+                      ; writeMetaTyVar tv (anyTypeOfKind tv_kind)
+
+                      -- See Note [Recurring into kinds for candidateQTyVars]
+                      ; collect_cand_qtvs True bound dv tv_kind }
+
+                |  otherwise
+                -> do { let tv' = tv `setTyVarKind` tv_kind
+                            dv' | is_dep    = dv { dv_kvs = kvs `extendDVarSet` tv' }
+                                | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' }
+                                -- See Note [Order of accumulation]
+
+                        -- See Note [Recurring into kinds for candidateQTyVars]
+                      ; collect_cand_qtvs True bound dv' tv_kind } }
 
 collect_cand_qtvs_co :: VarSet -- bound variables
                      -> CandidatesQTvs -> Coercion
@@ -1329,19 +1350,11 @@ collect_cand_qtvs_co bound = go_co
     go_co dv (KindCo co)           = go_co dv co
     go_co dv (SubCo co)            = go_co dv co
 
-    go_co dv@(DV { dv_cvs = cvs }) (HoleCo hole)
+    go_co dv (HoleCo hole)
       = do m_co <- unpackCoercionHole_maybe hole
            case m_co of
              Just co -> go_co dv co
-             Nothing
-               | cv `elemVarSet` cvs -> return dv
-
-               | otherwise
-               -> collect_cand_qtvs True bound (dv { dv_cvs = cvs `extendVarSet` cv })
-                                                     cv_type
-                        -- See Note [Free vars in coercion hole]
-               where cv      = coHoleCoVar hole
-                     cv_type = varType cv
+             Nothing -> go_cv dv (coHoleCoVar hole)
 
     go_co dv (CoVarCo cv) = go_cv dv cv
 
@@ -1362,8 +1375,8 @@ collect_cand_qtvs_co bound = go_co
       | is_bound cv         = return dv
       | cv `elemVarSet` cvs = return dv
 
-      -- Why emptyVarSet below? See Note [Closing over free variable kinds] in TyCoRep
-      | otherwise           = collect_cand_qtvs True emptyVarSet
+        -- See Note [Recurring into kinds for candidateQTyVars]
+      | otherwise           = collect_cand_qtvs True bound
                                     (dv { dv_cvs = cvs `extendVarSet` cv })
                                     (idType cv)
 
@@ -1389,35 +1402,42 @@ element to the right.
 Note that the unitDVarSet/mappend implementation would not be wrong
 against any specification -- just suboptimal and confounding to users.
 
-Note [Free vars in coercion hole]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-First, read Note [Closing over free variable kinds] in TyCoRep, paying
+Note [Recurring into kinds for candidateQTyVars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+First, read Note [Closing over free variable kinds] in TyCoFVs, paying
 attention to the end of the Note about using an empty bound set when
 traversing a variable's kind.
 
-We do not do this for coercion holes. (The other Note doesn't address coercion
-holes, because that Note is about Core, where coercion holes do not exist.)
-Coercion holes are *never* bound. Yet a coercion hole *can* mention a locally
-bound type/coercion variable in its kind. This would happen if the constraint
-associated with the coercion hole is inside an implication constraint, and the
-bound variables in the hole's type are the skolems of the implication. We do
-not want to collect *all* free variables in the coercion hole's kind, because
-that list might contain skolems. (This actually happened in test case
-dependent/should_fail/BadTelescope5.) Instead, we remember the bound variables
-when traversing the coercion hole's kind so we can avoid visiting bound
-variables there.
-
-Example: forall k1 k2. .... |> (hole :: k1 ~# k2) ....
-This is obviously bogus, but if we collect k1 and k2 into the candidates,
-we'll have skolems in the CandidatesQTvs, directly contradicting that data
-structure's invariant. See its definition.
-
-Of course, Note [Closing over free variable kinds] observes that maintaining
-a bound set while going into a kind is potentially wrong, if there is shadowing.
-However, given that we are in the type-checker now, not in Core, shadowing cannot
-happen: the renamer would have sorted it out. So the bug that Note is fixing
-cannot occur here, and so we do not have to zap the bound set when looking at
-kinds.
+That Note concludes with the recommendation that we empty out the bound
+set when recurring into the kind of a type variable. Yet, we do not do
+this here. I have two tasks in order to convince you that this code is
+right. First, I must show why it is safe to ignore the reasoning in that
+Note. Then, I must show why is is necessary to contradict the reasoning in
+that Note.
+
+Why it is safe: There can be no
+shadowing in the candidateQ... functions: they work on the output of
+type inference, which is seeded by the renamer and its insistence to
+use different Uniques for different variables. (In contrast, the Core
+functions work on the output of optimizations, which may introduce
+shadowing.) Without shadowing, the problem studied by
+Note [Closing over free variable kinds] in TyCoFVs cannot happen.
+
+Why it is necessary:
+Wiping the bound set would be just plain wrong here. Consider
+
+  forall k1 k2 (a :: k1). Proxy k2 (a |> (hole :: k1 ~# k2))
+
+We really don't want to think k1 and k2 are free here. (It's true that we'll
+never be able to fill in `hole`, but we don't want to go off the rails just
+because we have an insoluble coercion hole.) So: why is it wrong to wipe
+the bound variables here but right in Core? Because the final statement
+in Note [Closing over free variable kinds] in TyCoFVs is wrong: not
+every variable is either free or bound. A variable can be a hole, too!
+The reasoning in that Note then breaks down.
+
+And the reasoning applies just as well to free non-hole variables, so we
+retain the bound set always.
 
 -}
 
@@ -1433,17 +1453,8 @@ quantifyTyVars is given the free vars of a type that we
 are about to wrap in a forall.
 
 It takes these free type/kind variables (partitioned into dependent and
-non-dependent variables) and
-  1. Zonks them and remove globals and covars
-  2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
-  3. Calls skolemiseQuantifiedTyVar on each
-
-Step (2) is often unimportant, because the kind variable is often
-also free in the type.  Eg
-     Typeable k (a::k)
-has free vars {k,a}.  But the type (see #7916)
-    (f::k->*) (a::k)
-has free vars {f,a}, but we must add 'k' as well! Hence step (2).
+non-dependent variables) skolemises metavariables with a TcLevel greater
+than the ambient level (see Note [Use level numbers of quantification]).
 
 * This function distinguishes between dependent and non-dependent
   variables only to keep correct defaulting behavior with -XNoPolyKinds.
@@ -1453,6 +1464,48 @@ has free vars {f,a}, but we must add 'k' as well! Hence step (2).
     - a coercion variable (or any tv mentioned in the kind of a covar)
     - a runtime-rep variable
 
+Note [Use level numbers for quantification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The level numbers assigned to metavariables are very useful. Not only
+do they track touchability (Note [TcLevel and untouchable type variables]
+in TcType), but they also allow us to determine which variables to
+generalise. The rule is this:
+
+  When generalising, quantify only metavariables with a TcLevel greater
+  than the ambient level.
+
+This works because we bump the level every time we go inside a new
+source-level construct. In a traditional generalisation algorithm, we
+would gather all free variables that aren't free in an environment.
+However, if a variable is in that environment, it will always have a lower
+TcLevel: it came from an outer scope. So we can replace the "free in
+environment" check with a level-number check.
+
+Here is an example:
+
+  f x = x + (z True)
+    where
+      z y = x * x
+
+We start by saying (x :: alpha[1]). When inferring the type of z, we'll
+quickly discover that z :: alpha[1]. But it would be disastrous to
+generalise over alpha in the type of z. So we need to know that alpha
+comes from an outer environment. By contrast, the type of y is beta[2],
+and we are free to generalise over it. What's the difference between
+alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for
+generalisation, and so we generalise it. alpha[1] does not, and so
+we leave it alone.
+
+Note that not *every* variable with a higher level will get generalised,
+either due to the monomorphism restriction or other quirks. See, for
+example, the code in TcSimplify.decideMonoTyVars and in
+TcHsType.kindGeneralizeSome, both of which exclude certain otherwise-eligible
+variables from being generalised.
+
+Using level numbers for quantification is implemented in the candidateQTyVars...
+functions, by adding only those variables with a level strictly higher than
+the ambient level to the set of candidates.
+
 Note [quantifyTyVars determinism]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The results of quantifyTyVars are wrapped in a forall and can end up in the
@@ -1468,15 +1521,17 @@ Note [Deterministic UniqFM] in UniqDFM.
 -}
 
 quantifyTyVars
-  :: TcTyCoVarSet     -- Global tvs; already zonked
-  -> CandidatesQTvs   -- See Note [Dependent type variables]
+  :: CandidatesQTvs   -- See Note [Dependent type variables]
                       -- Already zonked
   -> TcM [TcTyVar]
 -- See Note [quantifyTyVars]
 -- Can be given a mixture of TcTyVars and TyVars, in the case of
 --   associated type declarations. Also accepts covars, but *never* returns any.
-quantifyTyVars gbl_tvs
-               dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs, dv_cvs = covars })
+-- According to Note [Use level numbers for quantification] and the
+-- invariants on CandidateQTvs, we do not have to filter out variables
+-- free in the environment here. Just quantify unconditionally, subject
+-- to the restrictions in Note [quantifyTyVars].
+quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
        -- short-circuit common case
   | isEmptyDVarSet dep_tkvs
   , isEmptyDVarSet nondep_tkvs
@@ -1484,53 +1539,21 @@ quantifyTyVars gbl_tvs
        ; return [] }
 
   | otherwise
-  = do { outer_tclvl <- getTcLevel
-       ; traceTc "quantifyTyVars 1" (vcat [ppr outer_tclvl, ppr dvs, ppr gbl_tvs])
-       ; let co_tvs = closeOverKinds covars
-             mono_tvs = gbl_tvs `unionVarSet` co_tvs
-              -- NB: All variables in the kind of a covar must not be
-              -- quantified over, as we don't quantify over the covar.
-
-             dep_kvs = scopedSort $ dVarSetElems $
-                       dep_tkvs `dVarSetMinusVarSet` mono_tvs
+  = do { traceTc "quantifyTyVars 1" (ppr dvs)
+
+       ; let dep_kvs     = scopedSort $ dVarSetElems dep_tkvs
                        -- scopedSort: put the kind variables into
                        --    well-scoped order.
                        --    E.g.  [k, (a::k)] not the other way roud
 
-             nondep_tvs = dVarSetElems $
-                          (nondep_tkvs `minusDVarSet` dep_tkvs)
-                           `dVarSetMinusVarSet` mono_tvs
+             nondep_tvs  = dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs)
                  -- See Note [Dependent type variables]
                  -- The `minus` dep_tkvs removes any kind-level vars
                  --    e.g. T k (a::k)   Since k appear in a kind it'll
                  --    be in dv_kvs, and is dependent. So remove it from
                  --    dv_tvs which will also contain k
-                 -- No worry about dependent covars here;
-                 --    they are all in dep_tkvs
                  -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
 
-       -- This block uses level numbers to decide what to quantify
-       -- and emits a warning if the two methods do not give the same answer
-       ; let dep_kvs2    = scopedSort $ dVarSetElems $
-                           filterDVarSet (quantifiableTv outer_tclvl) dep_tkvs
-             nondep_tvs2 = filter (quantifiableTv outer_tclvl) $
-                           dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs)
-
-             all_ok = dep_kvs == dep_kvs2 && nondep_tvs == nondep_tvs2
-             bad_msg = hang (text "Quantification by level numbers would fail")
-                          2 (vcat [ text "Outer level =" <+> ppr outer_tclvl
-                                  , text "gbl_tvs ="     <+> ppr gbl_tvs
-                                  , text "mono_tvs ="    <+> ppr mono_tvs
-                                  , text "dep_tkvs ="    <+> ppr dep_tkvs
-                                  , text "co_vars ="     <+> vcat [ ppr cv <+> dcolon <+> ppr (varType cv)
-                                                                  | cv <- nonDetEltsUniqSet covars ]
-                                  , text "co_tvs ="      <+> ppr co_tvs
-                                  , text "dep_kvs ="     <+> ppr dep_kvs
-                                  , text "dep_kvs2 ="    <+> ppr dep_kvs2
-                                  , text "nondep_tvs ="  <+> ppr nondep_tvs
-                                  , text "nondep_tvs2 =" <+> ppr nondep_tvs2 ])
-       ; MASSERT2( all_ok, bad_msg )
-
              -- In the non-PolyKinds case, default the kind variables
              -- to *, and zonk the tyvars as usual.  Notice that this
              -- may make quantifyTyVars return a shorter list
@@ -1544,9 +1567,7 @@ quantifyTyVars gbl_tvs
            -- now refer to the dep_kvs'
 
        ; traceTc "quantifyTyVars 2"
-           (vcat [ text "globals:"    <+> ppr gbl_tvs
-                 , text "mono_tvs:"   <+> ppr mono_tvs
-                 , text "nondep:"     <+> pprTyVars nondep_tvs
+           (vcat [ text "nondep:"     <+> pprTyVars nondep_tvs
                  , text "dep:"        <+> pprTyVars dep_kvs
                  , text "dep_kvs'"    <+> pprTyVars dep_kvs'
                  , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
@@ -1578,10 +1599,10 @@ quantifyTyVars gbl_tvs
                False -> do { tv <- skolemiseQuantifiedTyVar tkv
                            ; return (Just tv) } }
 
-quantifiableTv :: TcLevel   -- Level of the context, outside the quantification
-               -> TcTyVar
-               -> Bool
-quantifiableTv outer_tclvl tcv
+isQuantifiableTv :: TcLevel   -- Level of the context, outside the quantification
+                 -> TcTyVar
+                 -> Bool
+isQuantifiableTv outer_tclvl tcv
   | isTcTyVar tcv  -- Might be a CoVar; change this when gather covars separately
   = tcTyVarLevel tcv > outer_tclvl
   | otherwise
@@ -1859,22 +1880,6 @@ a \/\a in the final result but all the occurrences of a will be zonked to ()
 
 -}
 
--- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
--- the environment. To improve subsequent calls to the same function it writes
--- the zonked set back into the environment. Note that this returns all
--- variables free in anything (term-level or type-level) in scope. We thus
--- don't have to worry about clashes with things that are not in scope, because
--- if they are reachable, then they'll be returned here.
--- NB: This is closed over kinds, so it can return unification variables mentioned
--- in the kinds of in-scope tyvars.
-tcGetGlobalTyCoVars :: TcM TcTyVarSet
-tcGetGlobalTyCoVars
-  = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
-       ; gbl_tvs  <- readMutVar gtv_var
-       ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
-       ; writeMutVar gtv_var gbl_tvs'
-       ; return gbl_tvs' }
-
 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
 -- Zonk a type and take its free variables
 -- With kind polymorphism it can be essential to zonk *first*
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index d4ff73d566..2fd8359477 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -1888,7 +1888,8 @@ runTcInteractive hsc_env thing_inside
                          , tcg_imports      = imports
                          }
 
-       ; lcl_env' <- tcExtendLocalTypeEnv lcl_env lcl_ids
+             lcl_env' = tcExtendLocalTypeEnv lcl_env lcl_ids
+
        ; setEnvs (gbl_env', lcl_env') thing_inside }
   where
     (home_insts, home_fam_insts) = hptInstances hsc_env (\_ -> True)
@@ -1930,9 +1931,8 @@ types have free RuntimeUnk skolem variables, standing for unknown
 types.  If we don't register these free TyVars as global TyVars then
 the typechecker will try to quantify over them and fall over in
 skolemiseQuantifiedTyVar. so we must add any free TyVars to the
-typechecker's global TyVar set.  That is most conveniently by using
-tcExtendLocalTypeEnv, which automatically extends the global TyVar
-set.
+typechecker's global TyVar set.  That is done by using
+tcExtendLocalTypeEnv.
 
 We do this by splitting out the Ids with open types, using 'is_closed'
 to do the partition.  The top-level things go in the global TypeEnv;
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index 48d8cae841..dfc80ed764 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -331,8 +331,7 @@ initTcWithGbl :: HscEnv
               -> TcM r
               -> IO (Messages, Maybe r)
 initTcWithGbl hsc_env gbl_env loc do_this
- = do { tvs_var      <- newIORef emptyVarSet
-      ; lie_var      <- newIORef emptyWC
+ = do { lie_var      <- newIORef emptyWC
       ; errs_var     <- newIORef (emptyBag, emptyBag)
       ; let lcl_env = TcLclEnv {
                 tcl_errs       = errs_var,
@@ -344,7 +343,6 @@ initTcWithGbl hsc_env gbl_env loc do_this
                 tcl_arrow_ctxt = NoArrowCtxt,
                 tcl_env        = emptyNameEnv,
                 tcl_bndrs      = [],
-                tcl_tyvars     = tvs_var,
                 tcl_lie        = lie_var,
                 tcl_tclvl      = topTcLevel
                 }
@@ -1667,8 +1665,7 @@ setLclTypeEnv :: TcLclEnv -> TcM a -> TcM a
 setLclTypeEnv lcl_env thing_inside
   = updLclEnv upd thing_inside
   where
-    upd env = env { tcl_env = tcl_env lcl_env,
-                    tcl_tyvars = tcl_tyvars lcl_env }
+    upd env = env { tcl_env = tcl_env lcl_env }
 
 traceTcConstraints :: String -> TcM ()
 traceTcConstraints msg
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 0a2db75a2d..cd3bf5c1a5 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -833,12 +833,6 @@ data TcLclEnv           -- Changes as we move inside an expression
         tcl_bndrs :: TcBinderStack,   -- Used for reporting relevant bindings,
                                       -- and for tidying types
 
-        tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
-                        -- Namely, the in-scope TyVars bound in tcl_env,
-                        -- plus the tyvars mentioned in the types of Ids bound
-                        -- in tcl_lenv.
-                        -- Why mutable? see notes with tcGetGlobalTyCoVars
-
         tcl_lie  :: TcRef WantedConstraints,    -- Place to accumulate type constraints
         tcl_errs :: TcRef Messages              -- Place to accumulate errors
     }
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index b60bbd2e5a..4146c8900c 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -110,12 +110,10 @@ tcRule (HsRule { rd_ext  = ext
        -- during zonking (see TcHsSyn.zonkRule)
 
        ; let tpl_ids = lhs_evs ++ id_bndrs
-       ; gbls  <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
-                                      -- monomorphic bindings from the MR; test tc111
        ; forall_tkvs <- candidateQTyVarsOfTypes $
                         map (mkSpecForAllTys tv_bndrs) $  -- don't quantify over lexical tyvars
                         rule_ty : map idType tpl_ids
-       ; qtkvs <- quantifyTyVars gbls forall_tkvs
+       ; qtkvs <- quantifyTyVars forall_tkvs
        ; traceTc "tcRule" (vcat [ pprFullRuleName rname
                                 , ppr forall_tkvs
                                 , ppr qtkvs
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 18f2c505d9..3534757af1 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -764,9 +764,8 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
               psig_theta  = [ pred | sig <- partial_sigs
                                    , pred <- sig_inst_theta sig ]
 
-       ; gbl_tvs <- tcGetGlobalTyCoVars
        ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)
-       ; qtkvs <- quantifyTyVars gbl_tvs dep_vars
+       ; qtkvs <- quantifyTyVars dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
        ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) }
 
@@ -1029,7 +1028,7 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
        ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 
        -- Step 3: decide which kind/type variables to quantify over
-       ; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+       ; qtvs <- decideQuantifiedTyVars name_taus psigs candidates
 
        -- Step 4: choose which of the remaining candidate
        --         predicates to actually quantify over
@@ -1081,7 +1080,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
 
        ; taus <- mapM (TcM.zonkTcType . snd) name_taus
 
-       ; mono_tvs0 <- tcGetGlobalTyCoVars
+       ; tc_lvl <- TcM.getTcLevel
        ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
 
              co_vars = coVarsOfTypes (psig_tys ++ taus)
@@ -1092,19 +1091,34 @@ decideMonoTyVars infer_mode name_taus psigs candidates
                -- E.g.  If we can't quantify over co :: k~Type, then we can't
                --       quantify over k either!  Hence closeOverKinds
 
+             mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
+                         tyCoVarsOfTypes candidates
+               -- We need to grab all the non-quantifiable tyvars in the
+               -- candidates so that we can grow this set to find other
+               -- non-quantifiable tyvars. This can happen with something
+               -- like
+               --    f x y = ...
+               --      where z = x 3
+               -- The body of z tries to unify the type of x (call it alpha[1])
+               -- with (beta[2] -> gamma[2]). This unification fails because
+               -- alpha is untouchable. But we need to know not to quantify over
+               -- beta or gamma, because they are in the equality constraint with
+               -- alpha. Actual test case: typecheck/should_compile/tc213
+
              mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
 
              eq_constraints = filter isEqPrimPred candidates
              mono_tvs2      = growThetaTyVars eq_constraints mono_tvs1
 
-             constrained_tvs = (growThetaTyVars eq_constraints
+             constrained_tvs = filterVarSet (isQuantifiableTv tc_lvl) $
+                               (growThetaTyVars eq_constraints
                                                (tyCoVarsOfTypes no_quant)
                                 `minusVarSet` mono_tvs2)
                                `delVarSetList` psig_qtvs
              -- constrained_tvs: the tyvars that we are not going to
-             -- quantify solely because of the moonomorphism restriction
+             -- quantify solely because of the monomorphism restriction
              --
-             -- (`minusVarSet` mono_tvs1`): a type variable is only
+             -- (`minusVarSet` mono_tvs2`): a type variable is only
              --   "constrained" (so that the MR bites) if it is not
              --   free in the environment (#13785)
              --
@@ -1126,7 +1140,6 @@ decideMonoTyVars infer_mode name_taus psigs candidates
 
        ; traceTc "decideMonoTyVars" $ vcat
            [ text "mono_tvs0 =" <+> ppr mono_tvs0
-           , text "mono_tvs1 =" <+> ppr mono_tvs1
            , text "no_quant =" <+> ppr no_quant
            , text "maybe_quant =" <+> ppr maybe_quant
            , text "eq_constraints =" <+> ppr eq_constraints
@@ -1215,13 +1228,12 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 
 ------------------
 decideQuantifiedTyVars
-   :: TyCoVarSet        -- Monomorphic tyvars
-   -> [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
+   :: [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
    -> [TcIdSigInst]     -- Partial signatures
    -> [PredType]        -- Candidates, zonked
    -> TcM [TyVar]
 -- Fix what tyvars we are going to quantify over, and quantify them
-decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+decideQuantifiedTyVars name_taus psigs candidates
   = do {     -- Why psig_tys? We try to quantify over everything free in here
              -- See Note [Quantification and partial signatures]
              --     Wrinkles 2 and 3
@@ -1230,7 +1242,6 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
        ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
                                                   , pred <- sig_inst_theta sig ]
        ; tau_tys  <- mapM (TcM.zonkTcType . snd) name_taus
-       ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
 
        ; let -- Try to quantify over variables free in these types
              psig_tys = psig_tv_tys ++ psig_theta
@@ -1258,7 +1269,7 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
            , text "grown_tcvs =" <+> ppr grown_tcvs
            , text "dvs =" <+> ppr dvs_plus])
 
-       ; quantifyTyVars mono_tvs dvs_plus }
+       ; quantifyTyVars dvs_plus }
 
 ------------------
 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index fbb26b103f..36d5807495 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -604,7 +604,7 @@ generaliseTcTyCon tc
 
        -- Step 2b: quantify, mainly meaning skolemise the free variables
        -- Returned 'inferred' are scope-sorted and skolemised
-       ; inferred <- quantifyTyVars emptyVarSet dvs2
+       ; inferred <- quantifyTyVars dvs2
 
        -- Step 3a: rename all the Specified and Required tyvars back to
        -- TyVars with their oroginal user-specified name.  Example
@@ -2320,7 +2320,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
        -- check there too!
        ; let scoped_tvs = imp_tvs ++ exp_tvs
        ; dvs  <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
-       ; qtvs <- quantifyTyVars emptyVarSet dvs
+       ; qtvs <- quantifyTyVars dvs
 
        ; (ze, qtvs) <- zonkTyBndrs qtvs
        ; lhs_ty     <- zonkTcTypeToTypeX ze lhs_ty
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 31e5c8c4e7..d03d0dc32b 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,13 +1,13 @@
 
 T14040a.hs:34:8: error:
-    • Cannot apply expression of type ‘Sing wl0
-                                       -> (forall y. p0 _0 'WeirdNil)
+    • Cannot apply expression of type ‘Sing wl
+                                       -> (forall y. p _0 'WeirdNil)
                                        -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
                                            Sing x
                                            -> Sing xs
-                                           -> p0 GHC.Types.Any xs
-                                           -> p0 GHC.Types.Any ('WeirdCons x xs))
-                                       -> p0 GHC.Types.Any wl0’
+                                           -> p GHC.Types.Any xs
+                                           -> p GHC.Types.Any ('WeirdCons x xs))
+                                       -> p _1 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
diff --git a/testsuite/tests/typecheck/should_compile/tc213.hs b/testsuite/tests/typecheck/should_compile/tc213.hs
index 43bba76526..d5f1ea374f 100644
--- a/testsuite/tests/typecheck/should_compile/tc213.hs
+++ b/testsuite/tests/typecheck/should_compile/tc213.hs
@@ -34,8 +34,14 @@ instance Ix key => Mark (ST s) (STUArray s key Bool) key where
      seen  s   = liftM (map fst . filter snd) (getAssocs s)
 
 -- traversing the hull suc^*(start) with loop detection
+-- trav :: forall f f2 m store key.
+--        (Foldable f, Foldable f2, Mark m store key, Monad m)
+--     => (key -> f key) -> f2 key -> (key, key) -> m store
 trav suc start i = new i >>= \ c -> mapM_ (compo c) start >> return c
-     where compo c x = markQ c x >>= flip unless (visit c x)
+     where -- compo :: (Monad m, Mark m store' key) => store' -> key -> m ()
+           compo c x = markQ c x >>= flip unless (visit c x)
+
+           -- visit :: (Monad m, Mark m store' key) => store' -> key -> m ()
            visit c x = mark c x >> mapM_ (compo c) (suc x)
 
 -- sample graph