Never Anyify during kind inference

See Note [Error on unconstrained meta-variables] in TcMType.

Close #17301
Close #17567
Close #17562
Close #15474

8 files changed, 295 insertions, 83 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index ac6c95d954..0a188d9020 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -537,7 +537,8 @@ tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs
        ; kvs <- kindGeneralizeAll ty1  -- "All" because it's a top-level type
        ; reportUnsolvedEqualities skol_info kvs tclvl wanted
 
-       ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)
+       ; ze       <- mkEmptyZonkEnv NoFlexi
+       ; final_ty <- zonkTcTypeToTypeX ze (mkInfForAllTys kvs ty1)
        ; traceTc "tc_top_lhs_type }" (vcat [ppr sig_ty, ppr final_ty])
        ; return final_ty }
   where
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 095fefe468..f3934e6f78 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -410,13 +410,14 @@ tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty
        -- These are /signatures/ so we zonk to squeeze out any kind
        -- unification variables.  Do this after kindGeneralizeAll which may
        -- default kind variables to *.
-       ; (ze, kv_bndrs)       <- zonkTyVarBinders (mkTyVarBinders InferredSpec kvs)
-       ; (ze, implicit_bndrs) <- zonkTyVarBindersX ze implicit_bndrs
-       ; (ze, univ_bndrs)     <- zonkTyVarBindersX ze univ_bndrs
-       ; (ze, ex_bndrs)       <- zonkTyVarBindersX ze ex_bndrs
-       ; req          <- zonkTcTypesToTypesX ze req
-       ; prov         <- zonkTcTypesToTypesX ze prov
-       ; body_ty      <- zonkTcTypeToTypeX   ze body_ty
+       ; ze                   <- mkEmptyZonkEnv NoFlexi
+       ; (ze, kv_bndrs)       <- zonkTyVarBindersX   ze (mkTyVarBinders InferredSpec kvs)
+       ; (ze, implicit_bndrs) <- zonkTyVarBindersX   ze implicit_bndrs
+       ; (ze, univ_bndrs)     <- zonkTyVarBindersX   ze univ_bndrs
+       ; (ze, ex_bndrs)       <- zonkTyVarBindersX   ze ex_bndrs
+       ; req                  <- zonkTcTypesToTypesX ze req
+       ; prov                 <- zonkTcTypesToTypesX ze prov
+       ; body_ty              <- zonkTcTypeToTypeX   ze body_ty
 
        -- Now do validity checking
        ; checkValidType ctxt $
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 42a00d73ba..78b32bec15 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -662,7 +662,7 @@ rewrite_vector ki roles tys
                                   tys
        }
   where
