Fix scoping of TyCon binders in TcTyClsDecls

This patch fixes #17566 by refactoring the way we decide the final
identity of the tyvars in the TyCons of a possibly-recursive nest
of type and class decls, possibly with associated types.

It's all laid out in
  Note [Swizzling the tyvars before generaliseTcTyCon]

Main changes:

* We have to generalise each decl (with its associated types)
  all at once: TcTyClsDecls.generaliseTyClDecl

* The main new work is done in TcTyClsDecls.swizzleTcTyConBndrs

* The mysterious TcHsSyn.zonkRecTyVarBndrs dies altogether

Other smaller things:

* A little refactoring, moving bindTyClTyVars from tcTyClDecl1
  to tcDataDefn, tcSynRhs, etc.  Clearer, reduces the number of
  parameters

* Reduce the amount of swizzling required.
  Specifically, bindExplicitTKBndrs_Q_Tv doesn't need
    to clone a new Name for the TyVarTv, and not
    cloning means that in the vasly common case,
    swizzleTyConBndrs is a no-op

  In detail:
    Rename newTyVarTyVar --> cloneTyVarTyVar
    Add newTyVarTyTyVar that doesn't clone
    Use the non-cloning newTyVarTyVar in
       bindExplicitTKBndrs_Q_Tv
       Rename newFlexiKindedTyVarTyVar
           --> cloneFlexiKindedTyVarTyVar

* Define new utility function and use it
     HsDecls.familyDeclName ::
        FamilyDecl (GhcPass p) -> IdP (GhcPass p)

Updates haddock submodule.

18 files changed, 625 insertions, 298 deletions

diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index 827f26b..aeec082 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/compiler/GHC/Hs/Decls.hs
@@ -83,7 +83,7 @@ module GHC.Hs.Decls (
   RoleAnnotDecl(..), LRoleAnnotDecl, roleAnnotDeclName,
   -- ** Injective type families
   FamilyResultSig(..), LFamilyResultSig, InjectivityAnn(..), LInjectivityAnn,
-  resultVariableName,
+  resultVariableName, familyDeclLName, familyDeclName,
 
   -- * Grouping
   HsGroup(..),  emptyRdrGroup, emptyRnGroup, appendGroups, hsGroupInstDecls,
@@ -710,11 +710,14 @@ tyFamInstDeclLName (TyFamInstDecl (HsIB _ (XFamEqn nec)))
 tyFamInstDeclLName (TyFamInstDecl (XHsImplicitBndrs nec))
   = noExtCon nec
 
-tyClDeclLName :: TyClDecl pass -> Located (IdP pass)
-tyClDeclLName (FamDecl { tcdFam = FamilyDecl { fdLName = ln } }) = ln
-tyClDeclLName decl = tcdLName decl
+tyClDeclLName :: TyClDecl (GhcPass p) -> Located (IdP (GhcPass p))
+tyClDeclLName (FamDecl { tcdFam = fd })     = familyDeclLName fd
+tyClDeclLName (SynDecl { tcdLName = ln })   = ln
+tyClDeclLName (DataDecl { tcdLName = ln })  = ln
+tyClDeclLName (ClassDecl { tcdLName = ln }) = ln
+tyClDeclLName (XTyClDecl nec) = noExtCon nec
 
-tcdName :: TyClDecl pass -> IdP pass
+tcdName :: TyClDecl (GhcPass p) -> IdP (GhcPass p)
 tcdName = unLoc . tyClDeclLName
 
 tyClDeclTyVars :: TyClDecl pass -> LHsQTyVars pass
@@ -1140,6 +1143,16 @@ data FamilyInfo pass
      -- said "type family Foo x where .."
   | ClosedTypeFamily (Maybe [LTyFamInstEqn pass])
 
+
+------------- Functions over FamilyDecls -----------
+
+familyDeclLName :: FamilyDecl (GhcPass p) -> Located (IdP (GhcPass p))
+familyDeclLName (FamilyDecl { fdLName = n }) = n
+familyDeclLName (XFamilyDecl nec) = noExtCon nec
+
+familyDeclName :: FamilyDecl (GhcPass p) -> IdP (GhcPass p)
+familyDeclName = unLoc . familyDeclLName
+
 famResultKindSignature :: FamilyResultSig (GhcPass p) -> Maybe (LHsKind (GhcPass p))
 famResultKindSignature (NoSig _) = Nothing
 famResultKindSignature (KindSig _ ki) = Just ki
@@ -1155,6 +1168,8 @@ resultVariableName :: FamilyResultSig (GhcPass a) -> Maybe (IdP (GhcPass a))
 resultVariableName (TyVarSig _ sig) = Just $ hsLTyVarName sig
 resultVariableName _                = Nothing
 
+------------- Pretty printing FamilyDecls -----------
+
 instance OutputableBndrId p
        => Outputable (FamilyDecl (GhcPass p)) where
   ppr = pprFamilyDecl TopLevel
diff --git a/compiler/deSugar/ExtractDocs.hs b/compiler/deSugar/ExtractDocs.hs
index 8612a05..632207c 100644
--- a/compiler/deSugar/ExtractDocs.hs
+++ b/compiler/deSugar/ExtractDocs.hs
@@ -14,7 +14,6 @@ import GHC.Hs.Binds
 import GHC.Hs.Doc
 import GHC.Hs.Decls
 import GHC.Hs.Extension
-import GHC.Hs.Pat
 import GHC.Hs.Types
 import GHC.Hs.Utils
 import Name
@@ -117,8 +116,7 @@ user-written. This lets us relate Names (from ClsInsts) to comments
 (associated with InstDecls and DerivDecls).
 -}
 
-getMainDeclBinder :: XRec pass Pat ~ Located (Pat pass) =>
-                     HsDecl pass -> [IdP pass]
+getMainDeclBinder :: HsDecl (GhcPass p) -> [IdP (GhcPass p)]
 getMainDeclBinder (TyClD _ d) = [tcdName d]
 getMainDeclBinder (ValD _ d) =
   case collectHsBindBinders d of
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 3d06019..9db8880 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -36,7 +36,7 @@ module TcHsSyn (
         zonkTopBndrs,
         ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
         zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
-        zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrs,
+        zonkTyBndrs, zonkTyBndrsX,
         zonkTcTypeToType,  zonkTcTypeToTypeX,
         zonkTcTypesToTypes, zonkTcTypesToTypesX,
         zonkTyVarOcc,
@@ -327,20 +327,14 @@ extendZonkEnv ze@(ZonkEnv { ze_tv_env = tyco_env, ze_id_env = id_env }) vars
   where
     (tycovars, ids) = partition isTyCoVar vars
 
-extendIdZonkEnv1 :: ZonkEnv -> Var -> ZonkEnv
-extendIdZonkEnv1 ze@(ZonkEnv { ze_id_env = id_env }) id
+extendIdZonkEnv :: ZonkEnv -> Var -> ZonkEnv
+extendIdZonkEnv ze@(ZonkEnv { ze_id_env = id_env }) id
   = ze { ze_id_env = extendVarEnv id_env id id }
 
-extendTyZonkEnv1 :: ZonkEnv -> TyVar -> ZonkEnv
-extendTyZonkEnv1 ze@(ZonkEnv { ze_tv_env = ty_env }) tv
+extendTyZonkEnv :: ZonkEnv -> TyVar -> ZonkEnv
+extendTyZonkEnv ze@(ZonkEnv { ze_tv_env = ty_env }) tv
   = ze { ze_tv_env = extendVarEnv ty_env tv tv }
 
-extendTyZonkEnvN :: ZonkEnv -> [(Name,TyVar)] -> ZonkEnv
-extendTyZonkEnvN ze@(ZonkEnv { ze_tv_env = ty_env }) pairs
-  = ze { ze_tv_env = foldl add ty_env pairs }
-  where
-    add env (name, tv) = extendVarEnv_Directly env (getUnique name) tv
-
 setZonkType :: ZonkEnv -> ZonkFlexi -> ZonkEnv
 setZonkType ze flexi = ze { ze_flexi = flexi }
 
@@ -429,7 +423,7 @@ zonkEvVarOcc env v
 zonkCoreBndrX :: ZonkEnv -> Var -> TcM (ZonkEnv, Var)
 zonkCoreBndrX env v
   | isId v = do { v' <- zonkIdBndr env v
-                ; return (extendIdZonkEnv1 env v', v') }
+                ; return (extendIdZonkEnv env v', v') }
   | otherwise = zonkTyBndrX env v
 
 zonkCoreBndrsX :: ZonkEnv -> [Var] -> TcM (ZonkEnv, [Var])
