Default kind vars in tyfams with -XNoPolyKinds

  We should still default kind variables in type families
  in the presence of -XNoPolyKinds, to avoid suggesting enabling
  -XPolyKinds just because the function arrow introduced kind variables,
  e.g.

    type family F (t :: Type) :: Type where
      F (a -> b) = b

  With -XNoPolyKinds, we should still default `r :: RuntimeRep`
  in `a :: TYPE r`.

  Fixes #20584

15 files changed, 376 insertions, 109 deletions

diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index c3ef8b9b65..407b474bac 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -1048,9 +1048,10 @@ as they appear during kind-checking of "newtype T :: TYPE r where..."
 -- incurring a significant syntactic overhead in otherwise simple
 -- type signatures (e.g. ($)). See Note [Defaulting RuntimeRep variables]
 -- and #11549 for further discussion.
-defaultIfaceTyVarsOfKind :: DefaultVarsOfKind
+defaultIfaceTyVarsOfKind :: Bool -- ^ default 'RuntimeRep'/'Levity' variables?
+                         -> Bool -- ^ default 'Multiplicity' variables?
                          -> IfaceType -> IfaceType
-defaultIfaceTyVarsOfKind def_ns_vars ty = go emptyFsEnv ty
+defaultIfaceTyVarsOfKind def_rep def_mult ty = go emptyFsEnv ty
   where
     go :: FastStringEnv IfaceType -- Set of enclosing forall-ed RuntimeRep/Levity/Multiplicity variables
        -> IfaceType
@@ -1073,17 +1074,17 @@ defaultIfaceTyVarsOfKind def_ns_vars ty = go emptyFsEnv ty
 
     go _ ty@(IfaceFreeTyVar tv)
       -- See Note [Defaulting RuntimeRep variables], about free vars
-      | def_runtimeRep def_ns_vars
+      | def_rep
       , GHC.Core.Type.isRuntimeRepTy (tyVarKind tv)
       , isMetaTyVar tv
       , isTyConableTyVar tv
       = liftedRep_ty
-      | def_levity def_ns_vars
+      | def_rep
       , GHC.Core.Type.isLevityTy (tyVarKind tv)
       , isMetaTyVar tv
       , isTyConableTyVar tv
       = lifted_ty
-      | def_multiplicity def_ns_vars
+      | def_mult
       , GHC.Core.Type.isMultiplicityTy (tyVarKind tv)
       , isMetaTyVar tv
       , isTyConableTyVar tv
@@ -1122,13 +1123,13 @@ defaultIfaceTyVarsOfKind def_ns_vars ty = go emptyFsEnv ty
 
     check_substitution :: IfaceType -> Maybe IfaceType
     check_substitution (IfaceTyConApp tc _)
-        | def_runtimeRep def_ns_vars
+        | def_rep
         , tc `ifaceTyConHasKey` runtimeRepTyConKey
         = Just liftedRep_ty
-        | def_levity def_ns_vars
+        | def_rep
         , tc `ifaceTyConHasKey` levityTyConKey
         = Just lifted_ty
-        | def_multiplicity def_ns_vars
+        | def_mult
         , tc `ifaceTyConHasKey` multiplicityTyConKey
         = Just many_ty
     check_substitution _ = Nothing
@@ -1161,13 +1162,10 @@ hideNonStandardTypes f ty
   = sdocOption sdocPrintExplicitRuntimeReps $ \printExplicitRuntimeReps ->
     sdocOption sdocLinearTypes $ \linearTypes ->
     getPprStyle      $ \sty    ->
-    let def_opts =
-          DefaultVarsOfKind
-            { def_runtimeRep   = not printExplicitRuntimeReps
-            , def_levity       = not printExplicitRuntimeReps
-            , def_multiplicity = not linearTypes }
+    let def_rep  = not printExplicitRuntimeReps
+        def_mult = not linearTypes
     in if userStyle sty
