Refactor kindGeneralize and friends

This commit should have no change in behavior.(*)

The observation was that Note [Recipe for checking a signature]
says that every metavariable in a type-checked type must either
  (A) be generalized
  (B) be promoted
  (C) be zapped.
Yet the code paths for doing these were all somewhat separate.
This led to some steps being skipped. This commit shores this
all up. The key innovation is TcHsType.kindGeneralizeSome, with
appropriate commentary.

This commit also sets the stage for #15809, by turning the
WARNing about bad level-numbers in generalisation into an
ASSERTion. The actual fix for #15809 will be in a separate
commit.

Other changes:
 * zonkPromoteType is now replaced by kindGeneralizeNone.
   This might have a small performance degradation, because
   zonkPromoteType zonked and promoted all at once. The new
   code path promotes first, and then zonks.

 * A call to kindGeneralizeNone was added in tcHsPartialSigType.
   I think this was a lurking bug, because it did not follow
   Note [Recipe for checking a signature]. I did not try to
   come up with an example showing the bug. This is the (*)
   above.

   Because of this change, there is an error message regression
   in partial-sigs/should_fail/T14040a. This problem isn't really
   a direct result of this refactoring, but is a symptom of
   something deeper. See #16775, which addresses the deeper
   problem.

 * I added a short-cut to quantifyTyVars, in case there's
   nothing to quantify.

 * There was a horribly-outdated Note that wasn't referred
   to. Gone now.

 * While poking around with T14040a, I discovered a small
   mistake in the Coercion.simplifyArgsWorker. Easy to fix,
   happily.

 * See new Note [Free vars in coercion hole] in TcMType.
   Previously, we were doing the wrong thing when looking
   at a coercion hole in the gather-candidates algorithm.
   Fixed now, with lengthy explanation.

Metric Decrease:
  T14683

9 files changed, 280 insertions, 224 deletions

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 946392f2d9..c575cb572c 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1553,7 +1553,7 @@ flatten_tyvar1 tv
                              (ppr tv <+> equals <+> ppr ty)
                          ; role <- getRole
                          ; return (FTRFollowed ty (mkReflCo role ty)) } ;
-           Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
+           Nothing -> do { traceFlat "Unfilled tyvar" (pprTyVar tv)
                          ; fr <- getFlavourRole
                          ; flatten_tyvar2 tv fr } }
 
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index dd6357ef68..0f6f22c074 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -47,14 +47,12 @@ module TcHsType (
 
         typeLevelMode, kindLevelMode,
 
-        kindGeneralize, checkExpectedKind_pp,
+        kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
+        checkExpectedKind_pp,
 
         -- Sort-checking kinds
         tcLHsKindSig, checkDataKindSig, DataSort(..),
 
-        -- Zonking and promoting
-        zonkPromoteType,
-
         -- Pattern type signatures
         tcHsPatSigType, tcPatSig,
 
@@ -83,7 +81,6 @@ import Inst   ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
 import TyCoRep( TyCoBinder(..) )  -- Used in etaExpandAlgTyCon
 import Type
 import TysPrim
-import Coercion
 import RdrName( lookupLocalRdrOcc )
 import Var
 import VarSet
@@ -266,7 +263,15 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
 
        ; spec_tkvs <- zonkAndScopedSort spec_tkvs
        ; let ty1 = mkSpecForAllTys spec_tkvs ty
-       ; kvs <- kindGeneralizeLocal wanted ty1
+
+       -- This bit is very much like decideMonoTyVars in TcSimplify,
+       -- but constraints are so much simpler in kinds, it is much
+       -- easier here. (In particular, we never quantify over a
+       -- constraint in a type.)
+       ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
+       ; let should_gen = not . (`elemVarSet` constrained)
+
+       ; kvs <- kindGeneralizeSome should_gen ty1
        ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
                                   tc_lvl wanted
 
@@ -292,7 +297,7 @@ tcTopLHsType hs_sig_type ctxt_kind
 
        ; spec_tkvs <- zonkAndScopedSort spec_tkvs
        ; let ty1 = mkSpecForAllTys spec_tkvs ty
-       ; kvs <- kindGeneralize ty1
+       ; kvs <- kindGeneralizeAll ty1  -- "All" because it's a top-level type
        ; final_ty <- zonkTcTypeToType (mkInvForAllTys kvs ty1)
        ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
        ; return final_ty}