@@ -444,12 +438,16 @@ zonkTyBndrsX = mapAccumLM zonkTyBndrX
 zonkTyBndrX :: ZonkEnv -> TcTyVar -> TcM (ZonkEnv, TyVar)
 -- This guarantees to return a TyVar (not a TcTyVar)
 -- then we add it to the envt, so all occurrences are replaced
+--
+-- It does not clone: the new TyVar has the sane Name
+-- as the old one.  This important when zonking the
+-- TyVarBndrs of a TyCon, whose Names may scope.
 zonkTyBndrX env tv
   = ASSERT2( isImmutableTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) )
     do { ki <- zonkTcTypeToTypeX env (tyVarKind tv)
                -- Internal names tidy up better, for iface files.
        ; let tv' = mkTyVar (tyVarName tv) ki
-       ; return (extendTyZonkEnv1 env tv', tv') }
+       ; return (extendTyZonkEnv env tv', tv') }
 
 zonkTyVarBinders ::  [VarBndr TcTyVar vis]
                  -> TcM (ZonkEnv, [VarBndr TyVar vis])
@@ -466,22 +464,6 @@ zonkTyVarBinderX env (Bndr tv vis)
   = do { (env', tv') <- zonkTyBndrX env tv
        ; return (env', Bndr tv' vis) }
 