-    (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki  -- "RAE" fix
+    (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
     fvs                                = tyCoVarsOfType ki
 {-# INLINE rewrite_vector #-}
 
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index b912baa04d..0e387c6247 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -887,10 +887,10 @@ generaliseTcTyCon (tc, scoped_prs, tc_res_kind)
 
        -- Step 3: Final zonk (following kind generalisation)
        -- See Note [Swizzling the tyvars before generaliseTcTyCon]
-       ; ze <- emptyZonkEnv
-       ; (ze, inferred)        <- zonkTyBndrsX ze inferred
-       ; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs
-       ; (ze, req_tvs)         <- zonkTyBndrsX ze req_tvs
+       ; ze <- mkEmptyZonkEnv NoFlexi
+       ; (ze, inferred)        <- zonkTyBndrsX      ze inferred
+       ; (ze, sorted_spec_tvs) <- zonkTyBndrsX      ze sorted_spec_tvs
+       ; (ze, req_tvs)         <- zonkTyBndrsX      ze req_tvs
        ; tc_res_kind           <- zonkTcTypeToTypeX ze tc_res_kind
 
        ; traceTc "generaliseTcTyCon: post zonk" $
@@ -2346,13 +2346,24 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
                   ; at_stuff  <- tcClassATs class_name clas ats at_defs
                   ; return (ctxt, fds, sig_stuff, at_stuff) }
 
+       -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+       -- Example: (typecheck/should_fail/T17562)
+       --   type C :: Type -> Type -> Constraint
+       --   class (forall a. a b ~ a c) => C b c
+       -- The kind of `a` is unconstrained.
+       ; dvs <- candidateQTyVarsOfTypes ctxt
+       ; let mk_doc tidy_env = do { (tidy_env2, ctxt) <- zonkTidyTcTypes tidy_env ctxt
+                                  ; return ( tidy_env2
+                                           , sep [ text "the class context:"
+                                                 , pprTheta ctxt ] ) }
+       ; doNotQuantifyTyVars dvs mk_doc
 
        -- The pushLevelAndSolveEqualities will report errors for any
        -- unsolved equalities, so these zonks should not encounter
        -- any unfilled coercion variables unless there is such an error
        -- The zonk also squeeze out the TcTyCons, and converts
        -- Skolems to tyvars.
-       ; ze        <- emptyZonkEnv
+       ; ze        <- mkEmptyZonkEnv NoFlexi
        ; ctxt      <- zonkTcTypesToTypesX ze ctxt
        ; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff
          -- ToDo: do we need to zonk at_stuff?
@@ -2739,7 +2750,20 @@ tcTySynRhs roles_info tc_name hs_ty
        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
        ; rhs_ty <- pushLevelAndSolveEqualities skol_info (binderVars binders) $
                    tcCheckLHsType hs_ty (TheKind res_kind)
-       ; rhs_ty <- zonkTcTypeToType rhs_ty
+
+         -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+         -- Example: (typecheck/should_fail/T17567)
+         --   type T = forall a. Proxy a
+         -- The kind of `a` is unconstrained.
+       ; dvs <- candidateQTyVarsOfType rhs_ty
+       ; let mk_doc tidy_env = do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_ty
+                                  ; return ( tidy_env2
+                                           , sep [ text "the type synonym right-hand side:"
+                                                 , ppr rhs_ty ] ) }
+       ; doNotQuantifyTyVars dvs mk_doc
+
+       ; ze <- mkEmptyZonkEnv NoFlexi
+       ; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty
        ; let roles = roles_info tc_name
        ; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) }
   where
@@ -2776,10 +2800,24 @@ tcDataDefn err_ctxt roles_info tc_name
        ; let skol_tvs = binderVars tycon_binders
        ; stupid_tc_theta <- pushLevelAndSolveEqualities skol_info skol_tvs $
                             tcHsContext ctxt
-       ; stupid_theta    <- zonkTcTypesToTypes stupid_tc_theta
-       ; kind_signatures <- xoptM LangExt.KindSignatures
 
-             -- Check that we don't use kind signatures without Glasgow extensions
+       -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+       -- Example: (typecheck/should_fail/T17567StupidTheta)
+       --   data (forall a. a b ~ a c) => T b c
+       -- The kind of 'a' is unconstrained.
+       ; dvs <- candidateQTyVarsOfTypes stupid_tc_theta
+       ; let mk_doc tidy_env
+               = do { (tidy_env2, theta) <- zonkTidyTcTypes tidy_env stupid_tc_theta
+                    ; return ( tidy_env2
+                             , sep [ text "the datatype context:"
+                                   , pprTheta theta ] ) }
+       ; doNotQuantifyTyVars dvs mk_doc
+
+       ; ze              <- mkEmptyZonkEnv NoFlexi
+       ; stupid_theta    <- zonkTcTypesToTypesX ze stupid_tc_theta
+
+             -- Check that we don't use kind signatures without the extension
+       ; kind_signatures <- xoptM LangExt.KindSignatures
        ; when (isJust mb_ksig) $
          checkTc (kind_signatures) (badSigTyDecl tc_name)
 
@@ -3016,7 +3054,18 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
               , text "lhs_ty"     <+> ppr lhs_ty
               , text "qtvs"       <+> pprTyVars qtvs ]
 
-       ; (ze, qtvs) <- zonkTyBndrs qtvs
+       -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+       -- Example: typecheck/should_fail/T17301
+       ; dvs_rhs <- candidateQTyVarsOfType rhs_ty
+       ; let mk_doc tidy_env
+               = do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_ty
+                    ; return ( tidy_env2
+                             , sep [ text "type family equation right-hand side:"
+                                   , ppr rhs_ty ] ) }
+       ; doNotQuantifyTyVars dvs_rhs mk_doc
+
+       ; ze         <- mkEmptyZonkEnv NoFlexi
+       ; (ze, qtvs) <- zonkTyBndrsX      ze qtvs
        ; lhs_ty     <- zonkTcTypeToTypeX ze lhs_ty
        ; rhs_ty     <- zonkTcTypeToTypeX ze rhs_ty
 
