Don't default type variables in type families

  This patch removes the following defaulting of type variables
  in type and data families:

    - type variables of kind RuntimeRep defaulting to LiftedRep
    - type variables of kind Levity defaulting to Lifted
    - type variables of kind Multiplicity defaulting to Many

  It does this by passing "defaulting options" to the `defaultTyVars`
  function; when calling from `tcTyFamInstEqnGuts` or
  `tcDataFamInstHeader` we pass options that avoid defaulting.

  This avoids wildcards being defaulted, which caused type families
  to unexpectedly fail to reduce.

  Note that kind defaulting, applicable only with -XNoPolyKinds,
  is not changed by this patch.

  Fixes #17536

-------------------------
Metric Increase:
    T12227
-------------------------

9 files changed, 157 insertions, 48 deletions

diff --git a/compiler/GHC/Core/Type.hs-boot b/compiler/GHC/Core/Type.hs-boot
index c38f6fc89d..e17cab9a40 100644
--- a/compiler/GHC/Core/Type.hs-boot
+++ b/compiler/GHC/Core/Type.hs-boot
@@ -19,6 +19,7 @@ piResultTy :: HasDebugCallStack => Type -> Type -> Type
 coreView :: Type -> Maybe Type
 tcView :: Type -> Maybe Type
 isRuntimeRepTy :: Type -> Bool