-zonkRecTyVarBndrs :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
--- This rather specialised function is used in exactly one place.
--- See Note [Tricky scoping in generaliseTcTyCon] in TcTyClsDecls.
-zonkRecTyVarBndrs names tc_tvs
-  = initZonkEnv $ \ ze ->
-    fixM $ \ ~(_, rec_new_tvs) ->
-    do { let ze' = extendTyZonkEnvN ze $
-                   zipWithLazy (\ tc_tv new_tv -> (getName tc_tv, new_tv))
-                               tc_tvs rec_new_tvs
-       ; new_tvs <- zipWithM (zonk_one ze') names tc_tvs
-       ; return (ze', new_tvs) }
-  where
-    zonk_one ze name tc_tv
-      = do { ki <- zonkTcTypeToTypeX ze (tyVarKind tc_tv)
-           ; return (mkTyVar name ki) }
-
 zonkTopExpr :: HsExpr GhcTcId -> TcM (HsExpr GhcTc)
 zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e
 
@@ -1357,7 +1339,7 @@ zonk_pat env (WildPat ty)
 
 zonk_pat env (VarPat x (L l v))
   = do  { v' <- zonkIdBndr env v
-        ; return (extendIdZonkEnv1 env v', VarPat x (L l v')) }
+        ; return (extendIdZonkEnv env v', VarPat x (L l v')) }
 
 zonk_pat env (LazyPat x pat)
   = do  { (env', pat') <- zonkPat env pat
@@ -1369,7 +1351,7 @@ zonk_pat env (BangPat x pat)
 
 zonk_pat env (AsPat x (L loc v) pat)
   = do  { v' <- zonkIdBndr env v
-        ; (env', pat') <- zonkPat (extendIdZonkEnv1 env v') pat
+        ; (env', pat') <- zonkPat (extendIdZonkEnv env v') pat
         ; return (env', AsPat x (L loc v') pat') }
 
 zonk_pat env (ViewPat ty expr pat)
@@ -1459,7 +1441,7 @@ zonk_pat env (NPlusKPat ty (L loc n) (L l lit1) lit2 e1 e2)
         ; lit1' <- zonkOverLit env2 lit1
         ; lit2' <- zonkOverLit env2 lit2
         ; ty' <- zonkTcTypeToTypeX env2 ty
-        ; return (extendIdZonkEnv1 env2 n',
+        ; return (extendIdZonkEnv env2 n',
                   NPlusKPat ty' (L loc n') (L l lit1') lit2' e1' e2') }
 
 zonk_pat env (CoPat x co_fn pat ty)
@@ -1607,7 +1589,7 @@ zonkCoreExpr env (Case scrut b ty alts)
     = do scrut' <- zonkCoreExpr env scrut
          ty' <- zonkTcTypeToTypeX env ty
          b' <- zonkIdBndr env b
-         let env1 = extendIdZonkEnv1 env b'
+         let env1 = extendIdZonkEnv env b'
          alts' <- mapM (zonkCoreAlt env1) alts
          return $ Case scrut' b' ty' alts'
 
@@ -1621,7 +1603,7 @@ zonkCoreBind :: ZonkEnv -> CoreBind -> TcM (ZonkEnv, CoreBind)
 zonkCoreBind env (NonRec v e)
     = do v' <- zonkIdBndr env v
          e' <- zonkCoreExpr env e
-         let env1 = extendIdZonkEnv1 env v'
+         let env1 = extendIdZonkEnv env v'
          return (env1, NonRec v' e')
 zonkCoreBind env (Rec pairs)
     = do (env1, pairs') <- fixM go
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 32fbae7..5726fc0 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -2009,11 +2009,10 @@ kcInferDeclHeader name flav
                --
                -- 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]
+             all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
+               -- NB: bindExplicitTKBndrs_Q_Tv does not clone;
+               --     ditto Implicit
+               -- See Note [Non-cloning for tyvar binders]
 
              tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
                                False -- not yet generalised
@@ -2039,98 +2038,102 @@ kcCheckDeclHeader_sig
   -> LHsQTyVars GhcRn  -- ^ Binders in the header
   -> TcM ContextKind   -- ^ The result kind. AnyKind == no result signature
   -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
-kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki =
-  addTyConFlavCtxt name flav $
-    pushTcLevelM_ $
-    solveEqualities $  -- #16687
-    bind_implicit (hsq_ext ktvs) $ \implicit_tcv_prs -> do
-
-      -- Step 1: zip user-written binders with quantifiers from the kind signature.
-      -- For example:
-      --
-      --   type F :: forall k -> k -> forall j. j -> Type
-      --   data F i a b = ...
-      --
-      -- Results in the following 'zipped_binders':
-      --
-      --                   TyBinder      LHsTyVarBndr
-      --    ---------------------------------------
-      --    ZippedBinder   forall k ->   i
-      --    ZippedBinder   k ->          a
-      --    ZippedBinder   forall j.
-      --    ZippedBinder   j ->          b
-      --
-      let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig (hsq_explicit ktvs)
-
-      -- Report binders that don't have a corresponding quantifier.
-      -- For example:
-      --
-      --   type T :: Type -> Type
-      --   data T b1 b2 b3 = ...
-      --
-      -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders.
-      --
-      unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs)
-
-      -- Convert each ZippedBinder to TyConBinder        for  tyConBinders
-      --                       and to [(Name, TcTyVar)]  for  tcTyConScopedTyVars
-      (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders
-
-      tcExtendNameTyVarEnv explicit_tv_prs $ do
-
-        -- Check that inline kind annotations on binders are valid.
-        -- For example:
-        --
-        --   type T :: Maybe k -> Type
-        --   data T (a :: Maybe j) = ...
-        --
-        -- Here we unify   Maybe k ~ Maybe j
-        mapM_ check_zipped_binder zipped_binders
-
-        -- Kind-check the result kind annotation, if present:
-        --
-        --    data T a b :: res_ki where
-        --               ^^^^^^^^^
-        -- We do it here because at this point the environment has been
-        -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'.
-        m_res_ki <- kc_res_ki >>= \ctx_k ->
-          case ctx_k of
-            AnyKind -> return Nothing
-            _ -> Just <$> newExpectedKind ctx_k
-
-        -- Step 2: split off invisible binders.
-        -- For example:
-        --
-        --   type F :: forall k1 k2. (k1, k2) -> Type
-        --   type family F
-        --
-        -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'?
-        -- See Note [Arity inference in kcCheckDeclHeader_sig]
-        let (invis_binders, r_ki) = split_invis kisig' m_res_ki
-
-        -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders.
-        invis_tcbs <- mapM invis_to_tcb invis_binders
-
-        -- Check that the inline result kind annotation is valid.
-        -- For example:
-        --
-        --   type T :: Type -> Maybe k
-        --   type family T a :: Maybe j where
-        --
-        -- Here we unify   Maybe k ~ Maybe j
-        whenIsJust m_res_ki $ \res_ki ->
-          discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
-          unifyKind Nothing r_ki res_ki
+kcCheckDeclHeader_sig kisig name flav
+          (HsQTvs { hsq_ext      = implicit_nms
+                  , hsq_explicit = explicit_nms }) kc_res_ki
+  = addTyConFlavCtxt name flav $
+    do {  -- Step 1: zip user-written binders with quantifiers from the kind signature.
+          -- For example:
+          --
+          --   type F :: forall k -> k -> forall j. j -> Type
+          --   data F i a b = ...
+          --
+          -- Results in the following 'zipped_binders':
+          --
+          --                   TyBinder      LHsTyVarBndr
+          --    ---------------------------------------
+          --    ZippedBinder   forall k ->   i
+          --    ZippedBinder   k ->          a
+          --    ZippedBinder   forall j.
+          --    ZippedBinder   j ->          b
+          --
+          let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig explicit_nms
+
+          -- Report binders that don't have a corresponding quantifier.
+          -- For example:
+          --
+          --   type T :: Type -> Type
+          --   data T b1 b2 b3 = ...
+          --
+          -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders.
+          --
+        ; unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs)
+
+          -- Convert each ZippedBinder to TyConBinder        for  tyConBinders
+          --                       and to [(Name, TcTyVar)]  for  tcTyConScopedTyVars
+        ; (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders
+
+        ; (implicit_tvs, (invis_binders, r_ki))
+             <- pushTcLevelM_ $
+                solveEqualities $  -- #16687
+                bindImplicitTKBndrs_Tv implicit_nms $
+                tcExtendNameTyVarEnv explicit_tv_prs  $
+                do { -- Check that inline kind annotations on binders are valid.
+                     -- For example:
+                     --
+                     --   type T :: Maybe k -> Type
+                     --   data T (a :: Maybe j) = ...
+                     --
+                     -- Here we unify   Maybe k ~ Maybe j
+                     mapM_ check_zipped_binder zipped_binders
+
+                     -- Kind-check the result kind annotation, if present:
+                     --
+                     --    data T a b :: res_ki where
+                     --               ^^^^^^^^^
+                     -- We do it here because at this point the environment has been
+                     -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'.
+                   ; ctx_k <- kc_res_ki
+                   ; m_res_ki <- case ctx_k of
+                                  AnyKind -> return Nothing
+                                  _ -> Just <$> newExpectedKind ctx_k
+
+                     -- Step 2: split off invisible binders.
+                     -- For example:
+                     --
+                     --   type F :: forall k1 k2. (k1, k2) -> Type
+                     --   type family F
+                     --
+                     -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'?
+                     -- See Note [Arity inference in kcCheckDeclHeader_sig]
+                   ; let (invis_binders, r_ki) = split_invis kisig' m_res_ki
+
+                     -- Check that the inline result kind annotation is valid.
+                     -- For example:
+                     --
+                     --   type T :: Type -> Maybe k
+                     --   type family T a :: Maybe j where
+                     --
+                     -- Here we unify   Maybe k ~ Maybe j
+                   ; whenIsJust m_res_ki $ \res_ki ->
+                      discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
+                      unifyKind Nothing r_ki res_ki
+
+                   ; return (invis_binders, r_ki) }
 
         -- Zonk the implicitly quantified variables.
-        implicit_tv_prs <- mapSndM zonkTcTyVarToTyVar implicit_tcv_prs
+        ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
+
+        -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders.
+        ; invis_tcbs <- mapM invis_to_tcb invis_binders
 
         -- Build the final, generalized TcTyCon
-        let tcbs       = vis_tcbs ++ invis_tcbs
-            all_tv_prs = implicit_tv_prs ++ explicit_tv_prs
-            tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav
+        ; let tcbs            = vis_tcbs ++ invis_tcbs
+              implicit_tv_prs = implicit_nms `zip` implicit_tvs
+              all_tv_prs      = implicit_tv_prs ++ explicit_tv_prs
+              tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav
 
-        traceTc "kcCheckDeclHeader_sig done:" $ vcat
+        ; traceTc "kcCheckDeclHeader_sig done:" $ vcat
           [ text "tyConName = " <+> ppr (tyConName tc)
           , text "kisig =" <+> debugPprType kisig
           , text "tyConKind =" <+> debugPprType (tyConKind tc)
@@ -2138,7 +2141,7 @@ kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki =
           , text "tcTyConScopedTyVars" <+> ppr (tcTyConScopedTyVars tc)
           , text "tyConResKind" <+> debugPprType (tyConResKind tc)
           ]
-        return tc
+        ; return tc }
   where
     -- Consider this declaration:
     --
@@ -2208,14 +2211,6 @@ kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki =
       MASSERT(null stv)
       return tcb
 
-    -- similar to:  bindImplicitTKBndrs_Tv
-    bind_implicit :: [Name] -> ([(Name,TcTyVar)] -> TcM a) -> TcM a
-    bind_implicit tv_names thing_inside =
-      do { let new_tv name = do { tcv <- newFlexiKindedTyVarTyVar name
-                                ; return (name, tcv) }
-         ; tcvs <- mapM new_tv tv_names
-         ; tcExtendNameTyVarEnv tcvs (thing_inside tcvs) }
-
     -- Check that the inline kind annotation on a binder is valid
     -- by unifying it with the kind of the quantifier.
     check_zipped_binder :: ZippedBinder -> TcM ()
@@ -2245,6 +2240,8 @@ kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki =
           n_inst = n_sig_invis_bndrs - n_res_invis_bndrs
       in splitPiTysInvisibleN n_inst sig_ki
 
+kcCheckDeclHeader_sig _ _ _ (XLHsQTyVars nec) _ = noExtCon nec
+
 -- A quantifier from a kind signature zipped with a user-written binder for it.
 data ZippedBinder =
   ZippedBinder TyBinder (Maybe (LHsTyVarBndr GhcRn))
@@ -2578,6 +2575,56 @@ expectedKindInCtxt _                   = OpenKind
 *                                                                      *
 ********************************************************************* -}
 
+{- Note [Non-cloning for tyvar binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+bindExplictTKBndrs_Q_Skol, bindExplictTKBndrs_Skol, do not clone;
+and nor do the Implicit versions.  There is no need.
+
+bindExplictTKBndrs_Q_Tv does not clone; and similarly Implicit.
+We take advantage of this in kcInferDeclHeader:
+     all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
+If we cloned, we'd need to take a bit more care here; not hard.
+
+The main payoff is that avoidng gratuitious cloning means that we can
+almost always take the fast path in swizzleTcTyConBndrs.  "Almost
+always" means not the case of mutual recursion with polymorphic kinds.
+
+
+Note [Cloning for tyvar binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+bindExplicitTKBndrs_Tv does cloning, making up a Name with a fresh Unique,
+unlike bindExplicitTKBndrs_Q_Tv.  (Nor do the Skol variants clone.)
+And similarly for bindImplicit...
+
+This for a narrow and tricky reason which, alas, I couldn't find a
+simpler way round.  #16221 is the poster child:
+
+   data SameKind :: k -> k -> *
+   data T a = forall k2 (b :: k2). MkT (SameKind a b) !Int
+
+When kind-checking T, we give (a :: kappa1). Then:
+
+- In kcConDecl we make a TyVarTv unification variable kappa2 for k2
+  (as described in Note [Kind-checking for GADTs], even though this
+  example is an existential)
+- So we get (b :: kappa2) via bindExplicitTKBndrs_Tv
+- We end up unifying kappa1 := kappa2, because of the (SameKind a b)
+
+Now we generalise over kappa2. But if kappa2's Name is precisely k2
+(i.e. we did not clone) we'll end up giving T the utterlly final kind
+  T :: forall k2. k2 -> *
+Nothing directly wrong with that but when we typecheck the data constructor
+we have k2 in scope; but then it's brought into scope /again/ when we find
+the forall k2.  This is chaotic, and we end up giving it the type
+  MkT :: forall k2 (a :: k2) k2 (b :: k2).
+         SameKind @k2 a b -> Int -> T @{k2} a
+which is bogus -- because of the shadowing of k2, we can't
+apply T to the kind or a!
+
+And there no reason /not/ to clone the Name when making a unification
+variable.  So that's what we do.
+-}
+
 --------------------------------------
 -- Implicit binders
 --------------------------------------
@@ -2585,10 +2632,12 @@ expectedKindInCtxt _                   = OpenKind
 bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
   bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
   :: [Name] -> TcM a -> TcM ([TcTyVar], a)
-bindImplicitTKBndrs_Skol   = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar
-bindImplicitTKBndrs_Tv     = bindImplicitTKBndrsX newFlexiKindedTyVarTyVar
 bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedSkolemTyVar)
 bindImplicitTKBndrs_Q_Tv   = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedTyVarTyVar)
+bindImplicitTKBndrs_Skol   = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar
+bindImplicitTKBndrs_Tv     = bindImplicitTKBndrsX cloneFlexiKindedTyVarTyVar
+  -- newFlexiKinded...           see Note [Non-cloning for tyvar binders]
+  -- cloneFlexiKindedTyVarTyVar: see Note [Cloning for tyvar binders]
 
 bindImplicitTKBndrsX
    :: (Name -> TcM TcTyVar) -- new_tv function
@@ -2621,7 +2670,10 @@ newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
 
 newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
 newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
-   -- See Note [Unification variables need fresh Names] in TcMType
+
+cloneFlexiKindedTyVarTyVar :: Name -> TcM TyVar
+cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar
+   -- See Note [Cloning for tyvar binders]
 
 --------------------------------------
 -- Explicit binders
@@ -2633,7 +2685,9 @@ bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
     -> TcM ([TcTyVar], a)
 
 bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar)
-bindExplicitTKBndrs_Tv   = bindExplicitTKBndrsX (tcHsTyVarBndr newTyVarTyVar)
+bindExplicitTKBndrs_Tv   = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar)
+  -- newSkolemTyVar:  see Note [Non-cloning for tyvar binders]
+  -- cloneTyVarTyVar: see Note [Cloning for tyvar binders]
 
 bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
     :: ContextKind
@@ -2643,6 +2697,8 @@ bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
 
 bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newSkolemTyVar)
 bindExplicitTKBndrs_Q_Tv   ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newTyVarTyVar)
