Stop inferring over-polymorphic kinds

Before this patch GHC was trying to be too clever
(Trac #16344); it succeeded in kind-checking this
polymorphic-recursive declaration

    data T ka (a::ka) b
      = MkT (T Type           Int   Bool)
            (T (Type -> Type) Maybe Bool)

As Note [No polymorphic recursion] discusses, the "solution" was
horribly fragile.  So this patch deletes the key lines in
TcHsType, and a wodge of supporting stuff in the renamer.

There were two regressions, both the same: a closed type family
decl like this (T12785b) does not have a CUSK:
  type family Payload (n :: Peano) (s :: HTree n x) where
    Payload Z (Point a) = a
    Payload (S n) (a `Branch` stru) = a

To kind-check the equations we need a dependent kind for
Payload, and we don't get that any more.  Solution: make it
a CUSK by giving the result kind -- probably a good thing anyway.

The other case (T12442) was very similar: a close type family
declaration without a CUSK.

20 files changed, 145 insertions, 147 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 67a05d647d..2aaafad29f 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -43,7 +43,6 @@ import Id
 import Name hiding( isVarOcc, isTcOcc, varName, tcName )
 import THNames
 import NameEnv
-import NameSet
 import TcType
 import TyCon
 import TysWiredIn
@@ -392,9 +391,7 @@ repFamilyDecl decl@(dL->L loc (FamilyDecl { fdInfo      = info
                                           , fdInjectivityAnn = injectivity }))
   = do { tc1 <- lookupLOcc tc           -- See note [Binders and occurrences]
        ; let mkHsQTvs :: [LHsTyVarBndr GhcRn] -> LHsQTyVars GhcRn
-             mkHsQTvs tvs = HsQTvs { hsq_ext = HsQTvsRn
-                                                { hsq_implicit = []
-                                                , hsq_dependent = emptyNameSet }
+             mkHsQTvs tvs = HsQTvs { hsq_ext = []
                                    , hsq_explicit = tvs }
              resTyVar = case resultSig of
                      TyVarSig _ bndr -> mkHsQTvs [bndr]
@@ -569,9 +566,7 @@ repTyFamEqn (HsIB { hsib_ext = var_names
                                        , feqn_fixity = fixity
                                        , feqn_rhs  = rhs }})
   = do { tc <- lookupLOcc tc_name     -- See note [Binders and occurrences]
-       ; let hs_tvs = HsQTvs { hsq_ext = HsQTvsRn
-                               { hsq_implicit = var_names
-                               , hsq_dependent = emptyNameSet }   -- Yuk
+       ; let hs_tvs = HsQTvs { hsq_ext = var_names
                              , hsq_explicit = fromMaybe [] mb_bndrs }
        ; addTyClTyVarBinds hs_tvs $ \ _ ->
          do { mb_bndrs1 <- repMaybeList tyVarBndrQTyConName
@@ -610,9 +605,7 @@ repDataFamInstD (DataFamInstDecl { dfid_eqn =
                                              , feqn_fixity = fixity
                                              , feqn_rhs   = defn }})})
   = do { tc <- lookupLOcc tc_name         -- See note [Binders and occurrences]
-       ; let hs_tvs = HsQTvs { hsq_ext = HsQTvsRn
-                                 { hsq_implicit = var_names
-                                 , hsq_dependent = emptyNameSet }   -- Yuk
+       ; let hs_tvs = HsQTvs { hsq_ext = var_names
                              , hsq_explicit = fromMaybe [] mb_bndrs }
        ; addTyClTyVarBinds hs_tvs $ \ _ ->
          do { mb_bndrs1 <- repMaybeList tyVarBndrQTyConName
@@ -1052,7 +1045,7 @@ addTyVarBinds :: LHsQTyVars GhcRn                    -- the binders to be added
 -- gensym a list of type variables and enter them into the meta environment;
 -- the computations passed as the second argument is executed in that extended
 -- meta environment and gets the *new* names on Core-level as an argument
-addTyVarBinds (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_tvs}
+addTyVarBinds (HsQTvs { hsq_ext = imp_tvs
                       , hsq_explicit = exp_tvs })
               thing_inside
   = addSimpleTyVarBinds imp_tvs $
diff --git a/compiler/hieFile/HieAst.hs b/compiler/hieFile/HieAst.hs
index 2b112153bd..2ab2acbe3f 100644
--- a/compiler/hieFile/HieAst.hs
+++ b/compiler/hieFile/HieAst.hs
@@ -1474,7 +1474,7 @@ instance ToHie (TVScoped (LHsTyVarBndr GhcRn)) where
       XTyVarBndr _ -> []
 
 instance ToHie (TScoped (LHsQTyVars GhcRn)) where
-  toHie (TS sc (HsQTvs (HsQTvsRn implicits _) vars)) = concatM $
+  toHie (TS sc (HsQTvs implicits vars)) = concatM $
     [ pure $ bindingsOnly bindings
     , toHie $ tvScopes sc NoScope vars
     ]
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index 85715a9282..ba961b53d0 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -20,7 +20,7 @@ HsTypes: Abstract syntax: user-defined types
 module HsTypes (
         HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind,
         HsTyVarBndr(..), LHsTyVarBndr, ForallVisFlag(..),
-        LHsQTyVars(..), HsQTvsRn(..),
+        LHsQTyVars(..),
         HsImplicitBndrs(..),
         HsWildCardBndrs(..),
         LHsSigType, LHsSigWcType, LHsWcType,
@@ -79,7 +79,6 @@ import HsLit () -- for instances
 import Id ( Id )
 import Name( Name )
 import RdrName ( RdrName )
-import NameSet ( NameSet, emptyNameSet )
 import DataCon( HsSrcBang(..), HsImplBang(..),
                 SrcStrictness(..), SrcUnpackedness(..) )
 import TysPrim( funTyConName )
@@ -322,21 +321,13 @@ data LHsQTyVars pass   -- See Note [HsType binders]
     }
   | XLHsQTyVars (XXLHsQTyVars pass)
 
-data HsQTvsRn
-  = HsQTvsRn
-           { hsq_implicit :: [Name]
-                -- Implicit (dependent) variables
+type HsQTvsRn = [Name]  -- Implicit variables
+  -- For example, in   data T (a :: k1 -> k2) = ...
+  -- the 'a' is explicit while 'k1', 'k2' are implicit
 
-           , hsq_dependent :: NameSet
-               -- Which members of hsq_explicit are dependent; that is,
-               -- mentioned in the kind of a later hsq_explicit,
-               -- or mentioned in a kind in the scope of this HsQTvs
-               -- See Note [Dependent LHsQTyVars] in TcHsType
-           } deriving Data
-
-type instance XHsQTvs       GhcPs = NoExt
-type instance XHsQTvs       GhcRn = HsQTvsRn
-type instance XHsQTvs       GhcTc = HsQTvsRn
+type instance XHsQTvs GhcPs = NoExt
+type instance XHsQTvs GhcRn = HsQTvsRn
+type instance XHsQTvs GhcTc = HsQTvsRn
 
 type instance XXLHsQTyVars  (GhcPass _) = NoExt
 
@@ -347,11 +338,12 @@ hsQTvExplicit :: LHsQTyVars pass -> [LHsTyVarBndr pass]
 hsQTvExplicit = hsq_explicit
 
 emptyLHsQTvs :: LHsQTyVars GhcRn
-emptyLHsQTvs = HsQTvs (HsQTvsRn [] emptyNameSet) []
+emptyLHsQTvs = HsQTvs { hsq_ext = [], hsq_explicit = [] }
 
 isEmptyLHsQTvs :: LHsQTyVars GhcRn -> Bool
-isEmptyLHsQTvs (HsQTvs (HsQTvsRn [] _) []) = True
-isEmptyLHsQTvs _                = False
+isEmptyLHsQTvs (HsQTvs { hsq_ext = imp, hsq_explicit = exp })
+  = null imp && null exp
+isEmptyLHsQTvs _ = False
 
 ------------------------------------------------
 --            HsImplicitBndrs
@@ -997,7 +989,7 @@ hsExplicitLTyVarNames qtvs = map hsLTyVarName (hsQTvExplicit qtvs)
 
 hsAllLTyVarNames :: LHsQTyVars GhcRn -> [Name]
 -- All variables
-hsAllLTyVarNames (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kvs }
+hsAllLTyVarNames (HsQTvs { hsq_ext = kvs
                          , hsq_explicit = tvs })
   = kvs ++ hsLTyVarNames tvs
 hsAllLTyVarNames (XLHsQTyVars _) = panic "hsAllLTyVarNames"
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index f902b0ef07..19f0d315d2 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -2166,9 +2166,7 @@ rnConDecl decl@(ConDeclGADT { con_names   = names
                                       -- See Note [GADT abstract syntax] in HsDecls
                                       (PrefixCon arg_tys, final_res_ty)
 
-              new_qtvs =  HsQTvs { hsq_ext = HsQTvsRn
-                                     { hsq_implicit  = implicit_tkvs
-                                     , hsq_dependent = emptyNameSet }
+              new_qtvs =  HsQTvs { hsq_ext = implicit_tkvs
                                  , hsq_explicit  = explicit_tkvs }
 
         ; traceRn "rnConDecl2" (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index b84bbe3bae..53bcadee2a 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -822,11 +822,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
                                  -- body kvs, as mandated by
                                  -- Note [Ordering of implicit variables]
              implicit_kvs = filter_occs bndrs kv_occs
-             -- dep_bndrs is the subset of bndrs that are dependent
-             --   i.e. appear in bndr/body_kv_occs
-             -- Can't use implicit_kvs because we've deleted bndrs from that!
-             dep_bndrs = filter (`elemRdr` kv_occs) bndrs
-             del       = deleteBys eqLocated
+             del          = deleteBys eqLocated
              all_bound_on_lhs = null ((body_kv_occs `del` bndrs) `del` bndr_kv_occs)
 
        ; traceRn "checkMixedVars3" $
@@ -841,10 +837,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
        ; bindLocalNamesFV implicit_kv_nms                     $
          bindLHsTyVarBndrs doc mb_in_doc mb_assoc hs_tv_bndrs $ \ rn_bndrs ->
     do { traceRn "bindHsQTyVars" (ppr hsq_bndrs $$ ppr implicit_kv_nms $$ ppr rn_bndrs)
-       ; dep_bndr_nms <- mapM (lookupLocalOccRn . unLoc) dep_bndrs
-       ; thing_inside (HsQTvs { hsq_ext = HsQTvsRn
-                                   { hsq_implicit  = implicit_kv_nms
-                                   , hsq_dependent = mkNameSet dep_bndr_nms }
+       ; thing_inside (HsQTvs { hsq_ext = implicit_kv_nms
                               , hsq_explicit  = rn_bndrs })
                       all_bound_on_lhs } }
 
@@ -879,9 +872,6 @@ Then:
 
 * We want to quantify add implicit bindings for implicit_kvs
 
-* The "dependent" bndrs (hsq_dependent) are the subset of
-  bndrs that are free in bndr_kv_occs or body_kv_occs
-
 * If implicit_body_kvs is non-empty, then there is a kind variable
   mentioned in the kind signature that is not bound "on the left".
   That's one of the rules for a CUSK, so we pass that info on
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index b3c40274c4..0357c1046d 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -91,7 +91,7 @@ import ConLike
 import DataCon
 import Class
 import Name
-import NameSet
+-- import NameSet
 import VarEnv
 import TysWiredIn
 import BasicTypes
@@ -1611,48 +1611,6 @@ addTypeCtxt (L _ ty) thing
 %*                                                                      *
 %************************************************************************
 
-Note [Dependent LHsQTyVars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We track (in the renamer) which explicitly bound variables in a
-LHsQTyVars are manifestly dependent; only precisely these variables
-may be used within the LHsQTyVars. We must do this so that kcLHsQTyVars
-can produce the right TyConBinders, and tell Anon vs. Required.
-
-Example   data T k1 (a:k1) (b:k2) c
-               = MkT (Proxy a) (Proxy b) (Proxy c)
-
-Here
-  (a:k1),(b:k2),(c:k3)
-       are Anon     (explicitly specified as a binder, not used
-                     in the kind of any other binder
-  k1   is Required  (explicitly specifed as a binder, but used
-                     in the kind of another binder i.e. dependently)
-  k2   is Specified (not explicitly bound, but used in the kind
-                     of another binder)
-  k3   in Inferred  (not lexically in scope at all, but inferred
-                     by kind inference)
-and
-  T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> *
-
-See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
-in TyCoRep.
-
-kcLHsQTyVars uses the hsq_dependent field to decide whether
-k1, a, b, c should be Required or Anon.
-
-Earlier, thought it would work simply to do a free-variable check
-during kcLHsQTyVars, but this is bogus, because there may be
-unsolved equalities about. And we don't want to eagerly solve the
-equalities, because we may get further information after
-kcLHsQTyVars is called.  (Recall that kcLHsQTyVars is called
-only from getInitialKind.)
-This is what implements the rule that all variables intended to be
-dependent must be manifestly so.
-
-Sidenote: It's quite possible that later, we'll consider (t -> s)
-as a degenerate case of some (pi (x :: t) -> s) and then this will
-all get more permissive.
-
 Note [Keeping scoped variables in order: Explicit]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When the user writes `forall a b c. blah`, we bring a, b, and c into
@@ -1822,8 +1780,7 @@ kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk
 
 ------------------------------
 kcLHsQTyVars_Cusk name flav
-              (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
-                                           , hsq_dependent = dep_names }
+              (HsQTvs { hsq_ext = kv_ns
                       , hsq_explicit = hs_tvs }) thing_inside
   -- CUSK case
   -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
@@ -1874,7 +1831,6 @@ kcLHsQTyVars_Cusk name flav
          vcat [ text "name" <+> ppr name
               , text "kv_ns" <+> ppr kv_ns
               , text "hs_tvs" <+> ppr hs_tvs
-              , text "dep_names" <+> ppr dep_names
               , text "scoped_kvs" <+> ppr scoped_kvs
               , text "tc_tvs" <+> ppr tc_tvs
               , text "res_kind" <+> ppr res_kind
@@ -1895,8 +1851,7 @@ kcLHsQTyVars_Cusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
 
 ------------------------------
 kcLHsQTyVars_NonCusk name flav
-              (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
-                                           , hsq_dependent = dep_names }
+              (HsQTvs { hsq_ext = kv_ns
                       , hsq_explicit = hs_tvs }) thing_inside
   -- Non_CUSK case
   -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
@@ -1913,22 +1868,26 @@ kcLHsQTyVars_NonCusk name flav
                -- might unify with kind vars in other types in a mutually
                -- recursive group.
                -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
-             tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
+
+             tc_binders = mkAnonTyConBinders VisArg tc_tvs
                -- Also, note that tc_binders has the tyvars from only the
                -- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
                -- in TcTyClsDecls
+               --
+               -- mkAnonTyConBinder: see Note [No polymorphic recursion]
 
              all_tv_prs = (kv_ns                `zip` scoped_kvs) ++
                           (hsLTyVarNames hs_tvs `zip` tc_tvs)
                -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification
                --     variables, hence the need to zip here.  Ditto bindExplicit..
                -- See TcMType Note [Unification variables need fresh Names]
+
              tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
                                False -- not yet generalised
                                flav
 
        ; traceTc "kcLHsQTyVars: not-cusk" $
-         vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
+         vcat [ ppr name, ppr kv_ns, ppr hs_tvs
               , ppr scoped_kvs
               , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
        ; return tycon }
@@ -1936,18 +1895,57 @@ kcLHsQTyVars_NonCusk name flav
     ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
               | otherwise            = AnyKind
 
-    mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
-    -- See Note [Dependent LHsQTyVars]
-    mk_tc_binder hs_tv tv
-       | hsLTyVarName hs_tv `elemNameSet` dep_names
-       = mkNamedTyConBinder Required tv
-       | otherwise
-       = mkAnonTyConBinder VisArg tv
-
 kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
 
 
-{- Note [Kind-checking tyvar binders for associated types]
+{- Note [No polymorphic recursion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Should this kind-check?
+  data T ka (a::ka) b  = MkT (T Type           Int   Bool)
+                             (T (Type -> Type) Maybe Bool)
+
+Notice that T is used at two different kinds in its RHS.  No!
+This should not kind-check.  Polymorphic recursion is known to
+be a tough nut.
+
+Previously, we laboriously (with help from the renamer)
+tried to give T the polymoprhic kind
+   T :: forall ka -> ka -> kappa -> Type
+where kappa is a unification variable, even in the getInitialKinds
+phase (which is what kcLHsQTyVars_NonCusk is all about).  But
+that is dangerously fragile (see the ticket).
+
+Solution: make kcLHsQTyVars_NonCusk give T a straightforward
+monomorphic kind, with no quantification whatsoever. That's why
+we use mkAnonTyConBinder for all arguments when figuring out
+tc_binders.
+
+But notice that (Trac #16322 comment:3)
+
+* The algorithm successfully kind-checks this declaration:
+    data T2 ka (a::ka) = MkT2 (T2 Type a)
+
+  Starting with (getInitialKinds)
+    T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> *
+  we get
+    kappa4 := kappa1   -- from the (a:ka) kind signature
+    kappa1 := Type     -- From application T2 Type
+
+  These constraints are soluble so generaliseTcTyCon gives
+    T2 :: forall (k::Type) -> k -> *
+
+  But now the /typechecking/ (aka desugaring, tcTyClDecl) phase
+  fails, because the call (T2 Type a) in the RHS is ill-kinded.
+
+  We'd really prefer all errors to show up in the kind checking
+  phase.
+
+* This algorithm still accepts (in all phases)
+     data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
+  although T3 is really polymorphic-recursive too.
+  Perhaps we should somehow reject that.
+
+Note [Kind-checking tyvar binders for associated types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When kind-checking the type-variable binders for associated
    data/newtype decls
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 8d413139ba..2c9a672e8e 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1154,7 +1154,7 @@ kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
 kcConDecl (ConDeclGADT { con_names = names
                        , con_qvars = qtvs, con_mb_cxt = cxt
                        , con_args = args, con_res_ty = res_ty })
-  | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
+  | HsQTvs { hsq_ext = implicit_tkv_nms
            , hsq_explicit = explicit_tkv_nms } <- qtvs
   = -- Even though the data constructor's type is closed, we
     -- must still kind-check the type, because that may influence
@@ -1492,7 +1492,7 @@ tcDefaultAssocDecl _ (d1:_:_)
 tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
                                              , feqn_pats = hs_tvs
                                              , feqn_rhs = hs_rhs_ty })]
-  | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars}
+  | HsQTvs { hsq_ext = imp_vars
            , hsq_explicit = exp_vars } <- hs_tvs
   = -- See Note [Type-checking default assoc decls]
     setSrcSpan loc $
@@ -2281,7 +2281,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
                        , con_qvars = qtvs
                        , con_mb_cxt = cxt, con_args = hs_args
                        , con_res_ty = hs_res_ty })
-  | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
+  | HsQTvs { hsq_ext = implicit_tkv_nms
            , hsq_explicit = explicit_tkv_nms } <- qtvs
   = addErrCtxt (dataConCtxtName names) $
     do { traceTc "tcConDecl 1 gadt" (ppr names)
diff --git a/testsuite/tests/dependent/should_compile/T12442.hs b/testsuite/tests/dependent/should_compile/T12442.hs
index c76dfb962e..b4bcdb9d62 100644
--- a/testsuite/tests/dependent/should_compile/T12442.hs
+++ b/testsuite/tests/dependent/should_compile/T12442.hs
@@ -33,7 +33,8 @@ data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
 data instance Sing (elem :: EffElem x a xs) where
   SHere :: Sing Here
 
-type family UpdateResTy b t (xs :: [EFFECT]) (elem :: EffElem e a xs)
+type family UpdateResTy (b :: Type) (t :: Type)
+                        (xs :: [EFFECT]) (elem :: EffElem e a xs)
                         (thing :: e @@ a @@ b @@ t) :: [EFFECT] where
   UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
 
diff --git a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
index 109b18e9f7..789798b370 100644
--- a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
+++ b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
@@ -20,7 +20,9 @@ type DComp a
            (x :: a) =
   f (g x)
 
-type family ElimList a
+-- Ensure that ElimList has a CUSK, beuas it is
+-- is used polymorphically its RHS (c.f. Trac #16344)
+type family ElimList (a :: Type)
                      (p :: [a] -> Type)
                      (s :: [a])
                      (pNil :: p '[])
diff --git a/testsuite/tests/dependent/should_compile/T16344b.hs b/testsuite/tests/dependent/should_compile/T16344b.hs
new file mode 100644
index 0000000000..1f6fa8a00e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T16344b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeInType, GADTs, KindSignatures #-}
+
+module T16344 where
+
+import Data.Kind
+
+-- This one is accepted, even though it is polymorphic-recursive.
+-- See Note [No polymorphic recursion] in TcHsType
+
+data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 4ba649ac9d..4e162aed69 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -68,3 +68,5 @@ test('T14729kind', normal, ghci_script, ['T14729kind.script'])
 test('T16326_Compile1', normal, compile, [''])
 test('T16326_Compile2', normal, compile, [''])
 test('T16391a', normal, compile, [''])
+test('T16344b', normal, compile, [''])
+
diff --git a/testsuite/tests/dependent/should_fail/T16344.hs b/testsuite/tests/dependent/should_fail/T16344.hs
new file mode 100644
index 0000000000..0cf4b98642
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType, KindSignatures #-}
+
+module T16344 where
+
+import Data.Kind
+
+data T ka (a::ka) b  = MkT (T Type           Int   Bool)
+                           (T (Type -> Type) Maybe Bool)
diff --git a/testsuite/tests/dependent/should_fail/T16344.stderr b/testsuite/tests/dependent/should_fail/T16344.stderr
new file mode 100644
index 0000000000..b47561771f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344.stderr
@@ -0,0 +1,6 @@
+
+T16344.hs:7:46: error:
+    • Expected kind ‘ka’, but ‘Int’ has kind ‘*’
+    • In the second argument of ‘T’, namely ‘Int’
+      In the type ‘(T Type Int Bool)’
+      In the definition of data constructor ‘MkT’
diff --git a/testsuite/tests/dependent/should_fail/T16344a.hs b/testsuite/tests/dependent/should_fail/T16344a.hs
new file mode 100644
index 0000000000..cb4d1a7f21
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeInType, KindSignatures #-}
+
+module T16344 where
+
+import Data.Kind
+
+-- This one is rejected, but in the typechecking phase
+-- which is a bit nasty.
+-- See Note [No polymorphic recursion] in TcHsType
+
+data T2 ka (a::ka) = MkT2 (T2 Type a)
diff --git a/testsuite/tests/dependent/should_fail/T16344a.stderr b/testsuite/tests/dependent/should_fail/T16344a.stderr
new file mode 100644
index 0000000000..d838d14e57
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344a.stderr
@@ -0,0 +1,6 @@
+
+T16344a.hs:11:36: error:
+    • Expected a type, but ‘a’ has kind ‘ka’
+    • In the second argument of ‘T2’, namely ‘a’
+      In the type ‘(T2 Type a)’
+      In the definition of data constructor ‘MkT2’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index baaddd7442..1f75a85716 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -53,3 +53,5 @@ test('T16326_Fail10', normal, compile_fail, [''])
 test('T16326_Fail11', normal, compile_fail, [''])
 test('T16326_Fail12', normal, compile_fail, [''])
 test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
+test('T16344', normal, compile_fail, [''])
+test('T16344a', normal, compile_fail, [''])
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index 1bc285ac3b..8dd85edcd6 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -68,10 +68,7 @@
         ({ DumpRenamedAst.hs:9:6-10 }
          {Name: DumpRenamedAst.Peano})
         (HsQTvs
-         (HsQTvsRn
-          []
-          {NameSet:
-           []})
+         []
          [])
         (Prefix)
         (HsDataDefn
@@ -205,10 +202,7 @@
          ({ DumpRenamedAst.hs:11:13-18 }
           {Name: DumpRenamedAst.Length})
          (HsQTvs
-          (HsQTvsRn
-           [{Name: k}]
-           {NameSet:
-            []})
+          [{Name: k}]
           [({ DumpRenamedAst.hs:11:21-29 }
             (KindedTyVar
              (NoExt)
@@ -247,10 +241,7 @@
          ({ DumpRenamedAst.hs:15:13-15 }
           {Name: DumpRenamedAst.Nat})
          (HsQTvs
-          (HsQTvsRn
-           [{Name: k}]
-           {NameSet:
-            []})
+          [{Name: k}]
           [])
          (Prefix)
          ({ DumpRenamedAst.hs:15:17-33 }
@@ -365,11 +356,8 @@
                ({ DumpRenamedAst.hs:19:10-45 }
                 (False))
                (HsQTvs
-                (HsQTvsRn
-                 [{Name: f}
-                 ,{Name: g}]
-                 {NameSet:
-                  []})
+                [{Name: f}
+                ,{Name: g}]
                 [])
                (Nothing)
                (PrefixCon
@@ -457,10 +445,7 @@
         ({ DumpRenamedAst.hs:21:6 }
          {Name: DumpRenamedAst.T})
         (HsQTvs
-         (HsQTvsRn
-          [{Name: k}]
-          {NameSet:
-           []})
+         [{Name: k}]
          [({ DumpRenamedAst.hs:21:8 }
            (UserTyVar
             (NoExt)
@@ -595,10 +580,7 @@
          ({ DumpRenamedAst.hs:23:13-14 }
           {Name: DumpRenamedAst.F1})
          (HsQTvs
-          (HsQTvsRn
-           [{Name: k}]
-           {NameSet:
-            []})
+          [{Name: k}]
           [({ DumpRenamedAst.hs:23:17-22 }
             (KindedTyVar
              (NoExt)
diff --git a/testsuite/tests/parser/should_compile/T14189.stderr b/testsuite/tests/parser/should_compile/T14189.stderr
index e5aff5bf88..dd8df9dc04 100644
--- a/testsuite/tests/parser/should_compile/T14189.stderr
+++ b/testsuite/tests/parser/should_compile/T14189.stderr
@@ -7,25 +7,22 @@
    (NoExt)
    (XValBindsLR
     (NValBinds
-      []
-      []))
+     []
+     []))
    []
    [(TyClGroup
      (NoExt)
      [({ T14189.hs:6:1-42 }
        (DataDecl
         (DataDeclRn
-          (True)
-          {NameSet:
-           [{Name: GHC.Types.Int}]})
+         (True)
+         {NameSet:
+          [{Name: GHC.Types.Int}]})
         ({ T14189.hs:6:6-11 }
          {Name: T14189.MyType})
         (HsQTvs
-         (HsQTvsRn
          []
-         {NameSet:
-          []})
-          [])
+         [])
         (Prefix)
         (HsDataDefn
          (NoExt)
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.hs b/testsuite/tests/typecheck/should_fail/T12785b.hs
index b827372bf0..951b04c6cd 100644
--- a/testsuite/tests/typecheck/should_fail/T12785b.hs
+++ b/testsuite/tests/typecheck/should_fail/T12785b.hs
@@ -13,7 +13,7 @@ data HTree n a where
   Leaf :: HTree (S n) a
   Branch :: a -> HTree n (HTree (S n) a) -> HTree (S n) a
 
-data STree n :: forall a . (a -> Type) -> HTree n a -> Type where
+data STree (n ::Peano) :: forall a . (a -> Type) -> HTree n a -> Type where
   SPoint :: f a -> STree Z f (Point a)
   SLeaf :: STree (S n) f Leaf
   SBranch :: f a -> STree n (STree (S n) f) stru -> STree (S n) f (a `Branch` stru)
@@ -33,6 +33,6 @@ hmap f (Point a) = Point (f a)
 hmap f Leaf = Leaf
 hmap f (a `Branch` tr) = f a `Branch` hmap (hmap f) tr
 
-type family Payload (n :: Peano) (s :: HTree n x) where
+type family Payload (n :: Peano) (s :: HTree n x) :: x where
   Payload Z (Point a) = a
   Payload (S n) (a `Branch` stru) = a
diff --git a/utils/haddock b/utils/haddock
-Subproject e7586f005aa89a45b0fc4f3564f0f17ab9f79d3
+Subproject 65bbdfb6dc1b08f893187e1847985aad4505fcd