Implicitly bind kind variables in type family instance RHSes when it's sensible

Summary:
Before, there was a discrepancy in how GHC renamed type synonyms as
opposed to type family instances. That is, GHC would accept definitions like
this one:

```lang=haskell
type T = (Nothing :: Maybe a)
```

However, it would not accept a very similar type family instance:

```lang=haskell
type family   T :: Maybe a
type instance T = (Nothing :: Maybe a)
```

The primary goal of this patch is to bring the renaming of type family
instances up to par with that of type synonyms, causing the latter definition
to be accepted, and fixing #14131.

In particular, we now allow kind variables on the right-hand sides of type
(and data) family instances to be //implicitly// bound by LHS type (or kind)
patterns (as opposed to type variables, which must always be explicitly
bound by LHS type patterns only). As a consequence, this allows programs
reported in #7938 and #9574 to typecheck, whereas before they would
have been rejected.

Implementation-wise, there isn't much trickery involved in making this happen.
We simply need to bind additional kind variables from the RHS of a type family
in the right place (in particular, see `RnSource.rnFamInstEqn`, which has
undergone a minor facelift).

While doing this has the upside of fixing #14131, it also made it easier to
trigger #13985, so I decided to fix that while I was in town. This was
accomplished by a careful blast of `reportFloatingKvs` in `tcFamTyPats`.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie

GHC Trac Issues: #13985, #14131

Differential Revision: https://phabricator.haskell.org/D3872

16 files changed, 542 insertions, 107 deletions

diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index cb9c960dce..0e11ece40e 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -54,7 +54,7 @@ import Maybes           ( orElse )
 import FastString
 import SrcLoc
 import DynFlags