+isLevityTy :: Type -> Bool
 isMultiplicityTy :: Type -> Bool
 isLiftedTypeKind :: Type -> Bool
 tYPE :: Type -> Type
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index 422091784a..6251798a0a 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -73,8 +73,8 @@ import {-# SOURCE #-} GHC.Builtin.Types
                                  ( coercibleTyCon, heqTyCon
                                  , tupleTyConName
                                  , manyDataConTyCon, oneDataConTyCon
-                                 , liftedRepTyCon )
-import {-# SOURCE #-} GHC.Core.Type ( isRuntimeRepTy, isMultiplicityTy )
+                                 , liftedRepTyCon, liftedDataConTyCon )
+import {-# SOURCE #-} GHC.Core.Type ( isRuntimeRepTy, isMultiplicityTy, isLevityTy )
 
 import GHC.Core.TyCon hiding ( pprPromotionQuote )
 import GHC.Core.Coercion.Axiom
@@ -1002,7 +1002,7 @@ kind RuntimeRep to LiftedRep.
 Likewise, we default all Multiplicity variables to Many.
 
 This is done in a pass right before pretty-printing
-(defaultNonStandardVars, controlled by
+(defaultIfaceTyVarsOfKind, controlled by
 -fprint-explicit-runtime-reps and -XLinearTypes)
 
 This applies to /quantified/ variables like 'w' above.  What about
@@ -1028,7 +1028,8 @@ as they appear during kind-checking of "newtype T :: TYPE r where..."
 (test T18357a). Therefore, we additionally test for isTyConableTyVar.
 -}
 
--- | Default 'RuntimeRep' variables to 'LiftedRep', and 'Multiplicity'
+-- | Default 'RuntimeRep' variables to 'LiftedRep',
+--   'Levity' variables to 'Lifted', and 'Multiplicity'
 --   variables to 'Many'. For example:
 --
 -- @
@@ -1042,14 +1043,15 @@ as they appear during kind-checking of "newtype T :: TYPE r where..."
 -- @ ($) :: forall a (b :: *). (a -> b) -> a -> b @
 -- @ Just :: forall a . a -> Maybe a @
 --
--- We do this to prevent RuntimeRep and Multiplicity variables from
+-- We do this to prevent RuntimeRep, Levity and Multiplicity variables from
 -- incurring a significant syntactic overhead in otherwise simple
 -- type signatures (e.g. ($)). See Note [Defaulting RuntimeRep variables]
 -- and #11549 for further discussion.
-defaultNonStandardVars :: Bool -> Bool -> IfaceType -> IfaceType
-defaultNonStandardVars do_runtimereps do_multiplicities ty = go emptyFsEnv ty
+defaultIfaceTyVarsOfKind :: DefaultVarsOfKind
+                         -> IfaceType -> IfaceType
+defaultIfaceTyVarsOfKind def_ns_vars ty = go emptyFsEnv ty
   where
-    go :: FastStringEnv IfaceType -- Set of enclosing forall-ed RuntimeRep/Multiplicity variables
+    go :: FastStringEnv IfaceType -- Set of enclosing forall-ed RuntimeRep/Levity/Multiplicity variables
        -> IfaceType
        -> IfaceType
     go subs (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
@@ -1057,7 +1059,7 @@ defaultNonStandardVars do_runtimereps do_multiplicities ty = go emptyFsEnv ty
                                 -- or we get the mess in #13963
      , Just substituted_ty <- check_substitution var_kind
       = let subs' = extendFsEnv subs var substituted_ty
-            -- Record that we should replace it with LiftedRep,
+            -- Record that we should replace it with LiftedRep/Lifted/Many,
             -- and recurse, discarding the forall
         in go subs' ty
 
@@ -1070,11 +1072,18 @@ defaultNonStandardVars do_runtimereps do_multiplicities ty = go emptyFsEnv ty
 
     go _ ty@(IfaceFreeTyVar tv)
       -- See Note [Defaulting RuntimeRep variables], about free vars
-      | do_runtimereps && GHC.Core.Type.isRuntimeRepTy (tyVarKind tv)
+      | def_runtimeRep def_ns_vars
+      , GHC.Core.Type.isRuntimeRepTy (tyVarKind tv)
       , isMetaTyVar tv
       , isTyConableTyVar tv
       = liftedRep_ty
-      | do_multiplicities && GHC.Core.Type.isMultiplicityTy (tyVarKind tv)
+      | def_levity def_ns_vars
+      , GHC.Core.Type.isLevityTy (tyVarKind tv)
+      , isMetaTyVar tv
+      , isTyConableTyVar tv
+      = lifted_ty
+      | def_multiplicity def_ns_vars
+      , GHC.Core.Type.isMultiplicityTy (tyVarKind tv)
       , isMetaTyVar tv
       , isTyConableTyVar tv
       = many_ty
@@ -1112,8 +1121,15 @@ defaultNonStandardVars do_runtimereps do_multiplicities ty = go emptyFsEnv ty
 
     check_substitution :: IfaceType -> Maybe IfaceType
     check_substitution (IfaceTyConApp tc _)
-        | do_runtimereps, tc `ifaceTyConHasKey` runtimeRepTyConKey = Just liftedRep_ty
-        | do_multiplicities, tc `ifaceTyConHasKey` multiplicityTyConKey = Just many_ty
+        | def_runtimeRep def_ns_vars
+        , tc `ifaceTyConHasKey` runtimeRepTyConKey
+        = Just liftedRep_ty
+        | def_levity def_ns_vars
+        , tc `ifaceTyConHasKey` levityTyConKey
+        = Just lifted_ty
+        | def_multiplicity def_ns_vars
+        , tc `ifaceTyConHasKey` multiplicityTyConKey
+        = Just many_ty
     check_substitution _ = Nothing
 
 -- | The type ('BoxedRep 'Lifted), also known as LiftedRep.
@@ -1125,6 +1141,14 @@ liftedRep_ty =
     liftedRep = IfaceTyCon tc_name (mkIfaceTyConInfo NotPromoted IfaceNormalTyCon)
       where tc_name = getName liftedRepTyCon
 
+-- | The type 'Lifted :: Levity'.
+lifted_ty :: IfaceType
+lifted_ty =
+    IfaceTyConApp (IfaceTyCon dc_name (mkIfaceTyConInfo IsPromoted IfaceNormalTyCon))
+                  IA_Nil
+  where dc_name = getName liftedDataConTyCon
+
+-- | The type 'Many :: Multiplicity'.
 many_ty :: IfaceType
 many_ty =
     IfaceTyConApp (IfaceTyCon dc_name (mkIfaceTyConInfo IsPromoted IfaceNormalTyCon))
@@ -1136,10 +1160,13 @@ hideNonStandardTypes f ty
   = sdocOption sdocPrintExplicitRuntimeReps $ \printExplicitRuntimeReps ->
     sdocOption sdocLinearTypes $ \linearTypes ->
     getPprStyle      $ \sty    ->
-    let do_runtimerep = not printExplicitRuntimeReps
-        do_multiplicity = not linearTypes
+    let def_opts =
+          DefaultVarsOfKind
+            { def_runtimeRep   = not printExplicitRuntimeReps
+            , def_levity       = not printExplicitRuntimeReps
+            , def_multiplicity = not linearTypes }
     in if userStyle sty
-       then f (defaultNonStandardVars do_runtimerep do_multiplicity ty)
+       then f (defaultIfaceTyVarsOfKind def_opts ty)
        else f ty
 
 instance Outputable IfaceAppArgs where
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 10a8953d29..6f01091200 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2396,7 +2396,7 @@ kcCheckDeclHeader_cusk name flav
              candidates = candidates' { dv_kvs = dv_kvs candidates' `extendDVarSetList` non_tc_candidates }
              inf_candidates = candidates `delCandidates` spec_req_tkvs
 
-       ; inferred <- quantifyTyVars inf_candidates
+       ; inferred <- quantifyTyVars allVarsOfKindDefault inf_candidates
                      -- NB: 'inferred' comes back sorted in dependency order
 
        ; scoped_kvs <- mapM zonkTyCoVarKind scoped_kvs
@@ -3505,7 +3505,7 @@ kindGeneralizeSome wanted kind_or_type
          -- thus, every free variable is really a kv, never a tv.
        ; dvs <- candidateQTyVarsOfKind kind_or_type
        ; dvs <- filterConstrainedCandidates wanted dvs
-       ; quantifyTyVars dvs }
+       ; quantifyTyVars allVarsOfKindDefault dvs }
 
 filterConstrainedCandidates
   :: WantedConstraints    -- Don't quantify over variables free in these