+  -- See Note [Non-cloning for tyvar binders]
+
 
 bindExplicitTKBndrsX
     :: (HsTyVarBndr GhcRn -> TcM TcTyVar)
@@ -2662,7 +2718,7 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
             -- is mentioned in the kind of a later binder
             --   e.g. forall k (a::k). blah
             -- NB: tv's Name may differ from hs_tv's
-            -- See TcMType Note [Unification variables need fresh Names]
+            -- See TcMType Note [Cloning for tyvar binders]
             ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
                            go hs_tvs
             ; return (tv:tvs, res) }
@@ -2670,7 +2726,6 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
 -----------------
 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
               -> HsTyVarBndr GhcRn -> TcM TcTyVar
--- Returned TcTyVar has the same name; no cloning
 tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
   = do { kind <- newMetaKindVar
        ; new_tv tv_nm kind }
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 8a50e66..52599c9 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -57,7 +57,8 @@ module TcMType (
   -- Instantiation
   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
   newMetaTyVarTyVars, newMetaTyVarTyVarX,
-  newTyVarTyVar, newPatSigTyVar, newSkolemTyVar, newWildCardX,
+  newTyVarTyVar, cloneTyVarTyVar,
+  newPatSigTyVar, newSkolemTyVar, newWildCardX,
   tcInstType,
   tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
   tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
@@ -707,30 +708,6 @@ cloneMetaTyVarName name
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 At the moment we give a unification variable a System Name, which
 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
-
-Note [Unification variables need fresh Names]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Whenever we allocate a unification variable (MetaTyVar) we give
-it a fresh name.   #16221 is a very tricky case that illustrates
-why this is important:
-
-   data SameKind :: k -> k -> *
-   data T0 a = forall k2 (b :: k2). MkT0 (SameKind a b) !Int
-
-When kind-checking T0, we give (a :: kappa1). Then, in kcConDecl
-we allocate a unification variable kappa2 for k2, and then we
-end up unifying kappa1 := kappa2 (because of the (SameKind a b).
-
-Now we generalise over kappa2; but if kappa2's Name is k2,
-we'll end up giving T0 the kind forall k2. k2 -> *.  Nothing
-directly wrong with that but when we typecheck the data constrautor
-we end up giving it the type
-  MkT0 :: forall k1 (a :: k1) k2 (b :: k2).
-          SameKind @k2 a b -> Int -> T0 @{k2} a
-which is bogus.  The result type should be T0 @{k1} a.
-
-And there no reason /not/ to clone the Name when making a
-unification variable.  So that's what we do.
 -}
 
 metaInfoToTyVarName :: MetaInfo -> FastString
@@ -762,9 +739,18 @@ newSkolemTyVar name kind
 
 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
 -- See Note [TyVarTv]
--- See Note [Unification variables need fresh Names]
+-- Does not clone a fresh unique
 newTyVarTyVar name kind
   = do { details <- newMetaDetails TyVarTv
+       ; let tyvar = mkTcTyVar name kind details
+       ; traceTc "newTyVarTyVar" (ppr tyvar)
+       ; return tyvar }
+
+cloneTyVarTyVar :: Name -> Kind -> TcM TcTyVar
+-- See Note [TyVarTv]
+-- Clones a fresh unique
+cloneTyVarTyVar name kind
+  = do { details <- newMetaDetails TyVarTv
        ; uniq <- newUnique
        ; let name' = name `setNameUnique` uniq
              tyvar = mkTcTyVar name' kind details
@@ -772,7 +758,7 @@ newTyVarTyVar name kind
          -- We want to keep the original more user-friendly Name
          -- In practical terms that means that in error messages,
          -- when the Name is tidied we get 'a' rather than 'a0'
-       ; traceTc "newTyVarTyVar" (ppr tyvar)
+       ; traceTc "cloneTyVarTyVar" (ppr tyvar)
        ; return tyvar }
 
 newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
@@ -1315,11 +1301,11 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
     go dv (CoercionTy co)   = collect_cand_qtvs_co orig_ty bound dv co
 
     go dv (TyVarTy tv)
-      | is_bound tv      = return dv
-      | otherwise        = do { m_contents <- isFilledMetaTyVar_maybe tv
-                              ; case m_contents of
-                                  Just ind_ty -> go dv ind_ty
-                                  Nothing     -> go_tv dv tv }
+      | is_bound tv = return dv
+      | otherwise   = do { m_contents <- isFilledMetaTyVar_maybe tv
+                         ; case m_contents of
+                             Just ind_ty -> go dv ind_ty
+                             Nothing     -> go_tv dv tv }
 
     go dv (ForAllTy (Bndr tv _) ty)
       = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index bceb901..3048d61 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -6,7 +6,7 @@
 TcTyClsDecls: Typecheck type and class declarations
 -}
 
