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

6 files changed, 53 insertions, 32 deletions

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`