@@ -3533,7 +3533,7 @@ kindGeneralizeAll :: TcType -> TcM [KindVar]
 kindGeneralizeAll kind_or_type
   = do { traceTc "kindGeneralizeAll" (ppr kind_or_type)
        ; dvs <- candidateQTyVarsOfKind kind_or_type
-       ; quantifyTyVars dvs }
+       ; quantifyTyVars allVarsOfKindDefault dvs }
 
 -- | Specialized version of 'kindGeneralizeSome', but where no variables
 -- can be generalized, but perhaps some may need to be promoted.
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index 46b1e16313..a712ab4020 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -30,7 +30,7 @@ import GHC.Core.TyCon( isTypeFamilyTyCon )
 import GHC.Types.Id
 import GHC.Types.Var( EvVar )
 import GHC.Types.Var.Set
-import GHC.Types.Basic ( RuleName )
+import GHC.Types.Basic ( RuleName, allVarsOfKindDefault )
 import GHC.Types.SrcLoc
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
@@ -151,7 +151,7 @@ tcRule (HsRule { rd_ext  = ext
 
        -- See Note [Re-quantify type variables in rules]
        ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids)
-       ; qtkvs <- quantifyTyVars forall_tkvs
+       ; qtkvs <- quantifyTyVars allVarsOfKindDefault forall_tkvs
        ; traceTc "tcRule" (vcat [ pprFullRuleName rname
                                 , ppr forall_tkvs
                                 , ppr qtkvs
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 74a53ff348..389720d8f0 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -58,13 +58,14 @@ import GHC.Core.Predicate
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType
 import GHC.Core.Type
-import GHC.Builtin.Types ( liftedRepTy, manyDataConTy )
+import GHC.Builtin.Types ( liftedRepTy, manyDataConTy, liftedDataConTy )
 import GHC.Core.Unify    ( tcMatchTyKi )
 import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Types.Var
 import GHC.Types.Var.Set
-import GHC.Types.Basic    ( IntWithInf, intGtLimit )
+import GHC.Types.Basic    ( IntWithInf, intGtLimit
+                          , DefaultKindVars(..), allVarsOfKindDefault )
 import GHC.Types.Error
 import qualified GHC.LanguageExtensions as LangExt
 
@@ -1051,7 +1052,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                                    , pred <- sig_inst_theta sig ]
 
        ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)
-       ; qtkvs <- quantifyTyVars dep_vars
+       ; qtkvs <- quantifyTyVars allVarsOfKindDefault dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
        ; return (qtkvs, [], emptyTcEvBinds, False) }
 