-{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
+{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables, MultiWayIf #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
 
@@ -80,11 +80,12 @@ import qualified GHC.LanguageExtensions as LangExt
 import Control.Monad
 import Data.Foldable
 import Data.Function ( on )
+import Data.Functor.Identity
 import Data.List
 import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
 import qualified Data.Set as Set
-
+import Data.Tuple( swap )
 
 {-
 ************************************************************************
@@ -433,6 +434,108 @@ TcTyCons are used for two distinct purposes
 
 See also Note [Type checking recursive type and class declarations].
 
+Note [Swizzling the tyvars before generaliseTcTyCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This Note only applies when /inferring/ the kind of a TyCon.
+If there is a separate kind signature, or a CUSK, we take an entirely
+different code path.
+
+For inference, consider
+   class C (f :: k) x where
+      type T f
+      op :: D f => blah
+   class D (g :: j) y where
+      op :: C g => y -> blah
+
+Here C and D are considered mutually recursive.  Neither has a CUSK.
+Just before generalisation we have the (un-quantified) kinds
+   C :: k1 -> k2 -> Constraint
+   T :: k1 -> Type
+   D :: k1 -> Type -> Constraint
+Notice that f's kind and g's kind have been unified to 'k1'. We say
+that k1 is the "representative" of k in C's decl, and of j in D's decl.
+
+Now when quantifying, we'd like to end up with
+   C :: forall {k2}. forall k. k -> k2 -> Constraint
+   T :: forall k. k -> Type
+   D :: forall j. j -> Type -> Constraint
+
+That is, we want to swizzle the representative to have the Name given
+by the user. Partly this is to improve error messages and the output of
+:info in GHCi.  But it is /also/ important because the code for a
+default method may mention the class variable(s), but at that point
+(tcClassDecl2), we only have the final class tyvars available.
+(Alternatively, we could record the scoped type variables in the
+TyCon, but it's a nuisance to do so.)
+
+Notes:
+
+* On the input to generaliseTyClDecl, the mapping between the
+  user-specified Name and the representative TyVar is recorded in the
+  tyConScopedTyVars of the TcTyCon.  NB: you first need to zonk to see
+  this representative TyVar.
+
+* The swizzling is actually performed by swizzleTcTyConBndrs
+
+* We must do the swizzling across the whole class decl. Consider
+     class C f where
+       type S (f :: k)
+       type T f
+  Here f's kind k is a parameter of C, and its identity is shared
+  with S and T.  So if we swizzle the representative k at all, we
+  must do so consistently for the entire declaration.
+
+  Hence the call to check_duplicate_tc_binders is in generaliseTyClDecl,
+  rather than in generaliseTcTyCon.
+
+There are errors to catch here.  Suppose we had
+   class E (f :: j) (g :: k) where
+     op :: SameKind f g -> blah
+
+Then, just before generalisation we will have the (unquantified)
+   E :: k1 -> k1 -> Constraint
+
+That's bad!  Two distinctly-named tyvars (j and k) have ended up with
+the same representative k1.  So when swizzling, we check (in
+check_duplicate_tc_binders) that two distinct source names map
+to the same representative.
+
+Here's an interesting case:
+    class C1 f where
+      type S (f :: k1)
+      type T (f :: k2)
+Here k1 and k2 are different Names, but they end up mapped to the
+same representative TyVar.  To make the swizzling consistent (remember
+we must have a single k across C1, S and T) we reject the program.
+
+Another interesting case
+    class C2 f where
+      type S (f :: k) (p::Type)
+      type T (f :: k) (p::Type->Type)
+
+Here the two k's (and the two p's) get distinct Uniques, because they
+are seen by the renamer as locally bound in S and T resp.  But again
+the two (distinct) k's end up bound to the same representative TyVar.
+You might argue that this should be accepted, but it's definitely
+rejected (via an entirely different code path) if you add a kind sig:
+    type C2' :: j -> Constraint
+    class C2' f where
+      type S (f :: k) (p::Type)
+We get
+    • Expected kind ‘j’, but ‘f’ has kind ‘k’
+    • In the associated type family declaration for ‘S’
+
+So we reject C2 too, even without the kind signature.  We have
+to do a bit of work to get a good error message, since both k's
+look the same to the user.
+
+Another case
+    class C3 (f :: k1) where
+      type S (f :: k2)
+
+This will be rejected too.
+
+
 Note [Type environment evolution]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 As we typecheck a group of declarations the type environment evolves.
@@ -571,107 +674,227 @@ kcTyClGroup kisig_env decls
         -- Finally, go through each tycon and give it its final kind,
         -- with all the required, specified, and inferred variables
         -- in order.
-        ; generalized_tcs <- mapAndReportM generaliseTcTyCon inferred_tcs
+        ; let inferred_tc_env = mkNameEnv $
+                                map (\tc -> (tyConName tc, tc)) inferred_tcs
+        ; generalized_tcs <- concatMapM (generaliseTyClDecl inferred_tc_env)
+                                        kindless_decls
 
         ; let poly_tcs = checked_tcs ++ generalized_tcs
         ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
         ; return poly_tcs }
-
   where
     ppr_tc_kinds tcs = vcat (map pp_tc tcs)
     pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)
 
-generaliseTcTyCon :: TcTyCon -> TcM TcTyCon
-generaliseTcTyCon tc
+type ScopedPairs = [(Name, TcTyVar)]
+  -- The ScopedPairs for a TcTyCon are precisely
+  --    specified-tvs ++ required-tvs
+  -- You can distinguish them because there are tyConArity required-tvs
+
+generaliseTyClDecl :: NameEnv TcTyCon -> LTyClDecl GhcRn -> TcM [TcTyCon]
+-- See Note [Swizzling the tyvars before generaliseTcTyCon]
+generaliseTyClDecl inferred_tc_env (L _ decl)
+  = do { let names_in_this_decl :: [Name]
+             names_in_this_decl = tycld_names decl
+
+       -- Extract the specified/required binders and skolemise them
+       ; tc_with_tvs  <- mapM skolemise_tc_tycon names_in_this_decl
+
+       -- Zonk, to manifest the side-effects of skolemisation to the swizzler
+       -- NB: it's important to skolemise them all before this step. E.g.
+       --         class C f where { type T (f :: k) }
+       --     We only skolemise k when looking at T's binders,
+       --     but k appears in f's kind in C's binders.
+       ; tc_infos <- mapM zonk_tc_tycon tc_with_tvs
+
+       -- Swizzle
+       ; swizzled_infos <- tcAddDeclCtxt decl (swizzleTcTyConBndrs tc_infos)
+
+       -- And finally generalise
+       ; mapAndReportM generaliseTcTyCon swizzled_infos }
+  where
+    tycld_names :: TyClDecl GhcRn -> [Name]
+    tycld_names decl = tcdName decl : at_names decl
+
+    at_names :: TyClDecl GhcRn -> [Name]
+    at_names (ClassDecl { tcdATs = ats }) = map (familyDeclName . unLoc) ats
+    at_names _ = []  -- Only class decls have associated types
+
+    skolemise_tc_tycon :: Name -> TcM (TcTyCon, ScopedPairs)
+    -- Zonk and skolemise the Specified and Required binders
+    skolemise_tc_tycon tc_name
+      = do { let tc = lookupNameEnv_NF inferred_tc_env tc_name
+                      -- This lookup should not fail
+           ; scoped_prs <- mapSndM zonkAndSkolemise (tcTyConScopedTyVars tc)
+           ; return (tc, scoped_prs) }
+
+    zonk_tc_tycon :: (TcTyCon, ScopedPairs) -> TcM (TcTyCon, ScopedPairs, TcKind)
+    zonk_tc_tycon (tc, scoped_prs)
+      = do { scoped_prs <- mapSndM zonkTcTyVarToTyVar scoped_prs
+                           -- We really have to do this again, even though
+                           -- we have just done zonkAndSkolemise
+           ; res_kind   <- zonkTcType (tyConResKind tc)
+           ; return (tc, scoped_prs, res_kind) }
+
+swizzleTcTyConBndrs :: [(TcTyCon, ScopedPairs, TcKind)]
+                -> TcM [(TcTyCon, ScopedPairs, TcKind)]
+swizzleTcTyConBndrs tc_infos
+  | all no_swizzle swizzle_prs
+    -- This fast path happens almost all the time
+    -- See Note [Non-cloning for tyvar binders] in TcHsType
+  = do { traceTc "Skipping swizzleTcTyConBndrs for" (ppr (map fstOf3 tc_infos))
+       ; return tc_infos }
+
+  | otherwise
+  = do { check_duplicate_tc_binders
+
+       ; traceTc "swizzleTcTyConBndrs" $
+         vcat [ text "before" <+> ppr_infos tc_infos
+              , text "swizzle_prs" <+> ppr swizzle_prs
+              , text "after" <+> ppr_infos swizzled_infos ]
+
+       ; return swizzled_infos }
+
+  where
+    swizzled_infos =  [ (tc, mapSnd swizzle_var scoped_prs, swizzle_ty kind)
+                      | (tc, scoped_prs, kind) <- tc_infos ]
+
+    swizzle_prs :: [(Name,TyVar)]
+    -- Pairs the user-specifed Name with its representative TyVar
+    -- See Note [Swizzling the tyvars before generaliseTcTyCon]
+    swizzle_prs = [ pr | (_, prs, _) <- tc_infos, pr <- prs ]
+
+    no_swizzle :: (Name,TyVar) -> Bool
+    no_swizzle (nm, tv) = nm == tyVarName tv
+
+    ppr_infos infos = vcat [ ppr tc <+> pprTyVars (map snd prs)
+                           | (tc, prs, _) <- infos ]
+
+    -- Check for duplicates
+    -- E.g. data SameKind (a::k) (b::k)
+    --      data T (a::k1) (b::k2) = MkT (SameKind a b)
+    -- Here k1 and k2 start as TyVarTvs, and get unified with each other
+    -- If this happens, things get very confused later, so fail fast
+    check_duplicate_tc_binders :: TcM ()
+    check_duplicate_tc_binders = unless (null err_prs) $
+                                 do { mapM_ report_dup err_prs; failM }
+
+    -------------- Error reporting ------------
+    err_prs :: [(Name,Name)]
+    err_prs = [ (n1,n2)
+              | pr :| prs <- findDupsEq ((==) `on` snd) swizzle_prs
+              , (n1,_):(n2,_):_ <- [nubBy ((==) `on` fst) (pr:prs)] ]
+              -- This nubBy avoids bogus error reports when we have
+              --    [("f", f), ..., ("f",f)....] in swizzle_prs
+              -- which happens with  class C f where { type T f }
+
+    report_dup :: (Name,Name) -> TcM ()
+    report_dup (n1,n2)
+      = setSrcSpan (getSrcSpan n2) $ addErrTc $
+        hang (text "Different names for the same type variable:") 2 info
+      where
+        info | nameOccName n1 /= nameOccName n2
+             = quotes (ppr n1) <+> text "and" <+> quotes (ppr n2)
+             | otherwise -- Same OccNames! See C2 in
+                         -- Note [Swizzling the tyvars before generaliseTcTyCon]
+             = vcat [ quotes (ppr n1) <+> text "bound at" <+> ppr (getSrcLoc n1)
+                    , quotes (ppr n2) <+> text "bound at" <+> ppr (getSrcLoc n2) ]
+
+    -------------- The swizzler ------------
+    -- This does a deep traverse, simply doing a
+    -- Name-to-Name change, governed by swizzle_env
+    -- The 'swap' is what gets from the representative TyVar
+    -- back to the original user-specified Name
+    swizzle_env = mkVarEnv (map swap swizzle_prs)
+
+    swizzleMapper :: TyCoMapper () Identity
+    swizzleMapper = TyCoMapper { tcm_tyvar = swizzle_tv
+                               , tcm_covar = swizzle_cv
+                               , tcm_hole  = swizzle_hole
+                               , tcm_tycobinder = swizzle_bndr
+                               , tcm_tycon      = swizzle_tycon }
+    swizzle_hole  _ hole = pprPanic "swizzle_hole" (ppr hole)
+       -- These types are pre-zonked
+    swizzle_tycon tc = pprPanic "swizzle_tc" (ppr tc)
+       -- TcTyCons can't appear in kinds (yet)
+    swizzle_tv _ tv = return (mkTyVarTy (swizzle_var tv))
+    swizzle_cv _ cv = return (mkCoVarCo (swizzle_var cv))
+
+    swizzle_bndr _ tcv _
+      = return ((), swizzle_var tcv)
+
+    swizzle_var :: Var -> Var
+    swizzle_var v
+      | Just nm <- lookupVarEnv swizzle_env v
+      = updateVarType swizzle_ty (v `setVarName` nm)
+      | otherwise
+      = updateVarType swizzle_ty v
+
+    swizzle_ty ty = runIdentity (mapType swizzleMapper () ty)
+
+
+generaliseTcTyCon :: (TcTyCon, ScopedPairs, TcKind) -> TcM TcTyCon
+generaliseTcTyCon (tc, scoped_prs, tc_res_kind)
   -- See Note [Required, Specified, and Inferred for types]
   = setSrcSpan (getSrcSpan tc) $
     addTyConCtxt tc $
-    do { let tc_name      = tyConName tc
-             tc_res_kind  = tyConResKind tc
-             spec_req_prs = tcTyConScopedTyVars tc
-
-             (spec_req_names, spec_req_tvs) = unzip spec_req_prs
-             -- NB: spec_req_tvs includes both Specified and Required
-             -- Running example in Note [Inferring kinds for type declarations]
-             --    spec_req_prs = [ ("k1",kk1), ("a", (aa::kk1))
-             --                   , ("k2",kk2), ("x", (xx::kk2))]
-             -- where "k1" denotes the Name k1, and kk1, aa, etc are MetaTyVars,
-             -- specifically TyVarTvs
-
-       -- Step 0: zonk and skolemise the Specified and Required binders
-       -- It's essential that they are skolems, not MetaTyVars,
-       -- for Step 3 to work right
-       ; spec_req_tvs <- mapM zonkAndSkolemise spec_req_tvs
-             -- Running example, where kk1 := kk2, so we get
-             --   [kk2,kk2]
-
-       -- Step 1: Check for duplicates
-       -- E.g. data SameKind (a::k) (b::k)
-       --      data T (a::k1) (b::k2) = MkT (SameKind a b)
-       -- Here k1 and k2 start as TyVarTvs, and get unified with each other
-       -- If this happens, things get very confused later, so fail fast
-       ; checkDuplicateTyConBinders spec_req_names spec_req_tvs
+    do { -- Step 1: Separate Specified from Required variables
+         -- NB: spec_req_tvs = spec_tvs ++ req_tvs
+         --     And req_tvs is 1-1 with tyConTyVars
+         --     See Note [Scoped tyvars in a TcTyCon] in TyCon
+       ; let spec_req_tvs        = map snd scoped_prs
+             n_spec              = length spec_req_tvs - tyConArity tc
+             (spec_tvs, req_tvs) = splitAt n_spec spec_req_tvs
+             sorted_spec_tvs     = scopedSort spec_tvs
+                 -- NB: We can't do the sort until we've zonked
+                 --     Maintain the L-R order of scoped_tvs
 
        -- Step 2a: find all the Inferred variables we want to quantify over
-       -- NB: candidateQTyVarsOfKinds zonks as it goes
        ; dvs1 <- candidateQTyVarsOfKinds $
-                (tc_res_kind : map tyVarKind spec_req_tvs)
+                 (tc_res_kind : map tyVarKind spec_req_tvs)
        ; let dvs2 = dvs1 `delCandidates` spec_req_tvs
 
        -- Step 2b: quantify, mainly meaning skolemise the free variables
        -- Returned 'inferred' are scope-sorted and skolemised
        ; inferred <- quantifyTyVars dvs2
 
-       -- Step 3a: rename all the Specified and Required tyvars back to
-       -- TyVars with their oroginal user-specified name.  Example
-       --     class C a_r23 where ....
-       -- By this point we have scoped_prs = [(a_r23, a_r89[TyVarTv])]
-       -- We return with the TyVar a_r23[TyVar],
-       --    and ze mapping a_r89 :-> a_r23[TyVar]
-       ; traceTc "generaliseTcTyCon: before zonkRec"
-           (vcat [ text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
+       ; traceTc "generaliseTcTyCon: pre zonk"
+           (vcat [ text "tycon =" <+> ppr tc
+                 , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
+                 , text "tc_res_kind =" <+> ppr tc_res_kind
+                 , text "dvs1 =" <+> ppr dvs1
                  , text "inferred =" <+> pprTyVars inferred ])
-       ; (ze, final_spec_req_tvs) <- zonkRecTyVarBndrs spec_req_names spec_req_tvs
-           -- So ze maps from the tyvars that have ended up
 
-       -- Step 3b: Apply that mapping to the other variables
-       -- (remember they all started as TyVarTvs).
-       -- They have been skolemised by quantifyTyVars.
-       ; (ze, inferred) <- zonkTyBndrsX ze inferred
-       ; tc_res_kind    <- zonkTcTypeToTypeX ze tc_res_kind
+       -- Step 3: Final zonk (following kind generalisation)
+       -- See Note [Swizzling the tyvars before generaliseTcTyCon]
+       ; ze <- emptyZonkEnv
+       ; (ze, inferred)        <- zonkTyBndrsX ze inferred
+       ; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs
+       ; (ze, req_tvs)         <- zonkTyBndrsX ze req_tvs
+       ; tc_res_kind           <- zonkTcTypeToTypeX ze tc_res_kind
 
        ; traceTc "generaliseTcTyCon: post zonk" $
          vcat [ text "tycon =" <+> ppr tc
               , text "inferred =" <+> pprTyVars inferred
-              , text "ze =" <+> ppr ze
-              , text "spec_req_prs =" <+> ppr spec_req_prs
               , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
-              , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs ]
-
-       -- Step 4: Find the Specified and Inferred variables
-       -- NB: spec_req_tvs = spec_tvs ++ req_tvs
-       --     And req_tvs is 1-1 with tyConTyVars
-       --     See Note [Scoped tyvars in a TcTyCon] in TyCon
-       ; let n_spec        = length final_spec_req_tvs - tyConArity tc
-             (spec_tvs, req_tvs) = splitAt n_spec final_spec_req_tvs
-             specified     = scopedSort spec_tvs
-                             -- NB: maintain the L-R order of scoped_tvs
-
-       -- Step 5: Make the TyConBinders.
-             to_user tv     = lookupTyVarOcc ze tv `orElse` tv
-             dep_fv_set     = mapVarSet to_user (candidateKindVars dvs1)
+              , text "sorted_spec_tvs =" <+> pprTyVars sorted_spec_tvs
+              , text "req_tvs =" <+> ppr req_tvs
+              , text "zonk-env =" <+> ppr ze ]
+
+       -- Step 4: Make the TyConBinders.
+       ; let dep_fv_set     = candidateKindVars dvs1
              inferred_tcbs  = mkNamedTyConBinders Inferred inferred
-             specified_tcbs = mkNamedTyConBinders Specified specified
+             specified_tcbs = mkNamedTyConBinders Specified sorted_spec_tvs
              required_tcbs  = map (mkRequiredTyConBinder dep_fv_set) req_tvs
 
-       -- Step 6: Assemble the final list.
+       -- Step 5: Assemble the final list.
              final_tcbs = concat [ inferred_tcbs
                                  , specified_tcbs
                                  , required_tcbs ]
 
-       -- Step 7: Make the result TcTyCon
-             tycon = mkTcTyCon tc_name final_tcbs tc_res_kind
-                            (mkTyVarNamePairs final_spec_req_tvs)
+       -- Step 6: Make the result TcTyCon
+             tycon = mkTcTyCon (tyConName tc) final_tcbs tc_res_kind
+                            (mkTyVarNamePairs (sorted_spec_tvs ++ req_tvs))
                             True {- it's generalised now -}
                             (tyConFlavour tc)
 
@@ -679,32 +902,18 @@ generaliseTcTyCon tc
          vcat [ text "tycon =" <+> ppr tc
               , text "tc_res_kind =" <+> ppr tc_res_kind
               , text "dep_fv_set =" <+> ppr dep_fv_set
-              , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs
-              , text "inferred =" <+> pprTyVars inferred
-              , text "specified =" <+> pprTyVars specified
+              , text "inferred_tcbs =" <+> ppr inferred_tcbs
+              , text "specified_tcbs =" <+> ppr specified_tcbs
               , text "required_tcbs =" <+> ppr required_tcbs
               , text "final_tcbs =" <+> ppr final_tcbs ]
 
-       -- Step 8: Check for validity.
+       -- Step 7: Check for validity.
        -- We do this here because we're about to put the tycon into the
        -- the environment, and we don't want anything malformed there
        ; checkTyConTelescope tycon
 
        ; return tycon }
 
-checkDuplicateTyConBinders :: [Name] -> [TcTyVar] -> TcM ()
-checkDuplicateTyConBinders spec_req_names spec_req_tvs
-  | null dups = return ()
-  | otherwise = mapM_ report_dup dups >> failM
-  where
-    dups :: [(Name,Name)]
-    dups = findDupTyVarTvs $ spec_req_names `zip` spec_req_tvs
-
-    report_dup (n1, n2)
-      = setSrcSpan (getSrcSpan n2) $
-        addErrTc (text "Couldn't match" <+> quotes (ppr n1)
-                        <+> text "with" <+> quotes (ppr n2))
-
 {- Note [Required, Specified, and Inferred for types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Each forall'd type variable in a type or kind is one of
@@ -1029,8 +1238,8 @@ mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
 mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
   = unitNameEnv nm (APromotionErr ClassPE)
     `plusNameEnv`
-    mkNameEnv [ (name, APromotionErr TyConPE)
-              | (L _ (FamilyDecl { fdLName = L _ name })) <- ats ]
+    mkNameEnv [ (familyDeclName at, APromotionErr TyConPE)
+              | L _ at <- ats ]
 
 mk_prom_err_env (DataDecl { tcdLName = L _ name
                           , tcdDataDefn = HsDataDefn { dd_cons = cons } })
@@ -1770,17 +1979,14 @@ tcTyClDecl1 _parent roles_info
                      , tcdRhs   = rhs })
   = ASSERT( isNothing _parent )
     fmap noDerivInfos $
-    bindTyClTyVars tc_name $ \ binders res_kind ->
-    tcTySynRhs roles_info tc_name binders res_kind rhs
+    tcTySynRhs roles_info tc_name rhs
 
   -- "data/newtype" declaration
 tcTyClDecl1 _parent roles_info
             decl@(DataDecl { tcdLName = L _ tc_name
                            , tcdDataDefn = defn })
   = ASSERT( isNothing _parent )
-    bindTyClTyVars tc_name $ \ tycon_binders res_kind ->
-    tcDataDefn (tcMkDeclCtxt decl) roles_info tc_name
-               tycon_binders res_kind defn
+    tcDataDefn (tcMkDeclCtxt decl) roles_info tc_name defn
 
 tcTyClDecl1 _parent roles_info
             (ClassDecl { tcdLName = L _ class_name
@@ -1884,10 +2090,10 @@ tcClassATs class_name cls ats at_defs
        ; mapM tc_at ats }
   where
     at_def_tycon :: LTyFamDefltDecl GhcRn -> Name
-    at_def_tycon (L _ eqn) = tyFamInstDeclName eqn
+    at_def_tycon = tyFamInstDeclName . unLoc
 
     at_fam_name :: LFamilyDecl GhcRn -> Name
-    at_fam_name (L _ decl) = unLoc (fdLName decl)
+    at_fam_name = familyDeclName . unLoc
 
     at_names = mkNameSet (map at_fam_name ats)
 
@@ -2226,12 +2432,11 @@ tcInjectivity tcbs (Just (L loc (InjectivityAnn _ lInjNames)))
                                        , ppr inj_ktvs, ppr inj_bools ])
        ; return $ Injective inj_bools }
 
-tcTySynRhs :: RolesInfo
-           -> Name
-           -> [TyConBinder] -> Kind
+tcTySynRhs :: RolesInfo -> Name
            -> LHsType GhcRn -> TcM TyCon
-tcTySynRhs roles_info tc_name binders res_kind hs_ty
-  = do { env <- getLclEnv
+tcTySynRhs roles_info tc_name hs_ty
+  = bindTyClTyVars tc_name $ \ binders res_kind ->
+    do { env <- getLclEnv
        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
        ; rhs_ty <- pushTcLevelM_   $
                    solveEqualities $
@@ -2241,27 +2446,29 @@ tcTySynRhs roles_info tc_name binders res_kind hs_ty
              tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
        ; return tycon }
 
-tcDataDefn :: SDoc
-           -> RolesInfo -> Name
-           -> [TyConBinder] -> Kind
+tcDataDefn :: SDoc -> RolesInfo -> Name
            -> HsDataDefn GhcRn -> TcM (TyCon, [DerivInfo])
   -- NB: not used for newtype/data instances (whether associated or not)
-tcDataDefn err_ctxt
-           roles_info
-           tc_name tycon_binders res_kind
+tcDataDefn err_ctxt roles_info tc_name
            (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                        , dd_ctxt = ctxt
                        , dd_kindSig = mb_ksig  -- Already in tc's kind
                                                -- via inferInitialKinds
                        , dd_cons = cons
                        , dd_derivs = derivs })
- =  do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons
+  = bindTyClTyVars tc_name $ \ tycon_binders res_kind ->
+       -- The TyCon tyvars must scope over
+       --    - the stupid theta (dd_ctxt)
+       --    - for H98 constructors only, the ConDecl
+       -- But it does no harm to bring them into scope
+       -- over GADT ConDecls as well; and it's awkward not to
+    do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons
+       ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind
 
        ; tcg_env <- getGblEnv
-       ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind
        ; let hsc_src = tcg_src tcg_env
        ; unless (mk_permissive_kind hsc_src cons) $
-           checkDataKindSig (DataDeclSort new_or_data) final_res_kind
+         checkDataKindSig (DataDeclSort new_or_data) final_res_kind
 
        ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt
        ; stupid_theta    <- zonkTcTypesToTypes stupid_tc_theta
@@ -2326,7 +2533,7 @@ tcDataDefn err_ctxt
           DataType -> return (mkDataTyConRhs data_cons)
           NewType  -> ASSERT( not (null data_cons) )
                       mkNewTyConRhs tc_name tycon (head data_cons)
-tcDataDefn _ _ _ _ _ (XHsDataDefn nec) = noExtCon nec
+tcDataDefn _ _ _ (XHsDataDefn nec) = noExtCon nec
 
 
 -------------------------
@@ -2382,7 +2589,13 @@ tcTyFamInstEqn fam_tc mb_clsinfo
                                       , feqn_rhs    = hs_rhs_ty }}))
   = ASSERT( getName fam_tc == eqn_tc_name )
     setSrcSpan loc $