-       then f (defaultIfaceTyVarsOfKind def_opts ty)
+       then f (defaultIfaceTyVarsOfKind def_rep def_mult 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 3c502c557d..6fd2be5b05 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 allVarsOfKindDefault inf_candidates
+       ; inferred <- quantifyTyVars DefaultNonStandardTyVars 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 allVarsOfKindDefault dvs }
+       ; quantifyTyVars DefaultNonStandardTyVars 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 allVarsOfKindDefault dvs }
+       ; quantifyTyVars DefaultNonStandardTyVars 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 0fabfa626c..10dffa2648 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, allVarsOfKindDefault )
+import GHC.Types.Basic ( RuleName, NonStandardDefaultingStrategy(..) )
 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 allVarsOfKindDefault forall_tkvs
+       ; qtkvs <- quantifyTyVars DefaultNonStandardTyVars 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 389720d8f0..2edd1bad8d 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -65,7 +65,7 @@ import GHC.Utils.Panic
 import GHC.Types.Var
 import GHC.Types.Var.Set
 import GHC.Types.Basic    ( IntWithInf, intGtLimit
-                          , DefaultKindVars(..), allVarsOfKindDefault )
+                          , DefaultingStrategy(..), NonStandardDefaultingStrategy(..) )
 import GHC.Types.Error
 import qualified GHC.LanguageExtensions as LangExt
 
@@ -1052,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 allVarsOfKindDefault dep_vars
+       ; qtkvs <- quantifyTyVars DefaultNonStandardTyVars dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
        ; return (qtkvs, [], emptyTcEvBinds, False) }
 
@@ -1505,8 +1505,10 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
       = return False
       | otherwise
       = defaultTyVar
-          (if not poly_kinds && is_kind_var then DefaultKinds else Don'tDefaultKinds)
-          allVarsOfKindDefault
+          (if not poly_kinds && is_kind_var
+           then DefaultKindVars
+           else NonStandardDefaulting DefaultNonStandardTyVars)
+          -- NB: only pass 'DefaultKindVars' when we know we're dealing with a kind variable.
           tv
 
     simplify_cand candidates
@@ -1567,7 +1569,7 @@ decideQuantifiedTyVars name_taus psigs candidates
            , text "grown_tcvs =" <+> ppr grown_tcvs
            , text "dvs =" <+> ppr dvs_plus])
 
-       ; quantifyTyVars allVarsOfKindDefault dvs_plus }
+       ; quantifyTyVars DefaultNonStandardTyVars dvs_plus }
 
 ------------------
 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 5dfa4cec86..f6f648d718 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 allVarsOfKindDefault dvs2
+       ; inferred <- quantifyTyVars DefaultNonStandardTyVars dvs2
 
        ; traceTc "generaliseTcTyCon: pre zonk"
            (vcat [ text "tycon =" <+> ppr tc
@@ -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 noVarsOfKindDefault dvs
+       ; qtvs <- quantifyTyVars TryNotToDefaultNonStandardTyVars 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 aac81d2cfa..f6ebd07c04 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 noVarsOfKindDefault dvs
+       ; qtvs <- quantifyTyVars TryNotToDefaultNonStandardTyVars 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 9f6d1e1284..d4637705b0 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -129,7 +129,8 @@ import GHC.Types.Var.Env
 import GHC.Types.Name.Env
 import GHC.Types.Unique.Set
 import GHC.Types.Basic ( TypeOrKind(..)
-                       , DefaultKindVars(..), DefaultVarsOfKind(..), allVarsOfKindDefault )
+                       , NonStandardDefaultingStrategy(..)
+                       , DefaultingStrategy(..), defaultNonStandardTyVars )
 
 import GHC.Data.FastString
 import GHC.Data.Bag
@@ -1691,7 +1692,7 @@ For more information about deterministic sets see
 Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
 -}
 
-quantifyTyVars :: DefaultVarsOfKind
+quantifyTyVars :: NonStandardDefaultingStrategy
                -> CandidatesQTvs   -- See Note [Dependent type variables]
                                    -- Already zonked
                -> TcM [TcTyVar]
@@ -1702,7 +1703,7 @@ quantifyTyVars :: DefaultVarsOfKind
 -- 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 def_varsOfKind dvs
