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
-------------------------

24 files changed, 227 insertions, 101 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
+    }
diff --git a/docs/users_guide/exts/representation_polymorphism.rst b/docs/users_guide/exts/representation_polymorphism.rst
index 3e6d250d27..28b3cc78bf 100644
--- a/docs/users_guide/exts/representation_polymorphism.rst
+++ b/docs/users_guide/exts/representation_polymorphism.rst
@@ -114,14 +114,14 @@ Printing representation-polymorphic types
 -----------------------------------------
 
 .. ghc-flag:: -fprint-explicit-runtime-reps
-    :shortdesc: Print ``RuntimeRep`` variables in types which are
+    :shortdesc: Print ``RuntimeRep`` and ``Levity`` variables in types which are
         runtime-representation polymorphic.
     :type: dynamic
     :reverse: -fno-print-explicit-runtime-reps
     :category: verbosity
 
-    Print ``RuntimeRep`` parameters as they appear; otherwise, they are
-    defaulted to ``LiftedRep``.
+    Print ``RuntimeRep`` and ``Levity`` parameters as they appear;
+    otherwise, they are defaulted to ``LiftedRep`` and ``Lifted``, respectively.
 
 Most GHC users will not need to worry about representation polymorphism
 or unboxed types. For these users, seeing the representation polymorphism
diff --git a/testsuite/tests/indexed-types/should_compile/T17536.hs b/testsuite/tests/indexed-types/should_compile/T17536.hs
new file mode 100644
index 0000000000..b007dfecfe
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17536.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T17536 where
+
+import Data.Kind
+import GHC.Types
+
+type R :: RuntimeRep -> Type
+type family R r where
+  R _ = Int
+
+r :: R FloatRep -> Int
+r x = x
+
+type L :: Levity -> Type
+type family L l where
+  L _ = Int
+
+l :: L Unlifted -> Int
+l x = x
+
+type M :: Multiplicity -> Type
+type family M m where
+  M _ = Int
+
+g :: M One -> Int
+g x = x
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index c2f6b12aaf..9e0558cf5b 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -294,6 +294,7 @@ test('T16828', normal, compile, [''])
 test('T17008b', normal, compile, [''])
 test('T17056', normal, compile, [''])
 test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
+test('T17536', normal, compile, [''])
 test('T17923', normal, compile, [''])
 test('T18065', normal, compile, ['-O'])
 test('T18809', normal, compile, ['-O'])
diff --git a/testsuite/tests/indexed-types/should_fail/T9357.stderr b/testsuite/tests/indexed-types/should_fail/T9357.stderr
index daa735d45a..3cda558e9e 100644
--- a/testsuite/tests/indexed-types/should_fail/T9357.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9357.stderr
@@ -1,4 +1,4 @@
 
 T9357.hs:12:15: error:
-    • Illegal polymorphic type: forall a. a -> a
+    • Illegal polymorphic type: forall (a :: TYPE t). a -> a
     • In the type instance declaration for ‘F’
diff --git a/testsuite/tests/primops/should_fail/LevPolyPtrEquality3.hs b/testsuite/tests/primops/should_compile/LevPolyPtrEquality3.hs
index b5c3da4f91..b5c3da4f91 100644
--- a/testsuite/tests/primops/should_fail/LevPolyPtrEquality3.hs
+++ b/testsuite/tests/primops/should_compile/LevPolyPtrEquality3.hs
diff --git a/testsuite/tests/primops/should_compile/all.T b/testsuite/tests/primops/should_compile/all.T
index 412b64151b..1613313748 100644
--- a/testsuite/tests/primops/should_compile/all.T
+++ b/testsuite/tests/primops/should_compile/all.T
@@ -1,3 +1,4 @@
 test('T6135_should_compile', normal, compile, [''])
 test('T16293a', normal, compile, [''])
 test('T19851', normal, compile, ['-O'])