@@ -1503,7 +1504,10 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
       | tv `elemVarSet` mono_tvs
       = return False
       | otherwise
-      = defaultTyVar (not poly_kinds && is_kind_var) tv
+      = defaultTyVar
+          (if not poly_kinds && is_kind_var then DefaultKinds else Don'tDefaultKinds)
+          allVarsOfKindDefault
+          tv
 
     simplify_cand candidates
       = do { clone_wanteds <- newWanteds DefaultOrigin candidates
@@ -1563,7 +1567,7 @@ decideQuantifiedTyVars name_taus psigs candidates
            , text "grown_tcvs =" <+> ppr grown_tcvs
            , text "dvs =" <+> ppr dvs_plus])
 
-       ; quantifyTyVars dvs_plus }
+       ; quantifyTyVars allVarsOfKindDefault dvs_plus }
 
 ------------------
 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
@@ -2398,6 +2402,11 @@ defaultTyVarTcS the_tv
   = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
        ; unifyTyVar the_tv liftedRepTy
        ; return True }
+  | isLevityVar the_tv
+  , not (isTyVarTyVar the_tv)
+  = do { traceTcS "defaultTyVarTcS Levity" (ppr the_tv)
+       ; unifyTyVar the_tv liftedDataConTy
+       ; return True }
   | isMultiplicityVar the_tv
   , not (isTyVarTyVar the_tv)  -- TyVarTvs should only be unified with a tyvar
                              -- never with a type; c.f. TcMType.defaultTyVar
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 713d3f173b..dc12ac0735 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -907,7 +907,7 @@ generaliseTcTyCon (tc, scoped_prs, tc_res_kind)
 
        -- Step 2b: quantify, mainly meaning skolemise the free variables
        -- Returned 'inferred' are scope-sorted and skolemised
-       ; inferred <- quantifyTyVars dvs2
+       ; inferred <- quantifyTyVars allVarsOfKindDefault dvs2
 
        ; traceTc "generaliseTcTyCon: pre zonk"
            (vcat [ text "tycon =" <+> ppr tc
@@ -2701,7 +2701,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
                               , fdInjectivityAnn = inj })
   | DataFamily <- fam_info
   = bindTyClTyVars tc_name $ \ _ binders res_kind -> do