@@ -375,13 +380,13 @@ tcHsTypeApp wc_ty kind
                -- See Note [Wildcards in visible type application]
                tcNamedWildCardBinders sig_wcs $ \ _ ->
                tcCheckLHsType hs_ty kind
-       -- We must promote here. Ex:
-       --   f :: forall a. a
-       --   g = f @(forall b. Proxy b -> ()) @Int ...
-       -- After when processing the @Int, we'll have to check its kind
-       -- against the as-yet-unknown kind of b. This check causes an assertion
-       -- failure if we don't promote.
-       ; ty <- zonkPromoteType ty
+       -- We do not kind-generalize type applications: we just
+       -- instantiate with exactly what the user says.
+       -- See Note [No generalization in type application]
+       -- We still must call kindGeneralizeNone, though, according
+       -- to Note [Recipe for checking a signature]
+       ; kindGeneralizeNone ty
+       ; ty <- zonkTcType ty
        ; checkValidType TypeAppCtxt ty
        ; return ty }
 tcHsTypeApp (XHsWildCardBndrs nec) _ = noExtCon nec
@@ -401,6 +406,22 @@ constraints on it.  See related Note [Wildcards in visible kind
 application] and Note [The wildcard story for types] in HsTypes.hs
 
 Ugh!
+
+Note [No generalization in type application]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We do not kind-generalize type applications. Imagine
+
+  id @(Proxy Nothing)
+
+If we kind-generalized, we would get
+
+  id @(forall {k}. Proxy @(Maybe k) (Nothing @k))
+
+which is very sneakily impredicative instantiation.
+
+There is also the possibility of mentioning a wildcard
+(`id @(Proxy _)`), which definitely should not be kind-generalized.
+
 -}
 
 {-
@@ -1664,10 +1685,9 @@ Checking a user-written signature requires several steps:
 
  1. Generate constraints.
  2. Solve constraints.
- 3. Zonk.
- 4. Promote tyvars and/or kind-generalize.
- 5. Zonk.
- 6. Check validity.
+ 3. Promote tyvars and/or kind-generalize.
+ 4. Zonk.
+ 5. Check validity.
 
 There may be some surprises in here:
 
@@ -1675,40 +1695,56 @@ Step 2 is necessary for two reasons: most signatures also bring
 implicitly quantified variables into scope, and solving is necessary
 to get these in the right order (see Note [Keeping scoped variables in
 order: Implicit]). Additionally, solving is necessary in order to
-kind-generalize correctly.
+kind-generalize correctly: otherwise, we do not know which metavariables
+are left unsolved.
 
-In Step 4, we have to deal with the fact that metatyvars generated
-in the type may have a bumped TcLevel, because explicit foralls
-raise the TcLevel. To avoid these variables from ever being visible
-in the surrounding context, we must obey the following dictum:
+Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to
+kindGeneralize{All,Some,None}. Here, we have to deal with the fact that
+metatyvars generated in the type may have a bumped TcLevel, because explicit
+foralls raise the TcLevel. To avoid these variables from ever being visible in
+the surrounding context, we must obey the following dictum:
 
   Every metavariable in a type must either be
-    (A) promoted
-    (B) generalized, or
-    (C) zapped to Any
-
-If a variable is generalized, then it becomes a skolem and no longer
-has a proper TcLevel. (I'm ignoring the TcLevel on a skolem here, as
-it's not really in play here.) On the other hand, if it is not
-generalized (because we're not generalizing the construct -- e.g., pattern
-sig -- or because the metavars are constrained -- see kindGeneralizeLocal)
-we need to promote to maintain (MetaTvInv) of Note [TcLevel and untouchable type variables]
-in TcType.
+    (A) generalized, or
+    (B) promoted, or        See Note [Promotion in signatures]
+    (C) zapped to Any       See Note [Naughty quantification candidates] in TcMType
+
+The kindGeneralize functions do not require pre-zonking; they zonk as they
+go.
 
-For more about (C), see Note [Naughty quantification candidates] in TcMType.
+If you are actually doing kind-generalization, you need to bump the level
+before generating constraints, as we will only generalize variables with
+a TcLevel higher than the ambient one.
 
-After promoting/generalizing, we need to zonk *again* because both
+After promoting/generalizing, we need to zonk again because both
 promoting and generalizing fill in metavariables.
 
-To avoid the double-zonk, we do two things:
- 1. When we're not generalizing:
-    zonkPromoteType and friends zonk and promote at the same time.
-    Accordingly, the function does steps 3-5 all at once, preventing
-    the need for multiple traversals.
+Note [Promotion in signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If an unsolved metavariable in a signature is not generalized
+(because we're not generalizing the construct -- e.g., pattern
+sig -- or because the metavars are constrained -- see kindGeneralizeSome)
+we need to promote to maintain (MetaTvInv) of Note [TcLevel and untouchable type variables]
+in TcType. Note that promotion is identical in effect to generalizing
+and the reinstantiating with a fresh metavariable at the current level.
+So in some sense, we generalize *all* variables, but then re-instantiate
+some of them.
+
+Here is an example of why we must promote:
+  foo (x :: forall a. a -> Proxy b) = ...
+
+In the pattern signature, `b` is unbound, and will thus be brought into
+scope. We do not know its kind: it will be assigned kappa[2]. Note that
+kappa is at TcLevel 2, because it is invented under a forall. (A priori,
+the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel
+than the surrounding context.) This kappa cannot be solved for while checking
+the pattern signature (which is not kind-generalized). When we are checking
+the *body* of foo, though, we need to unify the type of x with the argument
+type of bar. At this point, the ambient TcLevel is 1, and spotting a
+matavariable with level 2 would violate the (MetaTvInv) invariant of
+Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing,
+we promote the metavariable to level 1. This is all done in kindGeneralizeNone.
 
- 2. When we are generalizing:
-    kindGeneralize does not require a zonked type -- it zonks as it
-    gathers free variables. So this way effectively sidesteps step 3.
 -}
 
 tcNamedWildCardBinders :: [Name]
@@ -2228,59 +2264,75 @@ zonkAndScopedSort spec_tkvs
        -- Note [Ordering of implicit variables] in RnTypes
        ; return (scopedSort spec_tkvs) }
 
-kindGeneralize :: TcType -> TcM [KindVar]
--- Quantify the free kind variables of a kind or type
--- In the latter case the type is closed, so it has no free
--- type variables.  So in both cases, all the free vars are kind vars
--- Input needn't be zonked. All variables to be quantified must
--- have a TcLevel higher than the ambient TcLevel.
--- NB: You must call solveEqualities or solveLocalEqualities before
--- kind generalization
---
--- NB: this function is just a specialised version of
---        kindGeneralizeLocal emptyWC kind_or_type
---
-kindGeneralize kind_or_type
-  = do { kt <- zonkTcType kind_or_type
-       ; traceTc "kindGeneralise1" (ppr kt)
-       ; dvs <- candidateQTyVarsOfKind kind_or_type
-       ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
-       ; traceTc "kindGeneralize" (vcat [ ppr kind_or_type
-                                        , ppr dvs ])
-       ; quantifyTyVars gbl_tvs dvs }
-
--- | This variant of 'kindGeneralize' refuses to generalize over any
--- variables free in the given WantedConstraints. Instead, it promotes
--- these variables into an outer TcLevel. All variables to be quantified must
--- have a TcLevel higher than the ambient TcLevel. See also
--- Note [Promoting unification variables] in TcSimplify
-kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar]
-kindGeneralizeLocal wanted kind_or_type
-  = do {
-       -- This bit is very much like decideMonoTyVars in TcSimplify,
-       -- but constraints are so much simpler in kinds, it is much
-       -- easier here. (In particular, we never quantify over a
-       -- constraint in a type.)
-       ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
-       ; (_, constrained) <- promoteTyVarSet constrained
-
-       ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
-       ; let mono_tvs = gbl_tvs `unionVarSet` constrained
+-- | Generalize some of the free variables in the given type.
+-- All such variables should be *kind* variables; any type variables
+-- should be explicitly quantified (with a `forall`) before now.
+-- The supplied predicate says which free variables to quantify.
+-- But in all cases,
+-- generalize only those variables whose TcLevel is strictly greater
+-- than the ambient level. This "strictly greater than" means that
+-- you likely need to push the level before creating whatever type
+-- gets passed here. Any variable whose level is greater than the
+-- ambient level but is not selected to be generalized will be
+-- promoted. (See [Promoting unification variables] in TcSimplify
+-- and Note [Recipe for checking a signature].)
+-- The resulting KindVar are the variables to
+-- quantify over, in the correct, well-scoped order. They should
+-- generally be Inferred, not Specified, but that's really up to
+-- the caller of this function.
+kindGeneralizeSome :: (TcTyVar -> Bool)
+                   -> TcType    -- ^ needn't be zonked
+                   -> TcM [KindVar]
+kindGeneralizeSome should_gen kind_or_type
+  = do { traceTc "kindGeneralizeSome {" (ppr 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 <- candidateQTyVarsOfKind kind_or_type
-
-       ; traceTc "kindGeneralizeLocal" $
-         vcat [ text "Wanted:" <+> ppr wanted
-              , text "Kind or type:" <+> ppr kind_or_type
-              , text "tcvs of wanted:" <+> pprTyVars (nonDetEltsUniqSet (tyCoVarsOfWC wanted))
-              , text "constrained:" <+> pprTyVars (nonDetEltsUniqSet constrained)
-              , text "mono_tvs:" <+> pprTyVars (nonDetEltsUniqSet mono_tvs)
-              , text "dvs:" <+> ppr dvs ]
-
-       ; quantifyTyVars mono_tvs dvs }
+       ; dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) <- candidateQTyVarsOfKind kind_or_type
+
+       ; let promote_kvs = filterVarSet (not . should_gen) $ dVarSetToVarSet kvs
+             promote_tvs = filterVarSet (not . should_gen) $ dVarSetToVarSet tvs
+
+       ; (_, promoted) <- promoteTyVarSet (promote_kvs `unionVarSet` promote_tvs)
+
+       ; 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'
+
+       ; 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 "promoted:" <+> pprTyVars (nonDetEltsUniqSet promoted)
+              , text "gbl_tvs:" <+> pprTyVars (nonDetEltsUniqSet gbl_tvs)
+              , text "qkvs:" <+> pprTyVars qkvs ]
+
+       ; return qkvs }
+
+-- | Specialized version of 'kindGeneralizeSome', but where all variables
+-- can be generalized. Use this variant when you can be sure that no more
+-- constraints on the type's metavariables will arise or be solved.
+kindGeneralizeAll :: TcType  -- needn't be zonked
+                  -> TcM [KindVar]
+kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty
+                          ; kindGeneralizeSome (const True) ty }
+
+-- | Specialized version of 'kindGeneralizeSome', but where no variables
+-- can be generalized. Use this variant when it is unknowable whether metavariables
+-- might later be constrained.
+-- See Note [Recipe for checking a signature] for why and where this
+-- function is needed.
+kindGeneralizeNone :: TcType  -- needn't be zonked
+                   -> TcM ()
+kindGeneralizeNone ty
+  = do { traceTc "kindGeneralizeNone" empty
+       ; kvs <- kindGeneralizeSome (const False) ty
+       ; MASSERT( null kvs )
+       }
 
 {- Note [Levels and generalisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2598,6 +2650,12 @@ tcHsPartialSigType ctxt sig_ty
 
                   ; return (wcs, wcx, theta, tau) }
 
+         -- No kind-generalization here:
+       ; kindGeneralizeNone (mkSpecForAllTys implicit_tvs $
+                             mkSpecForAllTys explicit_tvs $
+                             mkPhiTy theta $
+                             tau)
+
        -- Spit out the wildcards (including the extra-constraints one)
        -- as "hole" constraints, so that they'll be reported if necessary
        -- See Note [Extra-constraint holes in partial type signatures]
@@ -2741,7 +2799,9 @@ tcHsPatSigType ctxt sig_ty
           -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ...
           -- When we instantiate x, we have to compare the kind of the argument
           -- to a's kind, which will be a metavariable.
-        ; sig_ty <- zonkPromoteType sig_ty
+          -- kindGeneralizeNone does this:
+        ; kindGeneralizeNone sig_ty
+        ; sig_ty <- zonkTcType sig_ty
         ; checkValidType ctxt sig_ty
 
         ; traceTc "tcHsPatSigType" (ppr sig_tkv_prs)
@@ -2877,70 +2937,6 @@ unifyKinds rn_tys act_kinds
 {-
 ************************************************************************
 *                                                                      *
-    Promotion
-*                                                                      *
-************************************************************************
--}
-
--- | Whenever a type is about to be added to the environment, it's necessary
--- to make sure that any free meta-tyvars in the type are promoted to the
--- current TcLevel. (They might be at a higher level due to the level-bumping
--- in tcExplicitTKBndrs, for example.) This function both zonks *and*
--- promotes. Why at the same time? See Note [Recipe for checking a signature]
-zonkPromoteType :: TcType -> TcM TcType
-zonkPromoteType = mapType zonkPromoteMapper ()
-
--- cf. TcMType.zonkTcTypeMapper
-zonkPromoteMapper :: TyCoMapper () TcM
-zonkPromoteMapper = TyCoMapper { tcm_tyvar    = const zonkPromoteTcTyVar
-                               , tcm_covar    = const covar
-                               , tcm_hole     = const hole
-                               , tcm_tycobinder = const tybinder
-                               , tcm_tycon    = return }
-  where
-    covar cv
-      = mkCoVarCo <$> zonkPromoteTyCoVarKind cv
-
-    hole :: CoercionHole -> TcM Coercion
-    hole h
-      = do { contents <- unpackCoercionHole_maybe h
-           ; case contents of
-               Just co -> do { co <- zonkPromoteCoercion co
-                             ; checkCoercionHole cv co }
-               Nothing -> do { cv' <- zonkPromoteTyCoVarKind cv
-                             ; return $ mkHoleCo (setCoHoleCoVar h cv') } }
-      where
-        cv = coHoleCoVar h
-
-    tybinder :: TyVar -> ArgFlag -> TcM ((), TyVar)
-    tybinder tv _flag = ((), ) <$> zonkPromoteTyCoVarKind tv
-
-zonkPromoteTcTyVar :: TyCoVar -> TcM TcType
-zonkPromoteTcTyVar tv
-  | isMetaTyVar tv
-  = do { let ref = metaTyVarRef tv
-       ; contents <- readTcRef ref
-       ; case contents of
-           Flexi -> do { (_, promoted_tv) <- promoteTyVar tv
-                       ; mkTyVarTy <$> zonkPromoteTyCoVarKind promoted_tv }
-           Indirect ty -> zonkPromoteType ty }
-
-  | isTcTyVar tv && isSkolemTyVar tv  -- NB: isSkolemTyVar says "True" to pure TyVars
-  = do { tc_lvl <- getTcLevel
-       ; mkTyVarTy <$> zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
-
-  | otherwise
-  = mkTyVarTy <$> zonkPromoteTyCoVarKind tv
-
-zonkPromoteTyCoVarKind :: TyCoVar -> TcM TyCoVar
-zonkPromoteTyCoVarKind = updateTyVarKindM zonkPromoteType
-
-zonkPromoteCoercion :: Coercion -> TcM Coercion
-zonkPromoteCoercion = mapCoercion zonkPromoteMapper ()
-
-{-
-************************************************************************
-*                                                                      *
         Sort checking kinds
 *                                                                      *
 ************************************************************************
@@ -2956,8 +2952,9 @@ tcLHsKindSig ctxt hs_kind
   = do { kind <- solveLocalEqualities "tcLHsKindSig" $
                  tc_lhs_kind kindLevelMode hs_kind
        ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
-       -- No generalization, so we must promote
-       ; kind <- zonkPromoteType kind
+       -- No generalization:
+       ; kindGeneralizeNone kind
+       ; kind <- zonkTcType kind
          -- This zonk is very important in the case of higher rank kinds
          -- E.g. #13879    f :: forall (p :: forall z (y::z). <blah>).
          --                          <more blah>
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index da6d836653..2953a466ad 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -65,7 +65,7 @@ module TcMType (
   tidyEvVar, tidyCt, tidySkolemInfo,
     zonkTcTyVar, zonkTcTyVars,
   zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
-  zonkTyCoVarsAndFV, zonkTcTypeAndFV,
+  zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
   zonkTyCoVarsAndFVList,
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
@@ -759,7 +759,7 @@ cloneAnonMetaTyVar info tv kind
   = do  { details <- newMetaDetails info
         ; name    <- cloneMetaTyVarName (tyVarName tv)
         ; let tyvar = mkTcTyVar name kind details
-        ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
+        ; traceTc "cloneAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar))
         ; return tyvar }
 
 newFskTyVar :: TcType -> TcM TcTyVar
@@ -1145,9 +1145,12 @@ data CandidatesQTvs
   -- See Note [CandidatesQTvs determinism and order]
   --
   -- Invariants:
-  --   * All variables stored here are MetaTvs. No exceptions.
   --   * All variables are fully zonked, including their kinds
   --
+  -- 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.
+  --
   = DV { dv_kvs :: DTyVarSet    -- "kind" metavariables (dependent)
        , dv_tvs :: DTyVarSet    -- "type" metavariables (non-dependent)
          -- A variable may appear in both sets
@@ -1252,11 +1255,11 @@ collect_cand_qtvs is_dep bound dvs ty
     go dv (CoercionTy co)   = collect_cand_qtvs_co bound dv co
 
     go dv (TyVarTy tv)
-      | is_bound tv = return dv
-      | otherwise   = do { m_contents <- isFilledMetaTyVar_maybe tv
-                         ; case m_contents of
-                             Just ind_ty -> go dv ind_ty
-                             Nothing     -> go_tv dv tv }
+      | is_bound tv      = return dv
+      | otherwise        = do { m_contents <- isFilledMetaTyVar_maybe tv
+                              ; case m_contents of
+                                  Just ind_ty -> go dv ind_ty
+                                  Nothing     -> go_tv dv tv }
 
     go dv (ForAllTy (Bndr tv _) ty)
       = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv)
@@ -1286,7 +1289,12 @@ collect_cand_qtvs is_dep bound dvs ty
                 intersectsVarSet bound (tyCoVarsOfType tv_kind)
 
              then -- See Note [Naughty quantification candidates]
-                  do { traceTc "Zapping naughty quantifier" (pprTyVar tv)
+                  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 }
 
@@ -1295,6 +1303,7 @@ collect_cand_qtvs is_dep bound dvs ty
                                | 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
 
 collect_cand_qtvs_co :: VarSet -- bound variables
                      -> CandidatesQTvs -> Coercion
@@ -1320,10 +1329,19 @@ 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 (HoleCo hole) = do m_co <- unpackCoercionHole_maybe hole
-                                case m_co of
-                                  Just co -> go_co dv co
-                                  Nothing -> go_cv dv (coHoleCoVar hole)
+    go_co dv@(DV { dv_cvs = cvs }) (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
 
     go_co dv (CoVarCo cv) = go_cv dv cv
 
@@ -1343,6 +1361,8 @@ collect_cand_qtvs_co bound = go_co
     go_cv dv@(DV { dv_cvs = cvs }) cv
       | 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
                                     (dv { dv_cvs = cvs `extendVarSet` cv })
                                     (idType cv)
@@ -1368,6 +1388,37 @@ 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
+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.
+
 -}
 
 {- *********************************************************************
@@ -1426,6 +1477,13 @@ quantifyTyVars
 --   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 })
+       -- short-circuit common case
+  | isEmptyDVarSet dep_tkvs
+  , isEmptyDVarSet nondep_tkvs
+  = do { traceTc "quantifyTyVars has nothing to quantify" empty
+       ; return [] }
+
+  | otherwise
   = do { outer_tclvl <- getTcLevel
        ; traceTc "quantifyTyVars 1" (vcat [ppr outer_tclvl, ppr dvs, ppr gbl_tvs])
        ; let co_tvs = closeOverKinds covars
@@ -1461,6 +1519,8 @@ quantifyTyVars gbl_tvs
              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 ]
@@ -1469,7 +1529,7 @@ quantifyTyVars gbl_tvs
                                   , text "dep_kvs2 ="    <+> ppr dep_kvs2
                                   , text "nondep_tvs ="  <+> ppr nondep_tvs
                                   , text "nondep_tvs2 =" <+> ppr nondep_tvs2 ])
-       ; WARN( not all_ok, bad_msg ) return ()
+       ; MASSERT2( all_ok, bad_msg )
 
              -- In the non-PolyKinds case, default the kind variables
              -- to *, and zonk the tyvars as usual.  Notice that this
@@ -1843,6 +1903,10 @@ zonkTyCoVarsAndFV tycovars
   -- the ordering by turning it into a nondeterministic set and the order
   -- of zonking doesn't matter for determinism.
 
+zonkDTyCoVarSetAndFV :: DTyCoVarSet -> TcM DTyCoVarSet
+zonkDTyCoVarSetAndFV tycovars
+  = mkDVarSet <$> (zonkTyCoVarsAndFVList $ dVarSetElems tycovars)
+
 -- Takes a list of TyCoVars, zonks them and returns a
 -- deterministically ordered list of their free variables.
 zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 151a7cbf83..d4ff73d566 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2432,6 +2432,8 @@ tcRnType hsc_env flexi normalise rdr_type
                   -- generalisation; e.g.   :kind (T _)
        ; failIfErrsM
 
+        -- We follow Note [Recipe for checking a signature] in TcHsType here
+
         -- Now kind-check the type
         -- It can have any rank or kind
         -- First bring into scope any wildcards
@@ -2445,8 +2447,7 @@ tcRnType hsc_env flexi normalise rdr_type
                           ; tcLHsTypeUnsaturated rn_type }
 
        -- Do kind generalisation; see Note [Kind-generalise in tcRnType]
-       ; kind <- zonkTcType kind
-       ; kvs <- kindGeneralize kind
+       ; kvs <- kindGeneralizeAll kind
        ; e <- mkEmptyZonkEnv flexi
 
        ; ty  <- zonkTcTypeToTypeX e ty
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 2ddca2805f..f6505152f8 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -396,7 +396,7 @@ tcPatSynSig name sig_ty
                                                  req ex_tvs prov body_ty
 
        -- Kind generalisation
-       ; kvs <- kindGeneralize ungen_patsyn_ty
+       ; kvs <- kindGeneralizeAll ungen_patsyn_ty
        ; traceTc "tcPatSynSig" (ppr ungen_patsyn_ty)
 
        -- These are /signatures/ so we zonk to squeeze out any kind
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 237f59f5b9..fbb26b103f 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2444,30 +2444,6 @@ But it can deal with covars that are arguments to GADT data constructors.
 So we somehow want to allow covars only in precisely those spots, then use
 them as givens when checking the RHS. TODO (RAE): Implement plan.
 
-
-Note [Quantifying over family patterns]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We need to quantify over two different lots of kind variables:
-
-First, the ones that come from the kinds of the tyvar args of
-tcTyVarBndrsKindGen, as usual
-  data family Dist a
-
-  -- Proxy :: forall k. k -> *
-  data instance Dist (Proxy a) = DP
-  -- Generates  data DistProxy = DP
-  --            ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
-  -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
-
-Second, the ones that come from the kind argument of the type family
-which we pick up using the (tyCoVarsOfTypes typats) in the result of
-the thing_inside of tcHsTyvarBndrsGen.
-  -- Any :: forall k. k
-  data instance Dist Any = DA
-  -- Generates  data DistAny k = DA
-  --            ax7 k :: Dist k (Any k) ~ DistAny k
-  -- The 'k' comes from kindGeneralizeKinds (Any k)
-
 Note [Quantified kind variables of a family pattern]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider   type family KindFam (p :: k1) (q :: k1)
@@ -2586,11 +2562,11 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
          -- the kvs below are those kind variables entirely unmentioned by the user
          --   and discovered only by generalization
 
-       ; kvs <- kindGeneralize (mkSpecForAllTys (binderVars tmpl_bndrs) $
-                                mkSpecForAllTys exp_tvs $
-                                mkPhiTy ctxt $
-                                mkVisFunTys arg_tys $
-                                unitTy)
+       ; kvs <- kindGeneralizeAll (mkSpecForAllTys (binderVars tmpl_bndrs) $
+                                   mkSpecForAllTys exp_tvs $
+                                   mkPhiTy ctxt $
+                                   mkVisFunTys arg_tys $
+                                   unitTy)
                  -- That type is a lie, of course. (It shouldn't end in ()!)
                  -- And we could construct a proper result type from the info
                  -- at hand. But the result would mention only the tmpl_tvs,
@@ -2670,10 +2646,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
        ; imp_tvs <- zonkAndScopedSort imp_tvs
        ; let user_tvs      = imp_tvs ++ exp_tvs
 
-       ; tkvs <- kindGeneralize (mkSpecForAllTys user_tvs $
-                                 mkPhiTy ctxt $
-                                 mkVisFunTys arg_tys $
-                                 res_ty)
+       ; tkvs <- kindGeneralizeAll (mkSpecForAllTys user_tvs $
+                                    mkPhiTy ctxt $
+                                    mkVisFunTys arg_tys $
+                                    res_ty)
 
              -- Zonk to Types
        ; (ze, tkvs)     <- zonkTyBndrs tkvs
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index d37887e9e7..d0000e1e35 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -2604,8 +2604,9 @@ Then we do the process described in Note [simplifyArgsWorker].
 2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> sym co1).
    This is not a dependent argument, so we don't extend the lifting context.
 
-Now we need to deal with argument (3). After flattening, should we tack on a homogenizing
-coercion? The way we normally tell is to lift the kind of the binder.
+Now we need to deal with argument (3).
+The way we normally proceed is to lift the kind of the binder, to see whether
+it's dependent.
 But here, the remainder of the kind of `a` that we're left with
 after processing two arguments is just `k`.
 
@@ -2712,6 +2713,19 @@ as desired.
 
 Whew.
 
+Historical note: I (Richard E) once thought that the final part of the kind
+had to be a variable k (as in the example above). But it might not be: it could
+be an application of a variable. Here is the example:
+
+  let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
+      k :: Type
+      x :: k
+
+  flatten (f @Type @((->) k) x)
+
+After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
+is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
+
 -}
 
 
@@ -2786,9 +2800,8 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
 
       -- See Note [Last case in simplifyArgsWorker]
     go acc_xis acc_cos lc [] inner_ki roles args
-      | Just k   <- getTyVar_maybe inner_ki
-      , Just co1 <- liftCoSubstTyVar lc Nominal k
-      = let co1_kind              = coercionKind co1
+      = let co1 = liftCoSubst Nominal lc inner_ki
+            co1_kind              = coercionKind co1
             unflattened_tys       = map (pSnd . coercionKind . snd) args
             (arg_cos, res_co)     = decomposePiCos co1 co1_kind unflattened_tys
             casted_args           = ASSERT2( equalLength args arg_cos
diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs
index b8da86e36c..b5d482c63c 100644
--- a/compiler/types/TyCoFVs.hs
+++ b/compiler/types/TyCoFVs.hs
@@ -162,8 +162,11 @@ ty_co_vars_of_type (TyVarTy v) is acc
   | otherwise          = ty_co_vars_of_type (tyVarKind v) emptyVarSet (extendVarSet acc v)
                                                           ^^^^^^^^^^^
 
-And that's it.
-
+And that's it. This works because a variable is either bound or free. If it is bound,
+then we won't look at it at all. If it is free, then all the variables free in its
+kind are free -- regardless of whether some local variable has the same Unique.
+So if we're looking at a variable occurrence at all, then all variables in its
+kind are free.
 -}
 
 tyCoVarsOfType :: Type -> TyCoVarSet
@@ -816,4 +819,3 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
 -- | Get the free vars of types in scoped order
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
-
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 24782235ba..31e5c8c4e7 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,10 +1,13 @@
 
 T14040a.hs:34:8: error:
-    • Cannot apply expression of type ‘Sing wl
-                                       -> (forall y. p _2 'WeirdNil)
-                                       -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                                           Sing x -> Sing xs -> p _0 xs -> p _1 ('WeirdCons x xs))
-                                       -> p _2 wl’
+    • Cannot apply expression of type ‘Sing wl0
+                                       -> (forall y. p0 _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’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’