-import Util             ( debugIsOn, lengthExceeds, partitionWith )
+import Util             ( debugIsOn, filterOut, lengthExceeds, partitionWith )
 import HscTypes         ( HscEnv, hsc_dflags )
 import ListSetOps       ( findDupsEq, removeDups, equivClasses )
 import Digraph          ( SCC, flattenSCC, flattenSCCs, Node(..)
@@ -720,14 +720,15 @@ rnFamInstEqn :: HsDocContext
                                      -- Just (cls,tvs) => associated,
                                      --   and gives class and tyvars of the
                                      --   parent instance delc
+             -> [Located RdrName]    -- Kind variables from the equation's RHS
              -> FamInstEqn GhcPs rhs
              -> (HsDocContext -> rhs -> RnM (rhs', FreeVars))
              -> RnM (FamInstEqn GhcRn rhs', FreeVars)
-rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
-                                                   , feqn_pats   = pats
-                                                   , feqn_fixity = fixity
-                                                   , feqn_rhs    = payload }})
-            rnPayload
+rnFamInstEqn doc mb_cls rhs_kvars
+    (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
+                               , feqn_pats   = pats
+                               , feqn_fixity = fixity
+                               , feqn_rhs    = payload }}) rn_payload
   = do { tycon'   <- lookupFamInstName (fmap fst mb_cls) tycon
        ; let loc = case pats of
                      []             -> pprPanic "rnFamInstEqn" (ppr tycon)
@@ -735,18 +736,25 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
                      (L loc _ : ps) -> combineSrcSpans loc (getLoc (last ps))
 
        ; pat_kity_vars_with_dups <- extractHsTysRdrTyVarsDups pats
+       ; let pat_vars = freeKiTyVarsAllVars $
+                        rmDupsInRdrTyVars pat_kity_vars_with_dups
              -- Use the "...Dups" form because it's needed
              -- below to report unsed binder on the LHS
-       ; var_names <- mapM (newTyVarNameRn mb_cls . L loc . unLoc) $
-                      freeKiTyVarsAllVars $
-                      rmDupsInRdrTyVars pat_kity_vars_with_dups
+       ; pat_var_names <- mapM (newTyVarNameRn mb_cls . L loc . unLoc) pat_vars
+
+             -- Make sure to filter out the kind variables that were explicitly
+             -- bound in the type patterns.
+       ; let payload_vars = filterOut (`elemRdr` pat_vars) rhs_kvars
+       ; payload_var_names <- mapM (newTyVarNameRn mb_cls) payload_vars
+
+       ; let all_var_names = pat_var_names ++ payload_var_names
 
              -- All the free vars of the family patterns
              -- with a sensible binding location
        ; ((pats', payload'), fvs)
-              <- bindLocalNamesFV var_names $
+              <- bindLocalNamesFV all_var_names $
                  do { (pats', pat_fvs) <- rnLHsTypes (FamPatCtx tycon) pats
-                    ; (payload', rhs_fvs) <- rnPayload doc payload
+                    ; (payload', rhs_fvs) <- rn_payload doc payload
 
                        -- Report unused binders on the LHS
                        -- See Note [Unused type variables in family instances]
@@ -766,13 +774,13 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
                           inst_tvs = case mb_cls of
                                        Nothing            -> []
                                        Just (_, inst_tvs) -> inst_tvs
-                    ; warnUnusedTypePatterns var_names tv_nms_used
+                    ; warnUnusedTypePatterns pat_var_names tv_nms_used
 
                          -- See Note [Renaming associated types]
                     ; let bad_tvs = case mb_cls of
                                       Nothing           -> []
                                       Just (_,cls_tkvs) -> filter is_bad cls_tkvs
-                          var_name_set = mkNameSet var_names
+                          var_name_set = mkNameSet all_var_names
 
                           is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs
                                         && not (cls_tkv `elemNameSet` var_name_set)
@@ -781,12 +789,13 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
                     ; return ((pats', payload'), rhs_fvs `plusFV` pat_fvs) }
 
        ; let anon_wcs = concatMap collectAnonWildCards pats'
-             all_ibs  = anon_wcs ++ var_names
+             all_ibs  = anon_wcs ++ all_var_names
                         -- all_ibs: include anonymous wildcards in the implicit
                         -- binders In a type pattern they behave just like any
                         -- other type variable except for being anoymous.  See
                         -- Note [Wildcards in family instances]
              all_fvs  = fvs `addOneFV` unLoc tycon'
+                        -- type instance => use, hence addOneFV
 
        ; return (HsIB { hsib_vars = all_ibs
                       , hsib_closed = True
@@ -796,7 +805,6 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
                                    , feqn_fixity = fixity
                                    , feqn_rhs    = payload' } },
                  all_fvs) }
-             -- type instance => use, hence addOneFV
 
 rnTyFamInstDecl :: Maybe (Name, [Name])
                 -> TyFamInstDecl GhcPs
@@ -808,8 +816,10 @@ rnTyFamInstDecl mb_cls (TyFamInstDecl { tfid_eqn = eqn })
 rnTyFamInstEqn :: Maybe (Name, [Name])
                -> TyFamInstEqn GhcPs
                -> RnM (TyFamInstEqn GhcRn, FreeVars)
-rnTyFamInstEqn mb_cls eqn@(HsIB { hsib_body = FamEqn { feqn_tycon  = tycon }})
-  = rnFamInstEqn (TySynCtx tycon) mb_cls eqn rnTySyn
+rnTyFamInstEqn mb_cls eqn@(HsIB { hsib_body = FamEqn { feqn_tycon = tycon
+                                                     , feqn_rhs   = rhs }})
+  = do { rhs_kvs <- extractHsTyRdrTyVarsKindVars rhs
+       ; rnFamInstEqn (TySynCtx tycon) mb_cls rhs_kvs eqn rnTySyn }
 
 rnTyFamDefltEqn :: Name
                 -> TyFamDefltEqn GhcPs
@@ -818,13 +828,14 @@ rnTyFamDefltEqn cls (FamEqn { feqn_tycon  = tycon
                             , feqn_pats   = tyvars
                             , feqn_fixity = fixity
                             , feqn_rhs    = rhs })
-  = bindHsQTyVars ctx Nothing (Just cls) [] tyvars $ \ tyvars' _ ->
+  = do { kvs <- extractHsTyRdrTyVarsKindVars rhs
+       ; bindHsQTyVars ctx Nothing (Just cls) kvs tyvars $ \ tyvars' _ ->
     do { tycon'      <- lookupFamInstName (Just cls) tycon
        ; (rhs', fvs) <- rnLHsType ctx rhs
        ; return (FamEqn { feqn_tycon  = tycon'
                         , feqn_pats   = tyvars'
                         , feqn_fixity = fixity
-                        , feqn_rhs    = rhs' }, fvs) }
+                        , feqn_rhs    = rhs' }, fvs) } }
   where
     ctx = TyFamilyCtx tycon
 
@@ -832,9 +843,11 @@ rnDataFamInstDecl :: Maybe (Name, [Name])
                   -> DataFamInstDecl GhcPs
                   -> RnM (DataFamInstDecl GhcRn, FreeVars)
 rnDataFamInstDecl mb_cls (DataFamInstDecl { dfid_eqn = eqn@(HsIB { hsib_body =
-                           FamEqn { feqn_tycon  = tycon }})})
-  = do { (eqn', fvs) <-
-           rnFamInstEqn (TyDataCtx tycon) mb_cls eqn rnDataDefn
+                           FamEqn { feqn_tycon = tycon
+                                  , feqn_rhs   = rhs }})})
+  = do { rhs_kvs <- extractDataDefnKindVars rhs
+       ; (eqn', fvs) <-
+           rnFamInstEqn (TyDataCtx tycon) mb_cls rhs_kvs eqn rnDataDefn
        ; return (DataFamInstDecl { dfid_eqn = eqn' }, fvs) }
 
 -- Renaming of the associated types in instances.
@@ -914,7 +927,7 @@ Relevant tickets: #3699, #10586, #10982 and #11451.
 
 Note [Renaming associated types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Check that the RHS of the decl mentions only type variables
+Check that the RHS of the decl mentions only type variables that are explicitly
 bound on the LHS.  For example, this is not ok
    class C a b where
       type F a x :: *
@@ -922,13 +935,26 @@ bound on the LHS.  For example, this is not ok
       type F (p,q) x = (x, r)   -- BAD: mentions 'r'
 c.f. Trac #5515
 
-The same thing applies to kind variables, of course (Trac #7938, #9574):
+Kind variables, on the other hand, are allowed to be implicitly or explicitly
+bound. As examples, this (#9574) is acceptable:
    class Funct f where
       type Codomain f :: *
    instance Funct ('KProxy :: KProxy o) where
+      -- o is implicitly bound by the kind signature
+      -- of the LHS type pattern ('KProxy)
       type Codomain 'KProxy = NatTr (Proxy :: o -> *)
-Here 'o' is mentioned on the RHS of the Codomain function, but
-not on the LHS.
+And this (#14131) is also acceptable:
+    data family Nat :: k -> k -> *
+    -- k is implicitly bound by an invisible kind pattern
+    newtype instance Nat :: (k -> *) -> (k -> *) -> * where
+      Nat :: (forall xx. f xx -> g xx) -> Nat f g
+We could choose to disallow this, but then associated type families would not
+be able to be as expressive as top-level type synonyms. For example, this type
+synonym definition is allowed:
+    type T = (Nothing :: Maybe a)
+So for parity with type synonyms, we also allow:
+    type family   T :: Maybe a
+    type instance T = (Nothing :: Maybe a)
 
 All this applies only for *instance* declarations.  In *class*
 declarations there is no RHS to worry about, and the class variables
@@ -1643,7 +1669,7 @@ rnTyClDecl (FamDecl { tcdFam = decl })
 rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars,
                       tcdFixity = fixity, tcdRhs = rhs })
   = do { tycon' <- lookupLocatedTopBndrRn tycon
-       ; kvs <- freeKiTyVarsKindVars <$> extractHsTyRdrTyVars rhs
+       ; kvs <- extractHsTyRdrTyVarsKindVars rhs
        ; let doc = TySynCtx tycon
        ; traceRn "rntycl-ty" (ppr tycon <+> ppr kvs)
        ; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' _ ->
@@ -1993,6 +2019,7 @@ are no data constructors we allow h98_style = True
 badAssocRhs :: [Name] -> RnM ()
 badAssocRhs ns
   = addErr (hang (text "The RHS of an associated type declaration mentions"
+                  <+> text "out-of-scope variable" <> plural ns
                   <+> pprWithCommas (quotes . ppr) ns)
                2 (text "All such variables must be bound on the LHS"))
 
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 40b52399f1..a1174f65ca 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -26,10 +26,12 @@ module RnTypes (
         bindLHsTyVarBndr,
         bindSigTyVarsFV, bindHsQTyVars, bindLRdrNames,
         extractFilteredRdrTyVars, extractFilteredRdrTyVarsDups,
-        extractHsTyRdrTyVars, extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars,
+        extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars,
+        extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars,
         extractHsTysRdrTyVarsDups, rmDupsInRdrTyVars,
         extractRdrKindSigVars, extractDataDefnKindVars,
-        freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars
+        freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars,
+        elemRdr
   ) where
 
 import {-# SOURCE #-} RnSplice( rnSpliceType )
@@ -1661,6 +1663,15 @@ extractHsTyRdrTyVarsDups :: LHsType GhcPs -> RnM FreeKiTyVarsWithDups
 extractHsTyRdrTyVarsDups ty
   = extract_lty TypeLevel ty emptyFKTV
 
+-- | Extracts the free kind variables (but not the type variables) of an
+-- 'HsType'. Does not return any wildcards.
+-- When the same name occurs multiple times in the type, only the first
+-- occurrence is returned.
+-- See Note [Kind and type-variable binders]
+extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> RnM [Located RdrName]
+extractHsTyRdrTyVarsKindVars ty
+  = freeKiTyVarsKindVars <$> extractHsTyRdrTyVars ty
+
 -- | Extracts free type and kind variables from types in a list.
 -- When the same name occurs multiple times in the types, only the first
 -- occurrence is returned and the rest is filtered out.
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index dab708c290..bd73bf3884 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -38,6 +38,8 @@ module TcHsType (
 
         kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
 
+        reportFloatingKvs,
+
         -- Sort-checking kinds
         tcLHsKindSig,
 
@@ -1744,6 +1746,46 @@ CUSK: When we determine the tycon's final, never-to-be-changed kind
 in kcHsTyVarBndrs, we check to make sure all implicitly-bound kind
 vars are indeed mentioned in a kind somewhere. If not, error.
 
+We also perform free-floating kind var analysis for type family instances
+(see #13985). Here is an interesting example:
+
+    type family   T :: k
+    type instance T = (Nothing :: Maybe a)
+
+Upon a cursory glance, it may appear that the kind variable `a` is
+free-floating above, since there are no (visible) LHS patterns in `T`. However,
+there is an *invisible* pattern due to the return kind, so inside of GHC, the
+instance looks closer to this:
+
+    type family T @k :: k
+    type instance T @(Maybe a) = (Nothing :: Maybe a)
+
+Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
+fact not free-floating. Contrast that with this example:
+
+    type instance T = Proxy (Nothing :: Maybe a)
+
+This would looks like this inside of GHC:
+
+    type instance T @(*) = Proxy (Nothing :: Maybe a)
+
+So this time, `a` is neither bound by a visible nor invisible type pattern on
+the LHS, so it would be reported as free-floating.
+
+Finally, here's one more brain-teaser (from #9574). In the example below:
+
+    class Funct f where
+      type Codomain f :: *
+    instance Funct ('KProxy :: KProxy o) where
+      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
+
+As it turns out, `o` is not free-floating in this example. That is because `o`
+bound by the kind signature of the LHS type pattern 'KProxy. To make this more
+obvious, one can also write the instance like so:
+
+    instance Funct ('KProxy :: KProxy o) where
+      type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
+
 -}
 
 --------------------
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index f445d83608..44492c08d9 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1380,7 +1380,9 @@ tc_fam_ty_pats :: FamTyConShape
                -> [Name]              -- Bound kind/type variable names
                -> HsTyPats GhcRn      -- Type patterns
                -> (TcKind -> TcM r)   -- Kind checker for RHS
-               -> TcM ([Type], r)     -- Returns the type-checked patterns
+               -> TcM ( [TcTyVar]     -- Returns the type-checked patterns,
+                      , [TcType]      -- the type variables that scope over
+                      , r )           -- them, and the thing inside
 -- Check the type patterns of a type or data family instance
 --     type instance F <pat1> <pat2> = <type>
 -- The 'tyvars' are the free type variables of pats
@@ -1413,7 +1415,7 @@ tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity
 
          -- Kind-check and quantify
          -- See Note [Quantifying over family patterns]
-       ; (_, result) <- tcImplicitTKBndrs tv_names $
+       ; (arg_tvs, (args, stuff)) <- tcImplicitTKBndrs tv_names $
          do { let loc          = nameSrcSpan name
                   lhs_fun      = L loc (HsTyVar NotPromoted (L loc name))
                   bogus_fun_ty = pprPanic "tc_fam_ty_pats" (ppr name $$ ppr arg_pats)
@@ -1428,7 +1430,7 @@ tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity
 
             ; return ((args, stuff), emptyVarSet) }
 
-       ; return result }
+       ; return (arg_tvs, args, stuff) }
 
 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
 tcFamTyPats :: FamTyConShape
@@ -1443,9 +1445,9 @@ tcFamTyPats :: FamTyConShape
                 -> TcKind
                 -> TcM a)            -- NB: You can use solveEqualities here.
             -> TcM a
-tcFamTyPats fam_shape@(FamTyConShape { fs_name = name }) mb_clsinfo
-            tv_names arg_pats kind_checker thing_inside
-  = do { (typats, (more_typats, res_kind))
+tcFamTyPats fam_shape@(FamTyConShape { fs_name = name, fs_flavor = fam_flav })
+            mb_clsinfo tv_names arg_pats kind_checker thing_inside
+  = do { (fam_used_tvs, typats, (more_typats, res_kind))
             <- solveEqualities $  -- See Note [Constraints in patterns]
                tc_fam_ty_pats fam_shape mb_clsinfo
                               tv_names arg_pats kind_checker
@@ -1481,7 +1483,21 @@ tcFamTyPats fam_shape@(FamTyConShape { fs_name = name }) mb_clsinfo
            -- bit is cleverer.
 
        ; traceTc "tcFamTyPats" (ppr name $$ ppr all_pats $$ ppr qtkvs)
-            -- Don't print out too much, as we might be in the knot
+           -- Don't print out too much, as we might be in the knot
+
+           -- See Note [Free-floating kind vars] in TcHsType
+       ; let tc_flav = case fam_flav of
+                         TypeFam -> OpenTypeFamilyFlavour
+                         DataFam -> DataFamilyFlavour
+             all_mentioned_tvs = mkVarSet qtkvs
+                                   -- qtkvs has all the tyvars bound by LHS
+                                   -- type patterns
+             unmentioned_tvs   = filterOut (`elemVarSet` all_mentioned_tvs)
+                                           fam_used_tvs
+                                   -- If there are tyvars left over, we can
+                                   -- assume they're free-floating, since they
+                                   -- aren't bound by a type pattern
+       ; checkNoErrs $ reportFloatingKvs name tc_flav qtkvs unmentioned_tvs
 
        ; tcExtendTyVarEnv qtkvs $
             -- Extend envt with TcTyVars not TyVars, because the
diff --git a/docs/users_guide/8.4.1-notes.rst b/docs/users_guide/8.4.1-notes.rst
index 96fbdd4886..db573202e2 100644
--- a/docs/users_guide/8.4.1-notes.rst
+++ b/docs/users_guide/8.4.1-notes.rst
@@ -27,6 +27,24 @@ Language
   wish to; this is quite like how regular datatypes with a kind signature can omit
   some type variables.
 
+- There are now fewer restrictions regarding whether kind variables can appear
+  on the right-hand sides of type and data family instances. Before, there was
+  a strict requirements that all kind variables on the RHS had to be explicitly
+  bound by type patterns on the LHS. Now, kind variables can be *implicitly*
+  bound, which allows constructions like these: ::
+
+    data family Nat :: k -> k -> *
+    -- k is implicitly bound by an invisible kind pattern
+    newtype instance Nat :: (k -> *) -> (k -> *) -> * where
+      Nat :: (forall xx. f xx -> g xx) -> Nat f g
+
+    class Funct f where
+      type Codomain f :: *
+    instance Funct ('KProxy :: KProxy o) where
+      -- o is implicitly bound by the kind signature
+      -- of the LHS type pattern ('KProxy)
+      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
+
 - Implicitly bidirectional pattern synonyms no longer allow bang patterns
   (``!``) or irrefutable patterns (``~``) on the right-hand side. Previously,
   this was allowed, although the bang patterns and irrefutable patterns would
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index bd11360acc..65f8629ccf 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -7659,8 +7659,23 @@ Note the following points:
    instance declarations of the class in which the family was declared,
    just as with the equations of the methods of a class.
 
--  The variables on the right hand side of the type family equation
-   must, as usual, be bound on the left hand side.
+-  The type variables on the right hand side of the type family equation
+   must, as usual, be explicitly bound by the left hand side. This restriction
+   is relaxed for *kind* variables, however, as the right hand side is allowed
+   to mention kind variables that are implicitly bound. For example, these are
+   legitimate: ::
+
+    data family Nat :: k -> k -> *
+    -- k is implicitly bound by an invisible kind pattern
+    newtype instance Nat :: (k -> *) -> (k -> *) -> * where
+      Nat :: (forall xx. f xx -> g xx) -> Nat f g
+
+    class Funct f where
+      type Codomain f :: *
+    instance Funct ('KProxy :: KProxy o) where
+      -- o is implicitly bound by the kind signature
+      -- of the LHS type pattern ('KProxy)
+      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
 
 -  The instance for an associated type can be omitted in class
    instances. In that case, unless there is a default instance (see
@@ -7715,15 +7730,18 @@ Note the following points:
 
 -  The default declaration must mention only type *variables* on the
    left hand side, and the right hand side must mention only type
-   variables bound on the left hand side. However, unlike the associated
-   type family declaration itself, the type variables of the default
-   instance are independent of those of the parent class.
+   variables that are explicitly bound on the left hand side. This restriction
+   is relaxed for *kind* variables, however, as the right hand side is allowed
+   to mention kind variables that are implicitly bound on the left hand side.
+
+-  Unlike the associated type family declaration itself, the type variables of
+   the default instance are independent of those of the parent class.
 
 Here are some examples:
 
 ::
 
-      class C a where
+      class C (a :: *) where
         type F1 a :: *
         type instance F1 a = [a]     -- OK
         type instance F1 a = a->a    -- BAD; only one default instance is allowed
@@ -7738,6 +7756,21 @@ Here are some examples:
         type F4 a
         type F4 b = a                -- BAD; 'a' is not in scope  in the RHS
 
+        type F5 a :: [k]
+        type F5 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
+                                            bound by an invisible kind pattern
+                                            on the LHS
+
+        type F6 a
+        type F6 a =
+          Proxy ('[] :: [x])         -- BAD; the kind variable x is not bound,
+                                             even by an invisible kind pattern
+
+        type F7 (x :: a) :: [a]
+        type F7 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
+                                            bound by the kind signature of the
+                                            LHS type pattern
+
 .. _scoping-class-params:
 
 Scoping of class parameters
@@ -7760,6 +7793,33 @@ Here, the right-hand side of the data instance mentions the type
 variable ``d`` that does not occur in its left-hand side. We cannot
 admit such data instances as they would compromise type safety.
 
+Bear in mind that it is also possible for the *right*-hand side of an
+associated family instance to contain *kind* parameters (by using the
+:ghc-flag:`-XPolyKinds` extension). For instance, this class and instance are
+perfectly admissible: ::
+
+    class C k where
+      type T :: k
+
+    instance C (Maybe a) where
+      type T = (Nothing :: Maybe a)
+
+Here, although the right-hand side ``(Nothing :: Maybe a)`` mentions a kind
+variable ``a`` which does not occur on the left-hand side, this is acceptable,
+because ``a`` is *implicitly* bound by ``T``'s kind pattern.
+
+A kind variable can also be bound implicitly in a LHS type pattern, as in this
+example: ::
+
+    class C a where
+      type T (x :: a) :: [a]
+
+    instance C (Maybe a) where
+      type T x = ('[] :: [Maybe a])
+
+In ``('[] :: [Maybe a])``, the kind variable ``a`` is implicitly bound by the
+kind signature of the LHS type pattern ``x``.
+
 Instance contexts and associated type and data instances
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/testsuite/tests/indexed-types/should_compile/T14131.hs b/testsuite/tests/indexed-types/should_compile/T14131.hs
new file mode 100644
index 0000000000..e8b15790a1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T14131.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module T14131 where
+
+import Data.Kind
+import Data.Proxy
+
+data family Nat :: k -> k -> *
+newtype instance Nat :: (k -> *) -> (k -> *) -> * where
+  Nat :: (forall xx. f xx -> g xx) -> Nat f g
+
+type family   F :: Maybe a
+type instance F = (Nothing :: Maybe a)
+
+class C k where
+  data CD :: k -> k -> *
+  type CT :: k
+
+instance C (Maybe a) where
+  data CD :: Maybe a -> Maybe a -> * where
+    CD :: forall (m :: Maybe a) (n :: Maybe a). Proxy m -> Proxy n -> CD m n
+  type CT = (Nothing :: Maybe a)
+
+class Z k where
+  type ZT :: Maybe k
+  type ZT = (Nothing :: Maybe k)
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index dc166dc470..ad80b0cec2 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -267,3 +267,4 @@ test('T13662', normal, compile, [''])
 test('T13705', normal, compile, [''])
 test('T12369', normal, compile, [''])
 test('T14045', normal, compile, [''])
+test('T14131', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T5515.stderr b/testsuite/tests/indexed-types/should_fail/T5515.stderr
index 25fbe9f0f0..688eef697e 100644
--- a/testsuite/tests/indexed-types/should_fail/T5515.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5515.stderr
@@ -1,8 +1,8 @@
 
-T5515.hs:9:3:
-    The RHS of an associated type declaration mentions ‘a’
+T5515.hs:9:3: error:
+    The RHS of an associated type declaration mentions out-of-scope variable ‘a’
       All such variables must be bound on the LHS
 
-T5515.hs:15:3:
-    The RHS of an associated type declaration mentions ‘a’
+T5515.hs:15:3: error:
+    The RHS of an associated type declaration mentions out-of-scope variable ‘a’
       All such variables must be bound on the LHS
diff --git a/testsuite/tests/indexed-types/should_fail/T7938.stderr b/testsuite/tests/indexed-types/should_fail/T7938.stderr
index a9b5aef499..2816e2f9f8 100644
--- a/testsuite/tests/indexed-types/should_fail/T7938.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7938.stderr
@@ -1,4 +1,6 @@
 
-T7938.hs:12:3:
-    The RHS of an associated type declaration mentions ‘k2’
-      All such variables must be bound on the LHS
+T7938.hs:12:16: error:
+    • Expected a type, but ‘(KP :: KProxy k2)’ has kind ‘KProxy k2’
+    • In the type ‘(KP :: KProxy k2)’
+      In the type instance declaration for ‘Bar’
+      In the instance declaration for ‘Foo (a :: k1) (b :: k2)’
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs
index cb23ad5085..493b736df5 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
+{-# LANGUAGE DataKinds, GADTs, PolyKinds, RankNTypes, TypeOperators,
+             TypeFamilies #-}
 
 module DumpRenamedAst where
 
@@ -8,4 +9,10 @@ type family Length (as :: [k]) :: Peano where
   Length (a : as) = Succ (Length as)
   Length '[]      = Zero
 
+data family Nat :: k -> k -> *
+-- Ensure that the `k` in the type pattern and `k` in the kind signature have
+-- the same binding site.
+newtype instance Nat (a :: k -> *) :: (k -> *) -> * where
+  Nat :: (forall xx. f xx -> g xx) -> Nat f g
+
 main = putStrLn "hello"
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index 6ea6e8f2e0..60862cc110 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -6,32 +6,32 @@
   [((,)
     (NonRecursive)
     {Bag(Located (HsBind Name)):
-     [({ DumpRenamedAst.hs:11:1-23 }
+     [({ DumpRenamedAst.hs:18:1-23 }
        (FunBind
-        ({ DumpRenamedAst.hs:11:1-4 }
+        ({ DumpRenamedAst.hs:18:1-4 }
          {Name: DumpRenamedAst.main})
         (MG
-         ({ DumpRenamedAst.hs:11:1-23 }
-          [({ DumpRenamedAst.hs:11:1-23 }
+         ({ DumpRenamedAst.hs:18:1-23 }
+          [({ DumpRenamedAst.hs:18:1-23 }
             (Match
              (FunRhs
-              ({ DumpRenamedAst.hs:11:1-4 }
+              ({ DumpRenamedAst.hs:18:1-4 }
                {Name: DumpRenamedAst.main})
               (Prefix)
               (NoSrcStrict))
              []
              (Nothing)
              (GRHSs
-              [({ DumpRenamedAst.hs:11:6-23 }
+              [({ DumpRenamedAst.hs:18:6-23 }
                 (GRHS
                  []
-                 ({ DumpRenamedAst.hs:11:8-23 }
+                 ({ DumpRenamedAst.hs:18:8-23 }
                   (HsApp
-                   ({ DumpRenamedAst.hs:11:8-15 }
+                   ({ DumpRenamedAst.hs:18:8-15 }
                     (HsVar
-                     ({ DumpRenamedAst.hs:11:8-15 }
+                     ({ DumpRenamedAst.hs:18:8-15 }
                       {Name: putStrLn})))
-                   ({ DumpRenamedAst.hs:11:17-23 }
+                   ({ DumpRenamedAst.hs:18:17-23 }
                     (HsLit
                      (HsString
                       (SourceText
@@ -49,9 +49,9 @@
   [])
  []
  [(TyClGroup
-   [({ DumpRenamedAst.hs:5:1-30 }
+   [({ DumpRenamedAst.hs:6:1-30 }
      (DataDecl
-      ({ DumpRenamedAst.hs:5:6-10 }
+      ({ DumpRenamedAst.hs:6:6-10 }
        {Name: DumpRenamedAst.Peano})
       (HsQTvs
        []
@@ -65,9 +65,9 @@
         [])
        (Nothing)
        (Nothing)
-       [({ DumpRenamedAst.hs:5:14-17 }
+       [({ DumpRenamedAst.hs:6:14-17 }
          (ConDeclH98
-          ({ DumpRenamedAst.hs:5:14-17 }
+          ({ DumpRenamedAst.hs:6:14-17 }
            {Name: DumpRenamedAst.Zero})
           (Nothing)
           (Just
@@ -76,19 +76,19 @@
           (PrefixCon
            [])
           (Nothing)))
-       ,({ DumpRenamedAst.hs:5:21-30 }
+       ,({ DumpRenamedAst.hs:6:21-30 }
          (ConDeclH98
-          ({ DumpRenamedAst.hs:5:21-24 }
+          ({ DumpRenamedAst.hs:6:21-24 }
            {Name: DumpRenamedAst.Succ})
           (Nothing)
           (Just
            ({ <no location info> }
             []))
           (PrefixCon
-           [({ DumpRenamedAst.hs:5:26-30 }
+           [({ DumpRenamedAst.hs:6:26-30 }
              (HsTyVar
               (NotPromoted)
-              ({ DumpRenamedAst.hs:5:26-30 }
+              ({ DumpRenamedAst.hs:6:26-30 }
                {Name: DumpRenamedAst.Peano})))])
           (Nothing)))]
        ({ <no location info> }
@@ -99,103 +99,262 @@
    []
    [])
  ,(TyClGroup
-   [({ DumpRenamedAst.hs:7:1-39 }
+   [({ DumpRenamedAst.hs:8:1-39 }
      (FamDecl
       (FamilyDecl
        (ClosedTypeFamily
         (Just
-         [({ DumpRenamedAst.hs:8:3-36 }
+         [({ DumpRenamedAst.hs:9:3-36 }
            (HsIB
             [{Name: a}
             ,{Name: as}]
             (FamEqn
-             ({ DumpRenamedAst.hs:8:3-8 }
+             ({ DumpRenamedAst.hs:9:3-8 }
               {Name: DumpRenamedAst.Length})
-             [({ DumpRenamedAst.hs:8:10-17 }
+             [({ DumpRenamedAst.hs:9:10-17 }
                (HsParTy
-                ({ DumpRenamedAst.hs:8:11-16 }
+                ({ DumpRenamedAst.hs:9:11-16 }
                  (HsOpTy
-                  ({ DumpRenamedAst.hs:8:11 }
+                  ({ DumpRenamedAst.hs:9:11 }
                    (HsTyVar
                     (NotPromoted)
-                    ({ DumpRenamedAst.hs:8:11 }
+                    ({ DumpRenamedAst.hs:9:11 }
                      {Name: a})))
-                  ({ DumpRenamedAst.hs:8:13 }
+                  ({ DumpRenamedAst.hs:9:13 }
                    {Name: :})
-                  ({ DumpRenamedAst.hs:8:15-16 }
+                  ({ DumpRenamedAst.hs:9:15-16 }
                    (HsTyVar
                     (NotPromoted)
-                    ({ DumpRenamedAst.hs:8:15-16 }
+                    ({ DumpRenamedAst.hs:9:15-16 }
                      {Name: as})))))))]
              (Prefix)
-             ({ DumpRenamedAst.hs:8:21-36 }
+             ({ DumpRenamedAst.hs:9:21-36 }
               (HsAppTy
-               ({ DumpRenamedAst.hs:8:21-24 }
+               ({ DumpRenamedAst.hs:9:21-24 }
                 (HsTyVar
                  (NotPromoted)
-                 ({ DumpRenamedAst.hs:8:21-24 }
+                 ({ DumpRenamedAst.hs:9:21-24 }
                   {Name: DumpRenamedAst.Succ})))
-               ({ DumpRenamedAst.hs:8:26-36 }
+               ({ DumpRenamedAst.hs:9:26-36 }
                 (HsParTy
-                 ({ DumpRenamedAst.hs:8:27-35 }
+                 ({ DumpRenamedAst.hs:9:27-35 }
                   (HsAppTy
-                   ({ DumpRenamedAst.hs:8:27-32 }
+                   ({ DumpRenamedAst.hs:9:27-32 }
                     (HsTyVar
                      (NotPromoted)
-                     ({ DumpRenamedAst.hs:8:27-32 }
+                     ({ DumpRenamedAst.hs:9:27-32 }
                       {Name: DumpRenamedAst.Length})))
-                   ({ DumpRenamedAst.hs:8:34-35 }
+                   ({ DumpRenamedAst.hs:9:34-35 }
                     (HsTyVar
                      (NotPromoted)
-                     ({ DumpRenamedAst.hs:8:34-35 }
+                     ({ DumpRenamedAst.hs:9:34-35 }
                       {Name: as}))))))))))
             (True)))
-         ,({ DumpRenamedAst.hs:9:3-24 }
+         ,({ DumpRenamedAst.hs:10:3-24 }
            (HsIB
             []
             (FamEqn
-             ({ DumpRenamedAst.hs:9:3-8 }
+             ({ DumpRenamedAst.hs:10:3-8 }
               {Name: DumpRenamedAst.Length})
-             [({ DumpRenamedAst.hs:9:10-12 }
+             [({ DumpRenamedAst.hs:10:10-12 }
                (HsExplicitListTy
                 (Promoted)
                 (PlaceHolder)
                 []))]
              (Prefix)
-             ({ DumpRenamedAst.hs:9:21-24 }
+             ({ DumpRenamedAst.hs:10:21-24 }
               (HsTyVar
                (NotPromoted)
-               ({ DumpRenamedAst.hs:9:21-24 }
+               ({ DumpRenamedAst.hs:10:21-24 }
                 {Name: DumpRenamedAst.Zero}))))
             (True)))]))
-       ({ DumpRenamedAst.hs:7:13-18 }
+       ({ DumpRenamedAst.hs:8:13-18 }
         {Name: DumpRenamedAst.Length})
        (HsQTvs
         [{Name: k}]
-        [({ DumpRenamedAst.hs:7:20-30 }
+        [({ DumpRenamedAst.hs:8:20-30 }
           (KindedTyVar
-           ({ DumpRenamedAst.hs:7:21-22 }
+           ({ DumpRenamedAst.hs:8:21-22 }
             {Name: as})
-           ({ DumpRenamedAst.hs:7:27-29 }
+           ({ DumpRenamedAst.hs:8:27-29 }
             (HsListTy
-             ({ DumpRenamedAst.hs:7:28 }
+             ({ DumpRenamedAst.hs:8:28 }
               (HsTyVar
                (NotPromoted)
-               ({ DumpRenamedAst.hs:7:28 }
+               ({ DumpRenamedAst.hs:8:28 }
                 {Name: k})))))))]
         {NameSet:
          []})
        (Prefix)
-       ({ DumpRenamedAst.hs:7:32-39 }
+       ({ DumpRenamedAst.hs:8:32-39 }
         (KindSig
-         ({ DumpRenamedAst.hs:7:35-39 }
+         ({ DumpRenamedAst.hs:8:35-39 }
           (HsTyVar
            (NotPromoted)
-           ({ DumpRenamedAst.hs:7:35-39 }
+           ({ DumpRenamedAst.hs:8:35-39 }
             {Name: DumpRenamedAst.Peano})))))
        (Nothing))))]
    []
-   [])]
+   [])
+ ,(TyClGroup
+   [({ DumpRenamedAst.hs:12:1-30 }
+     (FamDecl
+      (FamilyDecl
+       (DataFamily)
+       ({ DumpRenamedAst.hs:12:13-15 }
+        {Name: DumpRenamedAst.Nat})
+       (HsQTvs
+        [{Name: k}]
+        []
+        {NameSet:
+         []})
+       (Prefix)
+       ({ DumpRenamedAst.hs:12:17-30 }
+        (KindSig
+         ({ DumpRenamedAst.hs:12:20-30 }
+          (HsFunTy
+           ({ DumpRenamedAst.hs:12:20 }
+            (HsTyVar
+             (NotPromoted)
+             ({ DumpRenamedAst.hs:12:20 }
+              {Name: k})))
+           ({ DumpRenamedAst.hs:12:25-30 }
+            (HsFunTy
+             ({ DumpRenamedAst.hs:12:25 }
+              (HsTyVar
+               (NotPromoted)
+               ({ DumpRenamedAst.hs:12:25 }
+                {Name: k})))
+             ({ DumpRenamedAst.hs:12:30 }
+              (HsTyVar
+               (NotPromoted)
+               ({ DumpRenamedAst.hs:12:30 }
+                {Name: *})))))))))
+       (Nothing))))]
+   []
+   [({ DumpRenamedAst.hs:(15,1)-(16,45) }
+     (DataFamInstD
+      (DataFamInstDecl
+       (HsIB
+        [{Name: k}
+        ,{Name: a}]
+        (FamEqn
+         ({ DumpRenamedAst.hs:15:18-20 }
+          {Name: DumpRenamedAst.Nat})
+         [({ DumpRenamedAst.hs:15:22-34 }
+           (HsKindSig
+            ({ DumpRenamedAst.hs:15:23 }
+             (HsTyVar
+              (NotPromoted)
+              ({ DumpRenamedAst.hs:15:23 }
+               {Name: a})))
+            ({ DumpRenamedAst.hs:15:28-33 }
+             (HsFunTy
+              ({ DumpRenamedAst.hs:15:28 }
+               (HsTyVar
+                (NotPromoted)
+                ({ DumpRenamedAst.hs:15:28 }
+                 {Name: k})))
+              ({ DumpRenamedAst.hs:15:33 }
+               (HsTyVar
+                (NotPromoted)
+                ({ DumpRenamedAst.hs:15:33 }
+                 {Name: *})))))))]
+         (Prefix)
+         (HsDataDefn
+          (NewType)
+          ({ <no location info> }
+           [])
+          (Nothing)
+          (Just
+           ({ DumpRenamedAst.hs:15:39-51 }
+            (HsFunTy
+             ({ DumpRenamedAst.hs:15:39-46 }
+              (HsParTy
+               ({ DumpRenamedAst.hs:15:40-45 }
+                (HsFunTy
+                 ({ DumpRenamedAst.hs:15:40 }
+                  (HsTyVar
+                   (NotPromoted)
+                   ({ DumpRenamedAst.hs:15:40 }
+                    {Name: k})))
+                 ({ DumpRenamedAst.hs:15:45 }
+                  (HsTyVar
+                   (NotPromoted)
+                   ({ DumpRenamedAst.hs:15:45 }
+                    {Name: *})))))))
+             ({ DumpRenamedAst.hs:15:51 }
+              (HsTyVar
+               (NotPromoted)
+               ({ DumpRenamedAst.hs:15:51 }
+                {Name: *}))))))
+          [({ DumpRenamedAst.hs:16:3-45 }
+            (ConDeclGADT
+             [({ DumpRenamedAst.hs:16:3-5 }
+               {Name: DumpRenamedAst.Nat})]
+             (HsIB
+              [{Name: f}
+              ,{Name: g}]
+              ({ DumpRenamedAst.hs:16:10-45 }
+               (HsFunTy
+                ({ DumpRenamedAst.hs:16:10-34 }
+                 (HsParTy
+                  ({ DumpRenamedAst.hs:16:11-33 }
+                   (HsForAllTy
+                    [({ DumpRenamedAst.hs:16:18-19 }
+                      (UserTyVar
+                       ({ DumpRenamedAst.hs:16:18-19 }
+                        {Name: xx})))]
+                    ({ DumpRenamedAst.hs:16:22-33 }
+                     (HsFunTy
+                      ({ DumpRenamedAst.hs:16:22-25 }
+                       (HsAppTy
+                        ({ DumpRenamedAst.hs:16:22 }
+                         (HsTyVar
+                          (NotPromoted)
+                          ({ DumpRenamedAst.hs:16:22 }
+                           {Name: f})))
+                        ({ DumpRenamedAst.hs:16:24-25 }
+                         (HsTyVar
+                          (NotPromoted)
+                          ({ DumpRenamedAst.hs:16:24-25 }
+                           {Name: xx})))))
+                      ({ DumpRenamedAst.hs:16:30-33 }
+                       (HsAppTy
+                        ({ DumpRenamedAst.hs:16:30 }
+                         (HsTyVar
+                          (NotPromoted)
+                          ({ DumpRenamedAst.hs:16:30 }
+                           {Name: g})))
+                        ({ DumpRenamedAst.hs:16:32-33 }
+                         (HsTyVar
+                          (NotPromoted)
+                          ({ DumpRenamedAst.hs:16:32-33 }
+                           {Name: xx})))))))))))
+                ({ DumpRenamedAst.hs:16:39-45 }
+                 (HsAppTy
+                  ({ DumpRenamedAst.hs:16:39-43 }
+                   (HsAppTy
+                    ({ DumpRenamedAst.hs:16:39-41 }
+                     (HsTyVar
+                      (NotPromoted)
+                      ({ DumpRenamedAst.hs:16:39-41 }
+                       {Name: DumpRenamedAst.Nat})))
+                    ({ DumpRenamedAst.hs:16:43 }
+                     (HsTyVar
+                      (NotPromoted)
+                      ({ DumpRenamedAst.hs:16:43 }
+                       {Name: f})))))
+                  ({ DumpRenamedAst.hs:16:45 }
+                   (HsTyVar
+                    (NotPromoted)
+                    ({ DumpRenamedAst.hs:16:45 }
+                     {Name: g})))))))
+              (True))
+             (Nothing)))]
+          ({ <no location info> }
+           [])))
+        (True)))))])]
  []
  []
  []
diff --git a/testsuite/tests/polykinds/T13985.hs b/testsuite/tests/polykinds/T13985.hs
new file mode 100644
index 0000000000..c0555d8f69
--- /dev/null
+++ b/testsuite/tests/polykinds/T13985.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module T13985 where
+
+import Data.Kind
+import Data.Proxy
+
+data family Fam
+data instance Fam = MkFam (forall (a :: k). Proxy a)
+
+type family T
+type instance T = Proxy (Nothing :: Maybe a)
+
+class C k where
+  data CD :: k
+  type CT :: k
+
+instance C Type where
+  data CD = forall (a :: k). CD (Proxy a)
+  type CT = Proxy (Nothing :: Maybe a)
+
+class Z a where
+  type ZT a
+  type ZT a = Proxy (Nothing :: Maybe x)
diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr
new file mode 100644
index 0000000000..954dae5dcd
--- /dev/null
+++ b/testsuite/tests/polykinds/T13985.stderr
@@ -0,0 +1,39 @@
+
+T13985.hs:12:1: error:
+    • Kind variable ‘k’ is implicitly bound in data family
+      ‘Fam’, but does not appear as the kind of any
+      of its type variables. Perhaps you meant
+      to bind it (with TypeInType) explicitly somewhere?
+    • In the data instance declaration for ‘Fam’
+
+T13985.hs:15:15: error:
+    • Kind variable ‘a’ is implicitly bound in type family
+      ‘T’, but does not appear as the kind of any
+      of its type variables. Perhaps you meant
+      to bind it (with TypeInType) explicitly somewhere?
+    • In the type instance declaration for ‘T’
+
+T13985.hs:22:3: error:
+    • Kind variable ‘k’ is implicitly bound in data family
+      ‘CD’, but does not appear as the kind of any
+      of its type variables. Perhaps you meant
+      to bind it (with TypeInType) explicitly somewhere?
+    • In the data instance declaration for ‘CD’
+      In the instance declaration for ‘C Type’
+
+T13985.hs:23:8: error:
+    • Kind variable ‘a’ is implicitly bound in type family
+      ‘CT’, but does not appear as the kind of any
+      of its type variables. Perhaps you meant
+      to bind it (with TypeInType) explicitly somewhere?
+    • In the type instance declaration for ‘CT’
+      In the instance declaration for ‘C Type’
+
+T13985.hs:27:3: error:
+    • Kind variable ‘x’ is implicitly bound in type family
+      ‘ZT’, but does not appear as the kind of any
+      of its type variables. Perhaps you meant
+      to bind it (with TypeInType) explicitly somewhere?
+      Type variables with inferred kinds: (k :: *) (a :: k)
+    • In the default type instance declaration for ‘ZT’
+      In the class declaration for ‘Z’
diff --git a/testsuite/tests/polykinds/T9574.stderr b/testsuite/tests/polykinds/T9574.stderr
deleted file mode 100644
index 50b42ad590..0000000000
--- a/testsuite/tests/polykinds/T9574.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-T9574.hs:11:5:
-    The RHS of an associated type declaration mentions ‘o’
-      All such variables must be bound on the LHS
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index bdba4c0ca4..864e204f72 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -106,7 +106,7 @@ test('T9200b', normal, compile_fail, [''])
 test('T9750', normal, compile, [''])
 test('T9569', normal, compile, [''])
 test('T9838', normal, multimod_compile, ['T9838.hs','-v0'])
-test('T9574', normal, compile_fail, [''])
+test('T9574', normal, compile, [''])
 test('T9833', normal, compile, [''])
 test('T7908', normal, compile, [''])
 test('PolyInstances', normal, compile, [''])
@@ -163,6 +163,7 @@ test('T13393', normal, compile_fail, [''])
 test('T13555', normal, compile_fail, [''])
 test('T13659', normal, compile_fail, [''])
 test('T13625', normal, compile_fail, [''])
+test('T13985', normal, compile_fail, [''])
 test('T14110', normal, compile_fail, [''])
 test('BadKindVar', normal, compile_fail, [''])
 test('T13738', normal, compile_fail, [''])