-  { traceTc "data family:" (ppr tc_name)
+  { traceTc "tcFamDecl1 data family:" (ppr tc_name)
   ; checkFamFlag tc_name
 
   -- Check that the result kind is OK
@@ -2727,7 +2727,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
 
   | OpenTypeFamily <- fam_info
   = bindTyClTyVars tc_name $ \ _ binders res_kind -> do
-  { traceTc "open type family:" (ppr tc_name)
+  { traceTc "tcFamDecl1 open type family:" (ppr tc_name)
   ; checkFamFlag tc_name
   ; inj' <- tcInjectivity binders inj
   ; checkResultSigFlag tc_name sig  -- check after injectivity for better errors
@@ -2739,7 +2739,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   | ClosedTypeFamily mb_eqns <- fam_info
   = -- Closed type families are a little tricky, because they contain the definition
     -- of both the type family and the equations for a CoAxiom.
-    do { traceTc "Closed type family:" (ppr tc_name)
+    do { traceTc "tcFamDecl1 Closed type family:" (ppr tc_name)
          -- the variables in the header scope only over the injectivity
          -- declaration but this is not involved here
        ; (inj', binders, res_kind)
@@ -3140,7 +3140,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
 
        -- See Note [Generalising in tcTyFamInstEqnGuts]
        ; dvs  <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys outer_tvs)
-       ; qtvs <- quantifyTyVars dvs
+       ; qtvs <- quantifyTyVars noVarsOfKindDefault dvs
        ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
        ; checkFamTelescope tclvl outer_hs_bndrs outer_tvs
 
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 23c9fd8fff..aac81d2cfa 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -915,7 +915,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
 
        -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
        ; dvs  <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
-       ; qtvs <- quantifyTyVars dvs
+       ; qtvs <- quantifyTyVars noVarsOfKindDefault dvs
        ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
 
        -- Zonk the patterns etc into the Type world
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 7be996a789..9f6d1e1284 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -128,7 +128,8 @@ import GHC.Types.Error
 import GHC.Types.Var.Env
 import GHC.Types.Name.Env
 import GHC.Types.Unique.Set
-import GHC.Types.Basic ( TypeOrKind(..) )
+import GHC.Types.Basic ( TypeOrKind(..)
+                       , DefaultKindVars(..), DefaultVarsOfKind(..), allVarsOfKindDefault )
 
 import GHC.Data.FastString
 import GHC.Data.Bag
@@ -1690,7 +1691,8 @@ For more information about deterministic sets see
 Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
 -}
 
-quantifyTyVars :: CandidatesQTvs   -- See Note [Dependent type variables]
+quantifyTyVars :: DefaultVarsOfKind
+               -> CandidatesQTvs   -- See Note [Dependent type variables]
                                    -- Already zonked
                -> TcM [TcTyVar]
 -- See Note [quantifyTyVars]
@@ -1700,16 +1702,18 @@ 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
+quantifyTyVars def_varsOfKind dvs
        -- short-circuit common case
   | isEmptyCandidates dvs
   = do { traceTc "quantifyTyVars has nothing to quantify" empty
        ; return [] }
 
   | otherwise
-  = do { traceTc "quantifyTyVars {" (ppr dvs)
+  = do { traceTc "quantifyTyVars {"
+           ( vcat [ text "def_varsOfKind =" <+> ppr def_varsOfKind
+                  , text "dvs =" <+> ppr dvs ])
 
-       ; undefaulted <- defaultTyVars dvs
+       ; undefaulted <- defaultTyVars def_varsOfKind dvs
        ; final_qtvs  <- mapMaybeM zonk_quant undefaulted
 
        ; traceTc "quantifyTyVars }"
@@ -1787,11 +1791,12 @@ skolemiseQuantifiedTyVar tv
 
       _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk
 
-defaultTyVar :: Bool      -- True <=> please default this kind variable to *
+defaultTyVar :: DefaultKindVars
+             -> DefaultVarsOfKind
              -> TcTyVar   -- If it's a MetaTyVar then it is unbound
              -> TcM Bool  -- True <=> defaulted away altogether
 
-defaultTyVar default_kind tv
+defaultTyVar def_kindVars def_varsOfKind tv
   | not (isMetaTyVar tv)
   = return False
 
@@ -1803,22 +1808,26 @@ defaultTyVar default_kind tv
   = return False
 
 
-  | isRuntimeRepVar tv  -- Do not quantify over a RuntimeRep var
-                        -- unless it is a TyVarTv, handled earlier
+  | isRuntimeRepVar tv
+  , def_runtimeRep def_varsOfKind
+  -- Do not quantify over a RuntimeRep var
+  -- unless it is a TyVarTv, handled earlier
   = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
        ; writeMetaTyVar tv liftedRepTy
        ; return True }
   | isLevityVar tv
+  , def_levity def_varsOfKind
   = do { traceTc "Defaulting a Levity var to Lifted" (ppr tv)
        ; writeMetaTyVar tv liftedDataConTy
        ; return True }
   | isMultiplicityVar tv
+  , def_multiplicity def_varsOfKind
   = do { traceTc "Defaulting a Multiplicty var to Many" (ppr tv)
        ; writeMetaTyVar tv manyDataConTy
        ; return True }
 
-  | default_kind            -- -XNoPolyKinds and this is a kind var
-  = default_kind_var tv     -- so default it to * if possible
+  | DefaultKinds <- def_kindVars -- -XNoPolyKinds and this is a kind var
+  = default_kind_var tv          -- so default it to * if possible
 
   | otherwise
   = return False
@@ -1855,12 +1864,15 @@ defaultTyVar default_kind tv
 --     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
+defaultTyVars :: DefaultVarsOfKind
+              -> CandidatesQTvs  -- ^ all candidates for quantification
               -> TcM [TcTyVar]   -- ^ those variables not defaulted
-defaultTyVars dvs
+defaultTyVars def_varsOfKind dvs
   = do { poly_kinds <- xoptM LangExt.PolyKinds
-       ; defaulted_kvs <- mapM (defaultTyVar (not poly_kinds)) dep_kvs
-       ; defaulted_tvs <- mapM (defaultTyVar False)            nondep_tvs
+       ; let
+           def_kinds = if poly_kinds then Don'tDefaultKinds else DefaultKinds
+       ; defaulted_kvs <- mapM (defaultTyVar def_kinds         def_varsOfKind ) dep_kvs
+       ; defaulted_tvs <- mapM (defaultTyVar Don'tDefaultKinds def_varsOfKind ) 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) }
@@ -2017,7 +2029,7 @@ doNotQuantifyTyVars dvs where_found
 
   | otherwise
   = do { traceTc "doNotQuantifyTyVars" (ppr dvs)
-       ; undefaulted <- defaultTyVars dvs
+       ; undefaulted <- defaultTyVars allVarsOfKindDefault 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`
diff --git a/compiler/GHC/Types/Basic.hs b/compiler/GHC/Types/Basic.hs
index 342d9d3688..8717d30a4b 100644
--- a/compiler/GHC/Types/Basic.hs
+++ b/compiler/GHC/Types/Basic.hs
@@ -101,6 +101,9 @@ module GHC.Types.Basic (
 
         TypeOrKind(..), isTypeLevel, isKindLevel,
 
+        DefaultKindVars(..), DefaultVarsOfKind(..),
+        allVarsOfKindDefault, noVarsOfKindDefault,
+
         ForeignSrcLang (..)
    ) where
 
@@ -1745,3 +1748,60 @@ isTypeLevel KindLevel = False
 isKindLevel :: TypeOrKind -> Bool
 isKindLevel TypeLevel = False
 isKindLevel KindLevel = True
+
+{- *********************************************************************
+*                                                                      *
+                        Defaulting options
+*                                                                      *
+********************************************************************* -}
+
+-- | Whether to default kind variables. Usually: no, unless `-XNoPolyKinds`
+-- is enabled.
+data DefaultKindVars
+  = Don'tDefaultKinds
+  | DefaultKinds
+
+instance Outputable DefaultKindVars where
+  ppr Don'tDefaultKinds = text "Don'tDefaultKinds"
+  ppr DefaultKinds = text "DefaultKinds"
+
+-- | Whether to default type variables of the given kinds:
+--
+--   - default 'RuntimeRep' variables to LiftedRep?
+--   - default 'Levity' variables to Lifted?
+--   - default 'Multiplicity' variables to Many?
+data DefaultVarsOfKind =
+  DefaultVarsOfKind
+    { def_runtimeRep, def_levity, def_multiplicity :: !Bool }
+
+instance Outputable DefaultVarsOfKind where
+  ppr
+    (DefaultVarsOfKind
+      { def_runtimeRep   = rep
+      , def_levity       = lev
+      , def_multiplicity = mult })
+    = text "DefaultVarsOfKind:" <+> defaults
+      where
+        defaults :: SDoc
+        defaults =
+          case filter snd $ [ ("RuntimeRep", rep), ("Levity", lev), ("Multiplicity", mult)] of
+            []   -> text "<no defaulting>"
+            defs -> hsep (map (text . fst) defs)
+
+-- | Do defaulting for variables of kind `RuntimeRep`, `Levity` and `Multiplicity`.
+allVarsOfKindDefault :: DefaultVarsOfKind
+allVarsOfKindDefault =
+  DefaultVarsOfKind
+    { def_runtimeRep   = True
+    , def_levity       = True
+    , def_multiplicity = True
+    }
+
+-- | Don't do defaulting for variables of kind `RuntimeRep`, `Levity` and `Multiplicity`.
+noVarsOfKindDefault :: DefaultVarsOfKind
+noVarsOfKindDefault =
+  DefaultVarsOfKind
+    { def_runtimeRep   = False
+    , def_levity       = False
+    , def_multiplicity = False
+    }