-    do {
+    do { traceTc "tcTyFamInstEqn" $
+         vcat [ ppr fam_tc <+> ppr hs_pats
+              , text "fam tc bndrs" <+> pprTyVars (tyConTyVars fam_tc)
+              , case mb_clsinfo of
+                  NotAssociated -> empty
+                  InClsInst { ai_class = cls } -> text "class" <+> ppr cls <+> pprTyVars (classTyVars cls) ]
+
        -- First, check the arity of visible arguments
        -- If we wait until validity checking, we'll get kind errors
        -- below when an arity error will be much easier to understand.
@@ -2466,7 +2679,7 @@ tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
                    -> TcM ([TyVar], [TcType], TcType)      -- (tyvars, pats, rhs)
 -- Used only for type families, not data families
 tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
-  = do { traceTc "tcTyFamInstEqnGuts {" (vcat [ ppr fam_tc <+> ppr hs_pats ])
+  = do { traceTc "tcTyFamInstEqnGuts {" (ppr fam_tc)
 
        -- By now, for type families (but not data families) we should
        -- have checked that the number of patterns matches tyConArity
@@ -2495,6 +2708,13 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
        ; dvs  <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
        ; qtvs <- quantifyTyVars dvs
 
+       ; traceTc "tcTyFamInstEqnGuts 2" $
+         vcat [ ppr fam_tc
+              , text "scoped_tvs" <+> pprTyVars scoped_tvs
+              , text "lhs_ty"     <+> ppr lhs_ty
+              , text "dvs"        <+> ppr dvs
+              , text "qtvs"       <+> pprTyVars qtvs ]
+
        ; (ze, qtvs) <- zonkTyBndrs qtvs
        ; lhs_ty     <- zonkTcTypeToTypeX ze lhs_ty
        ; rhs_ty     <- zonkTcTypeToTypeX ze rhs_ty
@@ -2817,7 +3037,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
                  ; return (ctxt, final_arg_tys, res_ty, field_lbls, stricts)
                  }
        ; imp_tvs <- zonkAndScopedSort imp_tvs
-       ; let user_tvs      = imp_tvs ++ exp_tvs
+       ; let user_tvs = imp_tvs ++ exp_tvs
 
        ; tkvs <- kindGeneralizeAll (mkSpecForAllTys user_tvs $
                                     mkPhiTy ctxt $
diff --git a/testsuite/tests/polykinds/T11203.stderr b/testsuite/tests/polykinds/T11203.stderr
index f5c7213..e6f30c0 100644
--- a/testsuite/tests/polykinds/T11203.stderr
+++ b/testsuite/tests/polykinds/T11203.stderr
@@ -1,4 +1,4 @@
 
 T11203.hs:7:24: error:
-    • Couldn't match ‘k1’ with ‘k2’
-    • In the data type declaration for ‘Q’
+    • Different names for the same type variable: ‘k1’ and ‘k2’
+    • In the data declaration for ‘Q’
diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr
index f55c703..50d58df 100644
--- a/testsuite/tests/polykinds/T11821a.stderr
+++ b/testsuite/tests/polykinds/T11821a.stderr
@@ -1,4 +1,4 @@
 
 T11821a.hs:4:31: error:
-    • Couldn't match ‘k1’ with ‘k2’
-    • In the type synonym declaration for ‘SameKind’
+    • Different names for the same type variable: ‘k1’ and ‘k2’
+    • In the type declaration for ‘SameKind’
diff --git a/testsuite/tests/typecheck/should_compile/Makefile b/testsuite/tests/typecheck/should_compile/Makefile
index 5255485..5c0c84f 100644
--- a/testsuite/tests/typecheck/should_compile/Makefile
+++ b/testsuite/tests/typecheck/should_compile/Makefile
@@ -75,3 +75,8 @@ T14934:
 	$(RM) -f T14934a.o T14934a.hi T14934.o T14934.hi
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T14934a.hs -O
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T14934.hs  -O
+
+T17566:
+	$(RM) -f T17566a.o T17566a.hi T17566.o T17566.hi
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c T17566a.hs
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c T17566.hs
diff --git a/testsuite/tests/typecheck/should_compile/T17566.hs b/testsuite/tests/typecheck/should_compile/T17566.hs
new file mode 100644
index 0000000..5996bd7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17566.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T17566 where
+
+import Data.Kind
+import Data.Proxy
+import T17566a
+
+type family F1 (x :: Proxy a) :: Proxy a
+instance C1 Proxy z where
+  type T1 x = F1 x
+  data D1 x
+
+type family F2 (x :: Proxy a) :: Proxy a
+instance C2 Proxy z where
+  type T2 x = F2 x
+  data D2 x
diff --git a/testsuite/tests/typecheck/should_compile/T17566a.hs b/testsuite/tests/typecheck/should_compile/T17566a.hs
new file mode 100644
index 0000000..6255a7a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17566a.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T17566a where
+
+import Data.Kind
+
+class C1 (f :: k -> Type) z where
+  type T1 (x :: f a) :: f a
+  data D1 (x :: f a)
+
+class C2 f z where
+  type T2 (x :: f a) :: f a
+  data D2 (x :: f a)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 80b11ca..0f61b57 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -692,3 +692,4 @@ test('T17202', expect_broken(17202), compile, [''])
 test('T15839a', normal, compile, [''])
 test('T15839b', normal, compile, [''])
 test('T17343', exit_code(1), compile_and_run, [''])
+test('T17566', [extra_files(['T17566a.hs'])], makefile_test, [])
diff --git a/testsuite/tests/typecheck/should_fail/T17566b.hs b/testsuite/tests/typecheck/should_fail/T17566b.hs
new file mode 100644
index 0000000..7b1711a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17566b.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T17566b where
+
+class C f where
+  type T1 (f :: k1)
+  type T2 (f :: k2)
diff --git a/testsuite/tests/typecheck/should_fail/T17566b.stderr b/testsuite/tests/typecheck/should_fail/T17566b.stderr
new file mode 100644
index 0000000..be3c0e1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17566b.stderr
@@ -0,0 +1,4 @@
+
+T17566b.hs:7:17: error:
+    • Different names for the same type variable: ‘k1’ and ‘k2’
+    • In the class declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/T17566c.hs b/testsuite/tests/typecheck/should_fail/T17566c.hs
new file mode 100644
index 0000000..d7d68a0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17566c.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T17566c where
+
+import Data.Kind
+
+class C2 f z where
+  type T2 (f :: k -> Type)
+  data D2 (x :: (f :: k -> Type) a)
diff --git a/testsuite/tests/typecheck/should_fail/T17566c.stderr b/testsuite/tests/typecheck/should_fail/T17566c.stderr
new file mode 100644
index 0000000..df5e5c0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17566c.stderr
@@ -0,0 +1,6 @@
+
+T17566c.hs:11:23: error:
+    • Different names for the same type variable:
+        ‘k’ bound at T17566c.hs:10:17
+        ‘k’ bound at T17566c.hs:11:23
+    • In the class declaration for ‘C2’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index e11c239..f0f290c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -550,3 +550,5 @@ test('T17355', normal, compile_fail, [''])
 test('T17360', normal, compile_fail, [''])
 test('T17563', normal, compile_fail, [''])
 test('T16946', normal, compile_fail, [''])
+test('T17566b', normal, compile_fail, [''])
+test('T17566c', normal, compile_fail, [''])
diff --git a/utils/haddock b/utils/haddock
-Subproject 4808003d2238f76aee96d22cc022cee3e049f6a
+Subproject f3e3c4a766805a1bbea75bf23b84fdaaf053c22