Never Anyify during kind inferencewip/T17567

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

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

30 files changed, 462 insertions, 91 deletions

diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index 1b1e56b314..dfbc50a20c 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -440,7 +440,7 @@ emptyLHsQTvs = HsQTvs { hsq_ext = [], hsq_explicit = [] }
 -- we use use HsOuterImplicit, wrapped around a HsForAllTy
 -- for the visible quantification
 --
--- See Note [forall-or-nothing] rule
+-- See Note [forall-or-nothing rule]
 
 -- | The outermost type variables in a type that obeys the @forall@-or-nothing
 -- rule. See @Note [forall-or-nothing rule]@.
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 50d4f72610..4a1dc3a8b6 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 13b5da759f..622f991a57 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -222,7 +222,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))
@@ -674,11 +674,12 @@ tc_patsyn_finish lname dir is_infix lpat'
   = 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 075c14a987..81fa2d1c58 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,
@@ -1294,6 +1295,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)
@@ -1372,7 +1396,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
@@ -1390,6 +1414,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
@@ -1410,7 +1448,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
@@ -1561,7 +1599,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.
@@ -1637,46 +1675,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
@@ -1686,9 +1699,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
@@ -1698,11 +1710,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
@@ -1812,6 +1820,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
@@ -1846,6 +1872,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 a1ca04b487..6638e2d80e 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -32,10 +32,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,
@@ -283,6 +283,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]
@@ -290,6 +294,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
@@ -451,10 +458,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
@@ -1835,6 +1838,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
 
@@ -1887,9 +1893,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
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
index 1188bf17d4..6fae39f5a1 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
@@ -128,7 +128,7 @@ gcast x = do  Refl <- eqT  (typeRep :: TypeRep a)
               return x
 
 data SameKind :: k -> k -> Type
-type CheckAppResult = SameKind AppResult AppResultNoKind
+
   --  not the most thorough check
 foo :: AppResult x -> AppResultNoKind x
 foo (App y z) = AppNoKind y z
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr
index 8c212a06b6..eab430ac83 100644
--- a/testsuite/tests/indexed-types/should_compile/T15852.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr
@@ -3,10 +3,10 @@ TYPE CONSTRUCTORS
     roles nominal nominal nominal
 COERCION AXIOMS
   axiom T15852.D:R:DFProxyProxy0 ::
-    forall k1 k2 (j :: k1) (c :: k2).
-      DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c
+    forall k1 (j :: k1) k2 (c :: k2).
+      DF (Proxy c) = T15852.R:DFProxyProxy k1 j k2 c
 FAMILY INSTANCES
-  data instance forall {k1} {k2} {j :: k1} {c :: k2}.
+  data instance forall {k1} {j :: k1} {k2} {c :: k2}.
                   DF (Proxy c) -- Defined at T15852.hs:10:15
 Dependent modules: []
 Dependent packages: [base-4.16.0.0, ghc-bignum-1.0, ghc-prim-0.8.0]
diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.stderr b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
index 795506e3b3..86d13d9ba8 100644
--- a/testsuite/tests/indexed-types/should_fail/T17008a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
@@ -1,7 +1,7 @@
 
 T17008a.hs:11:5: error:
-    • Type variable ‘a1’ is mentioned in the RHS,
+    • Type variable ‘a2’ is mentioned in the RHS,
         but not bound on the LHS of the family instance
-        The real LHS (expanding synonyms) is: F @a2 x
+        The real LHS (expanding synonyms) is: F @a1 x
     • In the equations for closed type family ‘F’
       In the type family declaration for ‘F’
diff --git a/testsuite/tests/polykinds/NestedProxies.hs b/testsuite/tests/polykinds/NestedProxies.hs
new file mode 100644
index 0000000000..d59d026544
--- /dev/null
+++ b/testsuite/tests/polykinds/NestedProxies.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE StarIsType #-}
+{-# OPTIONS_GHC -Wno-star-is-type #-}
+-- NB: -XNoPolyKinds. All the variables in the Proxies should be defaulted to *.
+
+module NestedProxies where
+
+import Data.Proxy
+
+-- | 'F1' docs
+type family F1 a b :: * -> *
+-- | 'F2' docs
+type family F2 a b :: * -> * where
+  F2 Int b = Maybe
+  F2 a   b = []
+-- | 'D' docs
+data family D a :: * -> *
+
+v :: Int
+v = 42
+
+-- | 'C' docs
+class C a where
+  -- | 'AT' docs
+  type AT a
+  type AT a = Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy (Proxy)))))))))
diff --git a/testsuite/tests/polykinds/T13393.hs b/testsuite/tests/polykinds/T13393.hs
index f1c4af3fa0..28cf87a6d5 100644
--- a/testsuite/tests/polykinds/T13393.hs
+++ b/testsuite/tests/polykinds/T13393.hs
@@ -28,7 +28,7 @@ newtype AacEncSt (rate :: Rate) channels (codec :: AacCodec) = MkAacEncSt
 
 -- makeLenses ''AacEncSt
 