@@ -3283,10 +3332,11 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs res_kind tag_map
              -- See test dependent/should_fail/T13780a
 
        -- Zonk to Types
-       ; (ze, qkvs)          <- zonkTyBndrs kvs
-       ; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs
+       ; ze                  <- mkEmptyZonkEnv NoFlexi
+       ; (ze, qkvs)          <- zonkTyBndrsX              ze kvs
+       ; (ze, user_qtvbndrs) <- zonkTyVarBindersX         ze exp_tvbndrs
        ; arg_tys             <- zonkScaledTcTypesToTypesX ze arg_tys
-       ; ctxt                <- zonkTcTypesToTypesX ze ctxt
+       ; ctxt                <- zonkTcTypesToTypesX       ze ctxt
 
        -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
        ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
@@ -3368,10 +3418,11 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs _res_kind tag_map
        ; let tvbndrs =  mkTyVarBinders InferredSpec tkvs ++ outer_tv_bndrs
 
              -- Zonk to Types
-       ; (ze, tvbndrs) <- zonkTyVarBinders       tvbndrs
+       ; ze            <- mkEmptyZonkEnv NoFlexi
+       ; (ze, tvbndrs) <- zonkTyVarBindersX         ze tvbndrs
        ; arg_tys       <- zonkScaledTcTypesToTypesX ze arg_tys