+quantifyTyVars ns_strat dvs
        -- short-circuit common case
   | isEmptyCandidates dvs
   = do { traceTc "quantifyTyVars has nothing to quantify" empty
@@ -1710,10 +1711,10 @@ quantifyTyVars def_varsOfKind dvs
 
   | otherwise
   = do { traceTc "quantifyTyVars {"
-           ( vcat [ text "def_varsOfKind =" <+> ppr def_varsOfKind
+           ( vcat [ text "ns_strat =" <+> ppr ns_strat
                   , text "dvs =" <+> ppr dvs ])
 
-       ; undefaulted <- defaultTyVars def_varsOfKind dvs
+       ; undefaulted <- defaultTyVars ns_strat dvs
        ; final_qtvs  <- mapMaybeM zonk_quant undefaulted
 
        ; traceTc "quantifyTyVars }"
@@ -1791,12 +1792,13 @@ skolemiseQuantifiedTyVar tv
 
       _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk
 
-defaultTyVar :: DefaultKindVars
-             -> DefaultVarsOfKind
-             -> TcTyVar   -- If it's a MetaTyVar then it is unbound
-             -> TcM Bool  -- True <=> defaulted away altogether
-
-defaultTyVar def_kindVars def_varsOfKind tv
+-- | Default a type variable using the given defaulting strategy.
+--
+-- See Note [Type variable defaulting options] in GHC.Types.Basic.
+defaultTyVar :: DefaultingStrategy
+             -> TcTyVar    -- If it's a MetaTyVar then it is unbound
+             -> TcM Bool   -- True <=> defaulted away altogether
+defaultTyVar def_strat tv
   | not (isMetaTyVar tv)
   = return False
 
@@ -1807,32 +1809,33 @@ defaultTyVar def_kindVars def_varsOfKind tv
     -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
   = return False
 
-
   | isRuntimeRepVar tv
-  , def_runtimeRep def_varsOfKind
+  , default_ns_vars
   -- 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
+  , default_ns_vars
   = 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)
+  , default_ns_vars
+  = do { traceTc "Defaulting a Multiplicity var to Many" (ppr tv)
        ; writeMetaTyVar tv manyDataConTy
        ; return True }
 
-  | DefaultKinds <- def_kindVars -- -XNoPolyKinds and this is a kind var
-  = default_kind_var tv          -- so default it to * if possible
+  | DefaultKindVars <- def_strat -- -XNoPolyKinds and this is a kind var: we must default it
+  = default_kind_var tv
 
   | otherwise
   = return False
 
   where
+    default_ns_vars :: Bool
+    default_ns_vars = defaultNonStandardTyVars def_strat
     default_kind_var :: TyVar -> TcM Bool
        -- defaultKindVar is used exclusively with -XNoPolyKinds
        -- See Note [Defaulting with -XNoPolyKinds]
@@ -1859,20 +1862,37 @@ defaultTyVar def_kindVars def_varsOfKind 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 :: DefaultVarsOfKind
-              -> CandidatesQTvs  -- ^ all candidates for quantification
-              -> TcM [TcTyVar]   -- ^ those variables not defaulted
-defaultTyVars def_varsOfKind dvs
+-- | Default some unconstrained type variables, as specified
+-- by the defaulting options:
+--
+--  - 'RuntimeRep' tyvars default to 'LiftedRep'
+--  - 'Levity' tyvars default to 'Lifted'
+--  - '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 :: NonStandardDefaultingStrategy
+              -> CandidatesQTvs    -- ^ all candidates for quantification
+              -> TcM [TcTyVar]     -- ^ those variables not defaulted
+defaultTyVars ns_strat dvs
   = do { poly_kinds <- xoptM LangExt.PolyKinds
        ; 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
+           def_tvs, def_kvs :: DefaultingStrategy
+           def_tvs = NonStandardDefaulting ns_strat
+           def_kvs
+             | poly_kinds = def_tvs
+             | otherwise  = DefaultKindVars
+             -- As -XNoPolyKinds precludes polymorphic kind variables, we default them.
+             -- For example:
+             --
+             --   type F :: Type -> Type
+             --   type family F a where
+             --      F (a -> b) = b
+             --
+             -- Here we get `a :: TYPE r`, so to accept this program when -XNoPolyKinds is enabled
+             -- we must default the kind variable `r :: RuntimeRep`.
+             -- Test case: T20584.
+       ; defaulted_kvs <- mapM (defaultTyVar def_kvs) dep_kvs
+       ; defaulted_tvs <- mapM (defaultTyVar def_tvs) 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) }
@@ -2029,7 +2049,7 @@ doNotQuantifyTyVars dvs where_found
 
   | otherwise
   = do { traceTc "doNotQuantifyTyVars" (ppr dvs)
-       ; undefaulted <- defaultTyVars allVarsOfKindDefault dvs
+       ; undefaulted <- defaultTyVars DefaultNonStandardTyVars 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 8717d30a4b..bd4c82eb0c 100644
--- a/compiler/GHC/Types/Basic.hs
+++ b/compiler/GHC/Types/Basic.hs
@@ -101,8 +101,8 @@ module GHC.Types.Basic (
 
         TypeOrKind(..), isTypeLevel, isKindLevel,
 
-        DefaultKindVars(..), DefaultVarsOfKind(..),
-        allVarsOfKindDefault, noVarsOfKindDefault,
+        NonStandardDefaultingStrategy(..),
+        DefaultingStrategy(..), defaultNonStandardTyVars,
 
         ForeignSrcLang (..)
    ) where
@@ -1755,53 +1755,125 @@ isKindLevel KindLevel = True
 *                                                                      *
 ********************************************************************* -}
 
--- | Whether to default kind variables. Usually: no, unless `-XNoPolyKinds`
--- is enabled.
-data DefaultKindVars
-  = Don'tDefaultKinds
-  | DefaultKinds
+{- Note [Type variable defaulting options]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is an overview of the current type variable defaulting mechanisms,
+in the order in which they happen.
 
-instance Outputable DefaultKindVars where
-  ppr Don'tDefaultKinds = text "Don'tDefaultKinds"
-  ppr DefaultKinds = text "DefaultKinds"
+GHC.Tc.Utils.TcMType.defaultTyVar
 
--- | 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
-    }
+  This is a built-in defaulting mechanism for the following type variables:
+
+    (1) kind variables with -XNoPolyKinds,
+    (2) type variables of kind 'RuntimeRep' default to 'LiftedRep',
+        of kind 'Levity' to 'Lifted', and of kind 'Multiplicity' to 'Many'.
+
+  It is used in many situations:
+
+    - inferring a type (e.g. a declaration with no type signature or a
+      partial type signature), in 'GHC.Tc.Solver.simplifyInfer',
+    - simplifying top-level constraints in 'GHC.Tc.Solver.simplifyTop',
+    - kind checking a CUSK in 'GHC.Tc.Gen.kcCheckDeclHeader_cusk',
+    - 'GHC.Tc.TyCl.generaliseTcTyCon',
+    - type checking type family and data family instances,
+      in 'GHC.Tc.TyCl.tcTyFamInstEqnGuts' and 'GHC.Tc.TyCl.Instance.tcDataFamInstHeader'
+      respectively,
+    - type-checking rules in 'GHC.Tc.Gen.tcRule',
+    - kind generalisation in 'GHC.Tc.Gen.HsType.kindGeneralizeSome'
+      and 'GHC.Tc.Gen.HsType.kindGeneralizeAll'.
+
+  Different situations call for a different defaulting strategy,
+  so 'defaultTyVar' takes a strategy parameter which determines which
+  type variables to default.
+  Currently, this strategy is set as follows:
+
+    - Kind variables:
+      - with -XNoPolyKinds, these must be defaulted. This includes kind variables
+        of kind 'RuntimeRep', 'Levity' and 'Multiplicity'.
+        Test case: T20584.
+      - with -XPolyKinds, behave as if they were type variables (see below).
+    - Type variables of kind 'RuntimeRep', 'Levity' or 'Multiplicity'
+      - in type and data families instances, these are not defaulted.
+        Test case: T17536.
+      - otherwise: default variables of these three kinds. This ensures
+        that in a program such as
+
+          foo :: forall a. a -> a
+          foo x = x
+
+        we continue to infer `a :: Type`.
+
+  Note that the strategy is set in two steps: callers of 'defaultTyVars' only
+  specify whether to default type variables of "non-standard" kinds
+  (that is, of kinds 'RuntimeRep'/'Levity'/'Multiplicity'). Then 'defaultTyVars'
+  determines which variables are type variables and which are kind variables,
+  and if the user has asked for -XNoPolyKinds we default the kind variables.
+
+GHC.Tc.Solver.defaultTyVarTcS
+
+  This is a built-in defaulting mechanism that happens after
+  the constraint solver has run, in 'GHC.Tc.Solver.simplifyTopWanteds'.
+
+  It only defaults type (and kind) variables of kind 'RuntimeRep',
+  'Levity', 'Multiplicity'.
+
+  It is not configurable, neither by options nor by the user.
+
+GHC.Tc.Solver.applyDefaultingRules
+
+  This is typeclass defaulting, and includes defaulting plugins.
+  It happens right after 'defaultTyVarTcS' in 'GHC.Tc.Solver.simplifyTopWanteds'.
+  It is user configurable, using default declarations (/plugins).
+
+GHC.Iface.Type.defaultIfaceTyVarsOfKind
+
+  This is a built-in defaulting mechanism that only applies when pretty-printing.
+  It defaults 'RuntimeRep'/'Levity' variables unless -fprint-explicit-kinds is enabled,
+  and 'Multiplicity' variables unless -XLinearTypes is enabled.
+
+-}
+
+-- | Specify whether to default type variables of kind 'RuntimeRep'/'Levity'/'Multiplicity'.
+data NonStandardDefaultingStrategy
+  -- | Default type variables of the given kinds:
+  --
+  --   - default 'RuntimeRep' variables to 'LiftedRep'
+  --   - default 'Levity' variables to 'Lifted'
+  --   - default 'Multiplicity' variables to 'Many'
+  = DefaultNonStandardTyVars
+  -- | Try not to default type variables of the kinds 'RuntimeRep'/'Levity'/'Multiplicity'.
+  --
+  -- Note that these might get defaulted anyway, if they are kind variables
+  -- and `-XNoPolyKinds` is enabled.
+  | TryNotToDefaultNonStandardTyVars
+
+-- | Specify whether to default kind variables, and type variables
+-- of kind 'RuntimeRep'/'Levity'/'Multiplicity'.
+data DefaultingStrategy
+  -- | Default kind variables:
+  --
+  --   - default kind variables of kind 'Type' to 'Type',
+  --   - default 'RuntimeRep'/'Levity'/'Multiplicity' kind variables
+  --     to 'LiftedRep'/'Lifted'/'Many', respectively.
+  --
+  -- When this strategy is used, it means that we have determined that
+  -- the variables we are considering defaulting are all kind variables.
+  --
+  -- Usually, we pass this option when -XNoPolyKinds is enabled.
+  = DefaultKindVars
+  -- | Default (or don't default) non-standard variables, of kinds
+  -- 'RuntimeRep', 'Levity' and 'Multiplicity'.
+  | NonStandardDefaulting NonStandardDefaultingStrategy
+
+defaultNonStandardTyVars :: DefaultingStrategy -> Bool
+defaultNonStandardTyVars DefaultKindVars                                          = True
+defaultNonStandardTyVars (NonStandardDefaulting DefaultNonStandardTyVars)         = True
+defaultNonStandardTyVars (NonStandardDefaulting TryNotToDefaultNonStandardTyVars) = False
+
+instance Outputable NonStandardDefaultingStrategy where
+  ppr DefaultNonStandardTyVars         = text "DefaultOnlyNonStandardTyVars"
+  ppr TryNotToDefaultNonStandardTyVars = text "TryNotToDefaultNonStandardTyVars"
+
+instance Outputable DefaultingStrategy where
+  ppr DefaultKindVars            = text "DefaultKindVars"
+  ppr (NonStandardDefaulting ns) = text "NonStandardDefaulting" <+> ppr ns
diff --git a/compiler/MachDeps.h b/compiler/MachDeps.h
new file mode 100644
index 0000000000..98a90814d9
--- /dev/null
+++ b/compiler/MachDeps.h
@@ -0,0 +1,119 @@
+/* -----------------------------------------------------------------------------
+ *
+ * (c) The University of Glasgow 2002
+ *
+ * Definitions that characterise machine specific properties of basic
+ * types (C & Haskell) of a target platform.
+ *
+ * NB: Keep in sync with HsFFI.h and StgTypes.h.
+ * NB: THIS FILE IS INCLUDED IN HASKELL SOURCE!
+ *
+ * To understand the structure of the RTS headers, see the wiki:
+ *   https://gitlab.haskell.org/ghc/ghc/wikis/commentary/source-tree/includes
+ *
+ * ---------------------------------------------------------------------------*/
+
+#pragma once
+
+/* Don't allow stage1 (cross-)compiler embed assumptions about target
+ * platform. When ghc-stage1 is being built by ghc-stage0 is should not
+ * refer to target defines. A few past examples:
+ *  - https://gitlab.haskell.org/ghc/ghc/issues/13491
+ *  - https://phabricator.haskell.org/D3122
+ *  - https://phabricator.haskell.org/D3405
+ *
+ * In those cases code change assumed target defines like SIZEOF_HSINT
+ * are applied to host platform, not target platform.
+ *
+ * So what should be used instead in GHC_STAGE=1?
+ *
+ * To get host's equivalent of SIZEOF_HSINT you can use Bits instances:
+ *    Data.Bits.finiteBitSize (0 :: Int)
+ *
+ * To get target's values it is preferred to use runtime target
+ * configuration from 'targetPlatform :: DynFlags -> Platform'
+ * record.
+ *
+ * Hence we hide these macros from GHC_STAGE=1
+ */
+
+/* Sizes of C types come from here... */
+#include "ghcautoconf.h"
+
+/* Sizes of Haskell types follow.  These sizes correspond to:
+ *   - the number of bytes in the primitive type (eg. Int#)
+ *   - the number of bytes in the external representation (eg. HsInt)
+ *   - the scale offset used by writeFooOffAddr#
+ *
+ * In the heap, the type may take up more space: eg. SIZEOF_INT8 == 1,
+ * but it takes up SIZEOF_HSWORD (4 or 8) bytes in the heap.
+ */
+
+#define SIZEOF_HSCHAR           SIZEOF_WORD32
+#define ALIGNMENT_HSCHAR        ALIGNMENT_WORD32
+
+#define SIZEOF_HSINT            SIZEOF_VOID_P
+#define ALIGNMENT_HSINT         ALIGNMENT_VOID_P
+
+#define SIZEOF_HSWORD           SIZEOF_VOID_P
+#define ALIGNMENT_HSWORD        ALIGNMENT_VOID_P
+
+#define SIZEOF_HSDOUBLE         SIZEOF_DOUBLE
+#define ALIGNMENT_HSDOUBLE      ALIGNMENT_DOUBLE
+
+#define SIZEOF_HSFLOAT          SIZEOF_FLOAT
+#define ALIGNMENT_HSFLOAT       ALIGNMENT_FLOAT
+
+#define SIZEOF_HSPTR            SIZEOF_VOID_P
+#define ALIGNMENT_HSPTR         ALIGNMENT_VOID_P
+
+#define SIZEOF_HSFUNPTR         SIZEOF_VOID_P
+#define ALIGNMENT_HSFUNPTR      ALIGNMENT_VOID_P
+
+#define SIZEOF_HSSTABLEPTR      SIZEOF_VOID_P
+#define ALIGNMENT_HSSTABLEPTR   ALIGNMENT_VOID_P
+
+#define SIZEOF_INT8             SIZEOF_INT8_T
+#define ALIGNMENT_INT8          ALIGNMENT_INT8_T
+
+#define SIZEOF_WORD8            SIZEOF_UINT8_T
+#define ALIGNMENT_WORD8         ALIGNMENT_UINT8_T
+
+#define SIZEOF_INT16            SIZEOF_INT16_T
+#define ALIGNMENT_INT16         ALIGNMENT_INT16_T
+
+#define SIZEOF_WORD16           SIZEOF_UINT16_T
+#define ALIGNMENT_WORD16        ALIGNMENT_UINT16_T
+
+#define SIZEOF_INT32            SIZEOF_INT32_T
+#define ALIGNMENT_INT32         ALIGNMENT_INT32_T
+
+#define SIZEOF_WORD32           SIZEOF_UINT32_T
+#define ALIGNMENT_WORD32        ALIGNMENT_UINT32_T
+
+#define SIZEOF_INT64            SIZEOF_INT64_T
+#define ALIGNMENT_INT64         ALIGNMENT_INT64_T
+
+#define SIZEOF_WORD64           SIZEOF_UINT64_T
+#define ALIGNMENT_WORD64        ALIGNMENT_UINT64_T
+
+#if !defined(WORD_SIZE_IN_BITS)
+#if SIZEOF_HSWORD == 4
+#define WORD_SIZE_IN_BITS       32
+#define WORD_SIZE_IN_BITS_FLOAT 32.0
+#else
+#define WORD_SIZE_IN_BITS       64
+#define WORD_SIZE_IN_BITS_FLOAT 64.0
+#endif
+#endif
+
+#if !defined(TAG_BITS)
+#if SIZEOF_HSWORD == 4
+#define TAG_BITS                2
+#else
+#define TAG_BITS                3
+#endif
+#endif
+
+#define TAG_MASK ((1 << TAG_BITS) - 1)
+
diff --git a/testsuite/tests/indexed-types/should_compile/T17536.hs b/testsuite/tests/indexed-types/should_compile/T17536.hs
index b007dfecfe..7ae2ba9904 100644
--- a/testsuite/tests/indexed-types/should_compile/T17536.hs
+++ b/testsuite/tests/indexed-types/should_compile/T17536.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE NoPolyKinds #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 
diff --git a/testsuite/tests/indexed-types/should_compile/T17536c.hs b/testsuite/tests/indexed-types/should_compile/T17536c.hs
new file mode 100644
index 0000000000..860a2c357a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17536c.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+
+module T17536c where
+
+import Data.Kind
+import GHC.Exts
+
+type R :: forall (r :: RuntimeRep) -> TYPE r -> Type
+type family R r a where
+  R _ _ = Int
+
+r :: R FloatRep Float# -> Int
+r x = x
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 9e0558cf5b..d03de782c6 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -295,6 +295,7 @@ test('T17008b', normal, compile, [''])
 test('T17056', normal, compile, [''])
 test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
 test('T17536', normal, compile, [''])
+test('T17536c', normal, compile, [''])
 test('T17923', normal, compile, [''])
 test('T18065', normal, compile, ['-O'])
 test('T18809', normal, compile, ['-O'])
diff --git a/testsuite/tests/typecheck/should_compile/T20584.hs b/testsuite/tests/typecheck/should_compile/T20584.hs
new file mode 100644
index 0000000000..2d72a3ad41
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20584.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE NoPolyKinds #-}
+
+module T20584 where
+
+data Decision_Wrap
+data Decision_Map
+
+type family DecideFn p where
+  DecideFn (r -> p) = Decision_Map
+  DecideFn p = Decision_Wrap
diff --git a/testsuite/tests/typecheck/should_compile/T20584b.hs b/testsuite/tests/typecheck/should_compile/T20584b.hs
new file mode 100644
index 0000000000..a3e3287265
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20584b.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module T20584b where
+
+import Text.Printf ( printf )
+
+secs :: Double -> String
+secs k
+    | k < 0      = '-' : secs (-k)
+    | k >= 1     = k        `with` "s"
+    | k >= 1e-3  = (k*1e3)  `with` "ms"
+    | k >= 1e-6  = (k*1e6)  `with` "μs"
+    | k >= 1e-9  = (k*1e9)  `with` "ns"
+    | k >= 1e-12 = (k*1e12) `with` "ps"
+    | k >= 1e-15 = (k*1e15) `with` "fs"
+    | k >= 1e-18 = (k*1e18) `with` "as"
+    | otherwise  = printf "%g s" k
+     where with (t :: Double) (u :: String)
+               | t >= 1e9  = printf "%.4g %s" t u
+               | t >= 1e3  = printf "%.0f %s" t u
+               | t >= 1e2  = printf "%.1f %s" t u
+               | t >= 1e1  = printf "%.2f %s" t u
+               | otherwise = printf "%.3f %s" t u
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a2bb10ba02..9aad00f982 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -806,3 +806,5 @@ test('T20241', normal, compile, [''])
 test('T20187a', normal, compile, ['-Wredundant-strictness-flags'])
 test('T20187b', normal, compile, ['-Wredundant-strictness-flags'])
 test('T20356', normal, compile, [''])
+test('T20584', normal, compile, [''])
+test('T20584b', normal, compile, [''])