+test('LevPolyPtrEquality3', normal, compile, [''])
diff --git a/testsuite/tests/primops/should_fail/LevPolyPtrEquality3.stderr b/testsuite/tests/primops/should_fail/LevPolyPtrEquality3.stderr
deleted file mode 100644
index 88e44a6198..0000000000
--- a/testsuite/tests/primops/should_fail/LevPolyPtrEquality3.stderr
+++ /dev/null
@@ -1,15 +0,0 @@
-
-LevPolyPtrEquality3.hs:11:23: error:
-    • • Unsaturated use of a representation-polymorphic primitive function.
-        The first argument of ‘reallyUnsafePtrEquality#’
-        does not have a fixed runtime representation:
-          a0 :: TYPE ('GHC.Types.BoxedRep l0)
-      • Unsaturated use of a representation-polymorphic primitive function.
-        The second argument of ‘reallyUnsafePtrEquality#’
-        does not have a fixed runtime representation:
-          b0 :: TYPE ('GHC.Types.BoxedRep k0)
-    • In the first argument of ‘unsafeCoerce#’, namely
-        ‘reallyUnsafePtrEquality#’
-      In the expression: unsafeCoerce# reallyUnsafePtrEquality# a b
-      In an equation for ‘f’:
-          f a b = unsafeCoerce# reallyUnsafePtrEquality# a b
diff --git a/testsuite/tests/primops/should_fail/all.T b/testsuite/tests/primops/should_fail/all.T
deleted file mode 100644
index f599102c23..0000000000
--- a/testsuite/tests/primops/should_fail/all.T
+++ /dev/null
@@ -1 +0,0 @@
-test('LevPolyPtrEquality3', normal, compile_fail, [''])
diff --git a/testsuite/tests/rep-poly/T17536.hs b/testsuite/tests/rep-poly/T17536.hs
deleted file mode 100644
index 2361cc269f..0000000000
--- a/testsuite/tests/rep-poly/T17536.hs
+++ /dev/null
@@ -1,15 +0,0 @@
-{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}
-
-module T17536 where
-
-import Data.Kind
-import GHC.Exts
-
-data A (r :: RuntimeRep)
-
-type family IsA r where
-  IsA (A _) = Char
-  IsA _     = Int
-
-f :: IsA (A UnliftedRep)
-f = 'a'
diff --git a/testsuite/tests/rep-poly/all.T b/testsuite/tests/rep-poly/all.T
index 51038a56e8..c3b6e9eae6 100644
--- a/testsuite/tests/rep-poly/all.T
+++ b/testsuite/tests/rep-poly/all.T
@@ -11,7 +11,6 @@ test('T14561b', normal, compile_fail, [''])
 test('T14765', normal, compile_fail, [''])
 test('T17021', expect_broken(17201), compile, [''])
 test('T17360', normal, compile_fail, [''])
-test('T17536', expect_broken(17536), compile, [''])
 test('T17536b', expect_broken(17201), compile, [''])
 test('T17817', normal, compile_fail, [''])
 test('T18170a', [extra_files(['T18170c.hs'])], multimod_compile, ['T18170a.hs', '-v0'])
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs
index 6c1959e035..b6693d3d8a 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs
@@ -3,11 +3,12 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
 
 module UnliftedNewtypesOverlap where
 
-import GHC.Exts (TYPE)
+import GHC.Exts
 
 data family DF :: TYPE r
-data instance DF = MkDF4 | MkDF5
-newtype instance DF = MkDF6 Int
+data instance DF @LiftedRep = MkDF4 | MkDF5
+newtype instance DF @LiftedRep = MkDF6 Int
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr
index 808e8c0f60..3da742a1bf 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr
@@ -1,4 +1,5 @@
-UnliftedNewtypesOverlap.hs:12:15:
+
+UnliftedNewtypesOverlap.hs:13:15: error:
     Conflicting family instance declarations:
-      DF -- Defined at UnliftedNewtypesOverlap.hs:12:15
-      DF -- Defined at UnliftedNewtypesOverlap.hs:13:18
+      DF -- Defined at UnliftedNewtypesOverlap.hs:13:15
+      DF -- Defined at UnliftedNewtypesOverlap.hs:14:18
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
index a9cb694807..df7865f8d4 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
@@ -1,18 +1,32 @@
 
-UnliftedNewtypesUnassociatedFamilyFail.hs:21:30:
-     Expecting a lifted type, but ‘Int#’ is unlifted
-     In the type ‘Int#’
+UnliftedNewtypesUnassociatedFamilyFail.hs:21:30: error:
+    • Couldn't match kind ‘t’ with ‘'IntRep’
+      Expected a type, but ‘Int#’ has kind ‘TYPE 'IntRep’
+      ‘t’ is a rigid type variable bound by
+        the data constructor ‘MkDF1a’
+        at UnliftedNewtypesUnassociatedFamilyFail.hs:21:1-33
+    • In the type ‘Int#’
       In the definition of data constructor ‘MkDF1a’
       In the newtype instance declaration for ‘DF’
 
-UnliftedNewtypesUnassociatedFamilyFail.hs:22:30:
-     Expecting a lifted type, but ‘Word#’ is unlifted
-     In the type ‘Word#’
+UnliftedNewtypesUnassociatedFamilyFail.hs:22:30: error:
+    • Couldn't match kind ‘t’ with ‘'WordRep’
+      Expected a type, but ‘Word#’ has kind ‘TYPE 'WordRep’
+      ‘t’ is a rigid type variable bound by
+        the data constructor ‘MkDF2a’
+        at UnliftedNewtypesUnassociatedFamilyFail.hs:22:1-34
+    • In the type ‘Word#’
       In the definition of data constructor ‘MkDF2a’
       In the newtype instance declaration for ‘DF’
 
-UnliftedNewtypesUnassociatedFamilyFail.hs:23:30:
-     Expecting a lifted type, but ‘(# Int#, Word# #)’ is unlifted
-     In the type ‘(# Int#, Word# #)’
+UnliftedNewtypesUnassociatedFamilyFail.hs:23:30: error:
+    • Couldn't match kind ‘t’ with ‘'TupleRep '[ 'IntRep, 'WordRep]’
+      Expected a type,
+        but ‘(# Int#, Word# #)’ has kind ‘TYPE
+                                            ('TupleRep '[ 'IntRep, 'WordRep])’
+      ‘t’ is a rigid type variable bound by
+        the data constructor ‘MkDF3a’
+        at UnliftedNewtypesUnassociatedFamilyFail.hs:23:1-46
+    • In the type ‘(# Int#, Word# #)’
       In the definition of data constructor ‘MkDF3a’
       In the newtype instance declaration for ‘DF’
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs
index 443deadc1a..8315540fa3 100644
--- a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs
@@ -17,7 +17,8 @@ data instance F Int = TInt
 
 data family G a :: TYPE (BoxedRep l)
 
-data instance G Int = GInt
+data instance G Int :: Type where
+  GInt :: G Int
 data instance G Bool :: UnliftedType where
   GBool :: G Bool
 data instance G Char :: Type where
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/all.T b/testsuite/tests/unlifted-datatypes/should_fail/all.T
index f8e8c7c833..9ff585b9d6 100644
--- a/testsuite/tests/unlifted-datatypes/should_fail/all.T
+++ b/testsuite/tests/unlifted-datatypes/should_fail/all.T
@@ -1,2 +1,2 @@
-test('UnlDataNullaryPoly', normal, compile_fail, [''])
+test('UnlDataNullaryPoly', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('UnlDataInvalidResKind1', normal, compile_fail, [''])