-type Iso s t a b = forall p f. (Functor f) => (a -> f b) -> s -> (f t)
+type Iso s t a b = forall f. (Functor f) => (a -> f b) -> s -> (f t)
 instance (Monad m, Monoid w) => MonadState s (RWST r w s m) where
 
 iso :: (s -> a) -> (b -> t) -> Iso s t a b
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 52529f882a..c82f275f65 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -228,6 +228,7 @@ test('T18300', normal, compile_fail, [''])
 test('T18451', normal, compile_fail, [''])
 test('T18451a', normal, compile_fail, [''])
 test('T18451b', normal, compile_fail, [''])
+test('NestedProxies', normal, compile, [''])
 test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
 test('T18855', normal, compile, [''])
 test('T19092', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T17562b.hs b/testsuite/tests/typecheck/should_compile/T17562b.hs
new file mode 100644
index 0000000000..0d635d9248
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17562b.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses, TypeFamilies #-}
+-- NB: No PolyKinds
+
+module T17562b where
+
+class (forall a. a b ~ a c) => C b c
diff --git a/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.hs b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.hs
new file mode 100644
index 0000000000..36a4bca1e5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints, DatatypeContexts, TypeFamilies #-}
+-- NB: -XNoPolyKinds, to get defaulting.
+
+module T17567StupidThetaB where
+
+data (forall a. a b ~ a c) => T b c
diff --git a/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.stderr b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.stderr
new file mode 100644
index 0000000000..5e98268d8b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17567StupidThetaB.stderr
@@ -0,0 +1,3 @@
+
+T17567StupidThetaB.hs:1:37: warning:
+    -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3fc36839d8..8eac0df13c 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -729,6 +729,8 @@ test('T18831', normal, compile, [''])
 test('T18920', normal, compile, [''])
 test('T18939_Compile', normal, compile, [''])
 test('T15942', normal, compile, [''])
+test('T17562b', normal, compile, [''])
+test('T17567StupidThetaB', normal, compile, [''])
 test('ClassDefaultInHsBoot', [extra_files(['ClassDefaultInHsBootA1.hs','ClassDefaultInHsBootA2.hs','ClassDefaultInHsBootA2.hs-boot','ClassDefaultInHsBootA3.hs'])], multimod_compile, ['ClassDefaultInHsBoot', '-v0'])
 test('T17186', normal, compile, [''])
 test('CbvOverlap', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T15474.hs b/testsuite/tests/typecheck/should_fail/T15474.hs
new file mode 100644
index 0000000000..2fb68e8020
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15474.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module T15474 where
+
+import Data.Kind (Type)
+
+data Proxy a
+
+type Forall = forall t. Proxy t
+
+f1 :: forall (t :: Type). Proxy t
+f1 = f1
+
+f2 :: Forall
+f2 = f1
diff --git a/testsuite/tests/typecheck/should_fail/T15474.stderr b/testsuite/tests/typecheck/should_fail/T15474.stderr
new file mode 100644
index 0000000000..7fd96ebaa1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15474.stderr
@@ -0,0 +1,5 @@
+
+T15474.hs:9:1: error:
+    • Uninferrable type variable k0 in
+      the type synonym right-hand side: forall (t :: k0). Proxy @{k0} t
+    • In the type declaration for ‘Forall’
diff --git a/testsuite/tests/typecheck/should_fail/T17301.hs b/testsuite/tests/typecheck/should_fail/T17301.hs
new file mode 100644
index 0000000000..2fdaace98b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17301.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17301 where
+
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+
+data A = MkA
+data B (a :: A)
+
+data TySing ty where
+  SB :: TySing (B a)
+
+data ATySing where
+  MkATySing :: TySing ty -> ATySing
+
+type family Forget ty :: ATySing where
+  Forget (B a) = MkATySing SB
+
+type family Message ty where
+  Message (MkATySing (_ :: TySing ty)) =
+    TypeError ( ShowType ty )
+
+
+
+type KnownType = B MkA
+
+foo :: Message (Forget KnownType) => ()
+foo = ()
+
+bar :: ()
+bar = foo
diff --git a/testsuite/tests/typecheck/should_fail/T17301.stderr b/testsuite/tests/typecheck/should_fail/T17301.stderr
new file mode 100644
index 0000000000..7c7e20f005
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17301.stderr
@@ -0,0 +1,5 @@
+
+T17301.hs:22:3: error:
+    • Uninferrable type variable (a0 :: A) in
+      type family equation right-hand side: 'MkATySing @(B a0) ('SB @a0)
+    • In the type family declaration for ‘Forget’
diff --git a/testsuite/tests/typecheck/should_fail/T17562.hs b/testsuite/tests/typecheck/should_fail/T17562.hs
new file mode 100644
index 0000000000..a758a8cfe6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17562.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses, PolyKinds #-}
+-- NB: PolyKinds. This is actually accepted with -XNoPolyKinds because of defaulting.
+-- See T17562b for the NoPolyKinds case.
+
+module T17562 where
+
+class (forall a. a b ~ a c) => C b c
diff --git a/testsuite/tests/typecheck/should_fail/T17562.stderr b/testsuite/tests/typecheck/should_fail/T17562.stderr
new file mode 100644
index 0000000000..22086bdd0d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17562.stderr
@@ -0,0 +1,5 @@
+
+T17562.hs:7:1: error:
+    • Uninferrable type variable k0 in
+      the class context: forall (a :: k -> k0). (a b :: k0) ~ (a c :: k0)
+    • In the class declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/T17567.hs b/testsuite/tests/typecheck/should_fail/T17567.hs
new file mode 100644
index 0000000000..2ea82aae13
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE PolyKinds, RankNTypes #-}
+
+module T17567 where
+
+import Data.Proxy
+
+type T = forall a. Proxy a
+
+p :: T
+p = Proxy
+
+x :: Proxy a -> a
+x = undefined
+
+y = x p
diff --git a/testsuite/tests/typecheck/should_fail/T17567.stderr b/testsuite/tests/typecheck/should_fail/T17567.stderr
new file mode 100644
index 0000000000..75b4de2960
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567.stderr
@@ -0,0 +1,5 @@
+
+T17567.hs:7:1: error:
+    • Uninferrable type variable k0 in
+      the type synonym right-hand side: forall (a :: k0). Proxy @{k0} a
+    • In the type declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/T17567StupidTheta.hs b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.hs
new file mode 100644
index 0000000000..a023c0f7f8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints, DatatypeContexts, PolyKinds #-}
+-- NB: This actually works with -XNoPolyKinds, due to defaulting.
+
+module T17567StupidTheta where
+
+data (forall a. a b ~ a c) => T b c
diff --git a/testsuite/tests/typecheck/should_fail/T17567StupidTheta.stderr b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.stderr
new file mode 100644
index 0000000000..7ae2b35ab8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17567StupidTheta.stderr
@@ -0,0 +1,9 @@
+
+T17567StupidTheta.hs:1:37: warning:
+    -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
+
+T17567StupidTheta.hs:6:1: error:
+    • Uninferrable type variable k0 in
+      the datatype context:
+      forall (a :: k -> k0). (a b :: k0) ~ (a c :: k0)
+    • In the data declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index c55425ae3a..ba51bfb3ff 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -578,6 +578,11 @@ test('ExplicitSpecificity10', normal, compile_fail, [''])
 test('T18357', normal, compile_fail, [''])
 test('T18357a', normal, compile_fail, [''])
 test('T18357b', normal, compile_fail, [''])
+test('T17301', normal, compile_fail, [''])
+test('T17567', normal, compile_fail, [''])
+test('T17562', normal, compile_fail, [''])
+test('T17567StupidTheta', normal, compile_fail, [''])
+test('T15474', normal, compile_fail, [''])
 test('T18455', normal, compile_fail, [''])
 test('T18534', normal, compile_fail, [''])
 test('T18714', normal, compile_fail, [''])