-       ; ctxt          <- zonkTcTypesToTypesX ze ctxt
-       ; res_ty        <- zonkTcTypeToTypeX   ze res_ty
+       ; ctxt          <- zonkTcTypesToTypesX       ze ctxt
+       ; res_ty        <- zonkTcTypeToTypeX         ze res_ty
 
        ; let res_tmpl = mkDDHeaderTy dd_info rep_tycon tc_bndrs
              (univ_tvs, ex_tvs, tvbndrs', eq_preds, arg_subst)
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 11a10baf29..69656b41da 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -912,9 +912,10 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
        ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
 
        -- Zonk the patterns etc into the Type world
-       ; (ze, qtvs)   <- zonkTyBndrs qtvs
-       ; lhs_ty       <- zonkTcTypeToTypeX   ze lhs_ty
-       ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
+       ; ze           <- mkEmptyZonkEnv NoFlexi
+       ; (ze, qtvs)   <- zonkTyBndrsX           ze qtvs
+       ; lhs_ty       <- zonkTcTypeToTypeX      ze lhs_ty
+       ; stupid_theta <- zonkTcTypesToTypesX    ze stupid_theta
        ; master_res_kind   <- zonkTcTypeToTypeX ze master_res_kind
        ; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind
 
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 880787447e..2fd0669f91 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -228,7 +228,7 @@ mkProvEvidence ev_id
 dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
 -- See Note [Coercions that escape]
 dependentArgErr (arg, bad_cos)
-  = addErrTc $
+  = failWithTc $  -- fail here: otherwise we get downstream errors
     vcat [ text "Iceland Jack!  Iceland Jack! Stop torturing me!"
          , hang (text "Pattern-bound variable")
               2 (ppr arg <+> dcolon <+> ppr (idType arg))
@@ -675,11 +675,12 @@ tc_patsyn_finish lname dir is_infix lpat' prag_fn
   = do { -- Zonk everything.  We are about to build a final PatSyn
          -- so there had better be no unification variables in there
 
-         (ze, univ_tvs') <- zonkTyVarBinders univ_tvs
+       ; ze              <- mkEmptyZonkEnv NoFlexi
+       ; (ze, univ_tvs') <- zonkTyVarBindersX   ze univ_tvs
        ; req_theta'      <- zonkTcTypesToTypesX ze req_theta
-       ; (ze, ex_tvs')   <- zonkTyVarBindersX ze ex_tvs
+       ; (ze, ex_tvs')   <- zonkTyVarBindersX   ze ex_tvs
        ; prov_theta'     <- zonkTcTypesToTypesX ze prov_theta
-       ; pat_ty'         <- zonkTcTypeToTypeX ze pat_ty
+       ; pat_ty'         <- zonkTcTypeToTypeX   ze pat_ty
        ; arg_tys'        <- zonkTcTypesToTypesX ze arg_tys
 
        ; let (env1, univ_tvs) = tidyTyCoVarBinders emptyTidyEnv univ_tvs'
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 8d14d9201d..24b7e4d93a 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -83,6 +83,7 @@ module GHC.Tc.Utils.TcMType (
   defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
   quantifyTyVars, isQuantifiableTv,
   skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar,
+  doNotQuantifyTyVars,
 
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
@@ -1299,6 +1300,29 @@ instance Outputable CandidatesQTvs where
                                              , text "dv_tvs =" <+> ppr tvs
                                              , text "dv_cvs =" <+> ppr cvs ])
 
+isEmptyCandidates :: CandidatesQTvs -> Bool
+isEmptyCandidates (DV { dv_kvs = kvs, dv_tvs = tvs })
+  = isEmptyDVarSet kvs && isEmptyDVarSet tvs
+
+-- | Extract out the kind vars (in order) and type vars (in order) from
+-- a 'CandidatesQTvs'. The lists are guaranteed to be distinct. Keeping
+-- the lists separate is important only in the -XNoPolyKinds case.
+candidateVars :: CandidatesQTvs -> ([TcTyVar], [TcTyVar])
+candidateVars (DV { dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
+  = (dep_kvs, nondep_tvs)
+  where
+    dep_kvs = scopedSort $ dVarSetElems dep_kv_set
+      -- scopedSort: put the kind variables into
+      --    well-scoped order.
+      --    E.g.  [k, (a::k)] not the other way round
+
+    nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
+      -- 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
+      -- NB kinds of tvs are already zonked
 
 candidateKindVars :: CandidatesQTvs -> TyVarSet
 candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
@@ -1377,7 +1401,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
     go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
     -- Uses accumulating-parameter style
     go dv (AppTy t1 t2)    = foldlM go dv [t1, t2]
-    go dv (TyConApp _ tys) = foldlM go dv tys
+    go dv (TyConApp tc tys) = go_tc_args dv (tyConBinders tc) tys
     go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res]
     go dv (LitTy {})        = return dv
     go dv (CastTy ty co)    = do dv1 <- go dv ty
@@ -1395,6 +1419,20 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
       = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
            ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty }
 
+      -- This makes sure that we default e.g. the alpha in Proxy alpha (Any alpha).
+      -- Tested in polykinds/NestedProxies.
+      -- We just might get this wrong in AppTy, but I don't think that's possible
+      -- with -XNoPolyKinds. And fixing it would be non-performant, as we'd need
+      -- to look at kinds.
+    go_tc_args dv (tc_bndr:tc_bndrs) (ty:tys)
+      = do { dv1 <- collect_cand_qtvs orig_ty (is_dep || isNamedTyConBinder tc_bndr)
+                                      bound dv ty
+           ; go_tc_args dv1 tc_bndrs tys }
+    go_tc_args dv _bndrs tys  -- _bndrs might be non-empty: undersaturation
+                              -- tys might be non-empty: oversaturation
+                              -- either way, the foldlM is correct
+      = foldlM go dv tys
+
     -----------------
     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
       | tv `elemDVarSet` kvs
@@ -1415,7 +1453,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
            ; cur_lvl <- getTcLevel
            ; if |  tcTyVarLevel tv <= cur_lvl
                 -> return dv   -- this variable is from an outer context; skip
-                               -- See Note [Use level numbers ofor quantification]
+                               -- See Note [Use level numbers for quantification]
 
                 |  intersectsVarSet bound tv_kind_vars
                    -- the tyvar must not be from an outer context, but we have
@@ -1566,7 +1604,7 @@ are about to wrap in a forall.
 
 It takes these free type/kind variables (partitioned into dependent and
 non-dependent variables) skolemises metavariables with a TcLevel greater
-than the ambient level (see Note [Use level numbers of quantification]).
+than the ambient level (see Note [Use level numbers for quantification]).
 
 * This function distinguishes between dependent and non-dependent
   variables only to keep correct defaulting behavior with -XNoPolyKinds.
@@ -1642,46 +1680,21 @@ quantifyTyVars :: CandidatesQTvs   -- See Note [Dependent type variables]
 -- 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_kv_set, dv_tvs = nondep_tkv_set })
+quantifyTyVars dvs
        -- short-circuit common case
-  | isEmptyDVarSet dep_kv_set
-  , isEmptyDVarSet nondep_tkv_set
+  | isEmptyCandidates dvs
   = do { traceTc "quantifyTyVars has nothing to quantify" empty
        ; return [] }
 
   | otherwise
   = do { traceTc "quantifyTyVars {" (ppr dvs)
 
-       ; let dep_kvs = scopedSort $ dVarSetElems dep_kv_set
-              -- scopedSort: put the kind variables into
-              --    well-scoped order.
-              --    E.g.  [k, (a::k)] not the other way round
-
-             nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
-                 -- 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
-                 -- NB kinds of tvs are already zonked
-
-             -- 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
-             -- than it was passed, but that's ok
-       ; poly_kinds  <- xoptM LangExt.PolyKinds
-       ; dep_kvs'    <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
-       ; nondep_tvs' <- mapMaybeM (zonk_quant False)            nondep_tvs
-       ; let final_qtvs = dep_kvs' ++ nondep_tvs'
-           -- Because of the order, any kind variables
-           -- mentioned in the kinds of the nondep_tvs'
-           -- now refer to the dep_kvs'
+       ; undefaulted <- defaultTyVars dvs
+       ; final_qtvs  <- mapMaybeM zonk_quant undefaulted
 
        ; traceTc "quantifyTyVars }"
-           (vcat [ text "nondep:"     <+> pprTyVars nondep_tvs
-                 , text "dep:"        <+> pprTyVars dep_kvs
-                 , text "dep_kvs'"    <+> pprTyVars dep_kvs'
-                 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
+           (vcat [ text "undefaulted:" <+> pprTyVars undefaulted
+                 , text "final_qtvs:"  <+> pprTyVars final_qtvs ])
 
        -- We should never quantify over coercion variables; check this
        ; let co_vars = filter isCoVar final_qtvs
@@ -1691,9 +1704,8 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
   where
     -- zonk_quant returns a tyvar if it should be quantified over;
     -- otherwise, it returns Nothing. The latter case happens for
-    --    * Kind variables, with -XNoPolyKinds: don't quantify over these
-    --    * RuntimeRep variables: we never quantify over these
-    zonk_quant default_kind tkv
+    -- non-meta-tyvars
+    zonk_quant tkv
       | not (isTyVar tkv)
       = return Nothing   -- this can happen for a covar that's associated with
                          -- a coercion hole. Test case: typecheck/should_compile/T2494
@@ -1703,11 +1715,7 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
                            -- kind signature, we have the class variables in
                            -- scope, and they are TyVars not TcTyVars
       | otherwise
-      = do { deflt_done <- defaultTyVar default_kind tkv
-           ; case deflt_done of
-               True  -> return Nothing
-               False -> do { tv <- skolemiseQuantifiedTyVar tkv
-                           ; return (Just tv) } }
+      = Just <$> skolemiseQuantifiedTyVar tkv
 
 isQuantifiableTv :: TcLevel   -- Level of the context, outside the quantification
                  -> TcTyVar
@@ -1817,6 +1825,24 @@ defaultTyVar default_kind tv
       where
         (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 
+-- | Default some unconstrained type variables:
+--     RuntimeRep tyvars default to LiftedRep
+--     Multiplicity tyvars default to Many
+--     Type tyvars from dv_kvs default to Type, when -XNoPolyKinds
+--     (under -XNoPolyKinds, non-defaulting vars in dv_kvs is an error)
+defaultTyVars :: CandidatesQTvs  -- ^ all candidates for quantification
+              -> TcM [TcTyVar]   -- ^ those variables not defaulted
+defaultTyVars dvs
+  = do { poly_kinds <- xoptM LangExt.PolyKinds
+       ; defaulted_kvs <- mapM (defaultTyVar (not poly_kinds)) dep_kvs
+       ; defaulted_tvs <- mapM (defaultTyVar False)            nondep_tvs
+       ; let undefaulted_kvs = [ kv | (kv, False) <- dep_kvs    `zip` defaulted_kvs ]
+             undefaulted_tvs = [ tv | (tv, False) <- nondep_tvs `zip` defaulted_tvs ]
+       ; return (undefaulted_kvs ++ undefaulted_tvs) }
+          -- NB: kvs before tvs because tvs may depend on kvs
+  where
+    (dep_kvs, nondep_tvs) = candidateVars dvs
+
 skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
 -- Skolemise it, so that we are totally out of Meta-tyvar-land
@@ -1851,6 +1877,134 @@ skolemiseUnboundMetaTyVar tv
                Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                               return () }
 
+{- Note [Error on unconstrained meta-variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  type C :: Type -> Type -> Constraint
+  class (forall a. a b ~ a c) => C b c
+
+or
+
+  type T = forall a. Proxy a
+
+or
+
+  data (forall a. a b ~ a c) => T b c
+
+We will infer a :: Type -> kappa... but then we get no further information
+on kappa. What to do?
+
+ A. We could choose kappa := Type. But this only works when the kind of kappa
+    is Type (true in this example, but not always).
+ B. We could default to Any.
+ C. We could quantify.
+ D. We could error.
+
+We choose (D), as described in #17567. Discussion of alternatives is below.
+
+(One last example: type instance F Int = Proxy Any, where the unconstrained
+kind variable is the inferred kind of Any. The four examples here illustrate
+all cases in which this Note applies.)
+
+To do this, we must take an extra step before doing the final zonk to create
+e.g. a TyCon. (There is no problem in the final term-level zonk. See the
+section on alternative (B) below.) This extra step is needed only for
+constructs that do not quantify their free meta-variables, such as a class
+constraint or right-hand side of a type synonym.
+
+Specifically: before the final zonk, every construct must either call
+quantifyTyVars or doNotQuantifyTyVars. The latter issues an error
+if it is passed any free variables. (Exception: we still default
+RuntimeRep and Multiplicity variables.)
+
+Because no meta-variables remain after quantifying or erroring, we perform
+the zonk with NoFlexi, which panics upon seeing a meta-variable.
+
+Alternatives not implemented:
+
+A. As stated above, this works only sometimes. We might have a free
+   meta-variable of kind Nat, for example.
+
+B. This is what we used to do, but it caused Any to appear in error
+   messages sometimes. See #17567 for several examples. Defaulting to
+   Any during the final, whole-program zonk is OK, though, because
+   we are completely done type-checking at that point. No chance to
+   leak into an error message.
+
+C. Examine the class declaration at the top of this Note again.
+   Where should we quantify? We might imagine quantifying and
+   putting the kind variable in the forall of the quantified constraint.
+   But what if there are nested foralls? Which one should get the
+   variable? Other constructs have other problems. (For example,
+   the right-hand side of a type family instance equation may not
+   be a poly-type.)
+
+   More broadly, the GHC AST defines a set of places where it performs
+   implicit lexical generalization. For example, in a type
+   signature
+
+     f :: Proxy a -> Bool
+
+   the otherwise-unbound a is lexically quantified, giving us
+
+     f :: forall a. Proxy a -> Bool
+
+   The places that allow lexical quantification are marked in the AST with
+   HsImplicitBndrs. HsImplicitBndrs offers a binding site for otherwise-unbound
+   variables.
+
+   Later, during type-checking, we discover that a's kind is unconstrained.
+   We thus quantify *again*, to
+
+     f :: forall {k} (a :: k). Proxy @k a -> Bool
+
+   It is this second quantification that this Note is really about --
+   let's call it *inferred quantification*.
+   So there are two sorts of implicit quantification in types:
+     1. Lexical quantification: signalled by HsImplicitBndrs, occurs over
+        variables mentioned by the user but with no explicit binding site,
+        suppressed by a user-written forall (by the forall-or-nothing rule,
+        in Note [forall-or-nothing rule] in GHC.Hs.Type).
+     2. Inferred quantification: no signal in HsSyn, occurs over unconstrained
+        variables invented by the type-checker, possible only with -XPolyKinds,
+        unaffected by forall-or-nothing rule
+   These two quantifications are performed in different compiler phases, and are
+   essentially unrelated. However, it is convenient
+   for programmers to remember only one set of implicit quantification
+   sites. So, we choose to use the same places (those with HsImplicitBndrs)
+   for lexical quantification as for inferred quantification of unconstrained
+   meta-variables. Accordingly, there is no quantification in a class
+   constraint, or the other constructs that call doNotQuantifyTyVars.
+-}
+
+doNotQuantifyTyVars :: CandidatesQTvs
+                    -> (TidyEnv -> TcM (TidyEnv, SDoc))
+                            -- ^ like "the class context (D a b, E foogle)"
+                    -> TcM ()
+doNotQuantifyTyVars dvs where_found
+  | isEmptyCandidates dvs
+  = traceTc "doNotQuantifyTyVars has nothing to error on" empty
+
+  | otherwise
+  = do { traceTc "doNotQuantifyTyVars" (ppr dvs)
+       ; undefaulted <- defaultTyVars dvs
+          -- could have regular TyVars here, in an associated type RHS, or
+          -- bound by a type declaration head. So filter looking only for
+          -- metavars. e.g. b and c in `class (forall a. a b ~ a c) => C b c`
+          -- are OK
+       ; let leftover_metas = filter isMetaTyVar undefaulted
+       ; unless (null leftover_metas) $
+         do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
+            ; (tidy_env2, where_doc) <- where_found tidy_env1
+            ; let doc = vcat [ text "Uninferrable type variable"
+                               <> plural tidied_tvs
+                               <+> pprWithCommas pprTyVar tidied_tvs
+                               <+> text "in"
+                             , where_doc ]
+            ; failWithTcM (tidy_env2, pprWithExplicitKindsWhen True doc) }
+       ; traceTc "doNotQuantifyTyVars success" empty }
+
 {- Note [Defaulting with -XNoPolyKinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index acfa24dd10..fbcc8444ed 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -33,10 +33,10 @@ module GHC.Tc.Utils.Zonk (
         zonkTopDecls, zonkTopExpr, zonkTopLExpr,
         zonkTopBndrs,
         ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
-        zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
+        zonkTyVarBindersX, zonkTyVarBinderX,
         zonkTyBndrs, zonkTyBndrsX,
         zonkTcTypeToType,  zonkTcTypeToTypeX,
-        zonkTcTypesToTypes, zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX,
+        zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX,
         zonkTyVarOcc,
         zonkCoToCo,
         zonkEvBinds, zonkTcEvBinds,
@@ -284,6 +284,10 @@ There are three possibilities:
   It's a way to have a variable that is not a mutable
   unification variable, but doesn't have a binding site
   either.
+
+* NoFlexi: See Note [Error on unconstrained meta-variables]
+  in GHC.Tc.Utils.TcMType. This mode will panic on unfilled
+  meta-variables.
 -}
 
 data ZonkFlexi   -- See Note [Un-unified unification variables]
@@ -291,6 +295,9 @@ data ZonkFlexi   -- See Note [Un-unified unification variables]
   | SkolemiseFlexi  -- Skolemise unbound unification variables
                     -- See Note [Zonking the LHS of a RULE]
   | RuntimeUnkFlexi -- Used in the GHCi debugger
+  | NoFlexi         -- Panic on unfilled meta-variables
+                    -- See Note [Error on unconstrained meta-variables]
+                    -- in GHC.Tc.Utils.TcMType
 
 instance Outputable ZonkEnv where
   ppr (ZonkEnv { ze_tv_env = tv_env
@@ -452,10 +459,6 @@ zonkTyBndrX env tv
        ; let tv' = mkTyVar (tyVarName tv) ki
        ; return (extendTyZonkEnv env tv', tv') }
 
-zonkTyVarBinders ::  [VarBndr TcTyVar vis]
-                 -> TcM (ZonkEnv, [VarBndr TyVar vis])
-zonkTyVarBinders tvbs = initZonkEnv $ \ ze -> zonkTyVarBindersX ze tvbs
-
 zonkTyVarBindersX :: ZonkEnv -> [VarBndr TcTyVar vis]
                              -> TcM (ZonkEnv, [VarBndr TyVar vis])
 zonkTyVarBindersX = mapAccumLM zonkTyVarBinderX
@@ -1847,6 +1850,9 @@ commitFlexi flexi tv zonked_kind
                         -- otherwise-unconstrained unification variables are
                         -- turned into RuntimeUnks as they leave the
                         -- typechecker's monad
+
+      NoFlexi -> pprPanic "NoFlexi" (ppr tv <+> dcolon <+> ppr zonked_kind)
+
   where
      name = tyVarName tv
 
@@ -1899,9 +1905,6 @@ zonkTcTyConToTyCon tc
 zonkTcTypeToType :: TcType -> TcM Type
 zonkTcTypeToType ty = initZonkEnv $ \ ze -> zonkTcTypeToTypeX ze ty
 
-zonkTcTypesToTypes :: [TcType] -> TcM [Type]
-zonkTcTypesToTypes tys = initZonkEnv $ \ ze -> zonkTcTypesToTypesX ze tys
-
 zonkScaledTcTypeToTypeX :: ZonkEnv -> Scaled TcType -> TcM (Scaled TcType)
 zonkScaledTcTypeToTypeX env (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX env m
                                                    <*> zonkTcTypeToTypeX env ty