Use HsTyPats in associated type family defaults

Associated type family default declarations behave strangely in a
couple of ways:

1. If one tries to bind the type variables with an explicit `forall`,
   the `forall`'d part will simply be ignored. (#16110)
2. One cannot use visible kind application syntax on the left-hand
   sides of associated default equations, unlike every other form
   of type family equation. (#16356)

Both of these issues have a common solution. Instead of using
`LHsQTyVars` to represent the left-hand side arguments of an
associated default equation, we instead use `HsTyPats`, which is what
other forms of type family equations use. In particular, here are
some highlights of this patch:

* `FamEqn` is no longer parameterized by a `pats` type variable, as
  the `feqn_pats` field is now always `HsTyPats`.
* The new design for `FamEqn` in chronicled in
  `Note [Type family instance declarations in HsSyn]`.
* `TyFamDefltEqn` now becomes the same thing as `TyFamInstEqn`. This
  means that many of `TyFamDefltEqn`'s code paths can now reuse the
  code paths for `TyFamInstEqn`, resulting in substantial
  simplifications to various parts of the code dealing with
  associated type family defaults.

Fixes #16110 and #16356.

32 files changed, 474 insertions, 325 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 5de954ae7d..7e13fdcc36 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -328,7 +328,7 @@ repTyClD (dL->L loc (ClassDecl { tcdCtxt = cxt, tcdLName = cls,
               ; (ss, sigs_binds) <- rep_sigs_binds sigs meth_binds
               ; fds1   <- repLFunDeps fds
               ; ats1   <- repFamilyDecls ats
-              ; atds1  <- repAssocTyFamDefaults atds
+              ; atds1  <- mapM (repAssocTyFamDefaultD . unLoc) atds
               ; decls1 <- coreList decQTyConName (ats1 ++ atds1 ++ sigs_binds)
               ; decls2 <- repClass cxt1 cls1 bndrs fds1 decls1
               ; wrapGenSyms ss decls2 }
@@ -454,35 +454,8 @@ repInjectivityAnn (Just (dL->L _ (InjectivityAnn lhs rhs))) =
 repFamilyDecls :: [LFamilyDecl GhcRn] -> DsM [Core TH.DecQ]
 repFamilyDecls fds = liftM de_loc (mapM repFamilyDecl fds)
 
-repAssocTyFamDefaults :: [LTyFamDefltEqn GhcRn] -> DsM [Core TH.DecQ]
-repAssocTyFamDefaults = mapM rep_deflt
-  where
-     -- very like repTyFamEqn, but different in the details
-    rep_deflt :: LTyFamDefltEqn GhcRn -> DsM (Core TH.DecQ)
-    rep_deflt (dL->L _ (FamEqn { feqn_tycon = tc
-                               , feqn_bndrs = bndrs
-                               , feqn_pats  = tys
-                               , feqn_fixity = fixity
-                               , feqn_rhs   = rhs }))
-      = addTyClTyVarBinds tys $ \ _ ->
-        do { tc1  <- lookupLOcc tc
-           ; no_bndrs <- ASSERT( isNothing bndrs )
-                         coreNothingList tyVarBndrQTyConName
-           ; tys1 <- repLTys (hsLTyVarBndrsToTypes tys)
-           ; lhs <- case fixity of
-                      Prefix -> do { head_ty <- repNamedTyCon tc1
-                                   ; repTapps head_ty tys1 }
-                      Infix -> do { (t1:t2:args) <- checkTys tys1
-                                  ; head_ty <- repTInfix t1 tc1 t2
-                                  ; repTapps head_ty args }
-           ; rhs1 <- repLTy rhs
-           ; eqn1 <- repTySynEqn no_bndrs lhs rhs1
-           ; repTySynInst eqn1 }
-    rep_deflt _ = panic "repAssocTyFamDefaults"
-
-    checkTys :: [Core TH.TypeQ] -> DsM [Core TH.TypeQ]
-    checkTys tys@(_:_:_) = return tys
-    checkTys _ = panic "repAssocTyFamDefaults:checkTys"
+repAssocTyFamDefaultD :: TyFamDefltDecl GhcRn -> DsM (Core TH.DecQ)
+repAssocTyFamDefaultD = repTyFamInstD
 
 -------------------------
 -- represent fundeps
diff --git a/compiler/hieFile/HieAst.hs b/compiler/hieFile/HieAst.hs
index d86077ea27..84e5a627d8 100644
--- a/compiler/hieFile/HieAst.hs
+++ b/compiler/hieFile/HieAst.hs
@@ -333,7 +333,7 @@ instance HasLoc a => HasLoc [a] where
   loc [] = noSrcSpan
   loc xs = foldl1' combineSrcSpans $ map loc xs
 
-instance (HasLoc a, HasLoc b) => HasLoc (FamEqn s a b) where
+instance HasLoc a => HasLoc (FamEqn s a) where
   loc (FamEqn _ a Nothing b _ c) = foldl1' combineSrcSpans [loc a, loc b, loc c]
   loc (FamEqn _ a (Just tvs) b _ c) = foldl1' combineSrcSpans
                                               [loc a, loc tvs, loc b, loc c]
@@ -1149,18 +1149,12 @@ instance ToHie (LTyClDecl GhcRn) where
         , toHie $ fmap (BC InstanceBind ModuleScope) meths
         , toHie typs
         , concatMapM (pure . locOnly . getLoc) deftyps
-        , toHie $ map (go . unLoc) deftyps
+        , toHie deftyps
         ]
         where
           context_scope = mkLScope context
           rhs_scope = foldl1' combineScopes $ map mkScope
             [ loc deps, loc sigs, loc (bagToList meths), loc typs, loc deftyps]
-
-          go :: TyFamDefltEqn GhcRn
-             -> FamEqn GhcRn (TScoped (LHsQTyVars GhcRn)) (LHsType GhcRn)
-          go (FamEqn a var bndrs pat b rhs) =
-             FamEqn a var bndrs (TS (ResolvedScopes [mkLScope rhs]) pat) b rhs
-          go (XFamEqn NoExt) = XFamEqn NoExt
       XTyClDecl _ -> []
 
 instance ToHie (LFamilyDecl GhcRn) where
@@ -1206,15 +1200,12 @@ instance ToHie (Located (FunDep (Located Name))) where
     , toHie $ map (C Use) rhs
     ]
 
-instance (ToHie pats, ToHie rhs, HasLoc pats, HasLoc rhs)
-    => ToHie (TScoped (FamEqn GhcRn pats rhs)) where
+instance (ToHie rhs, HasLoc rhs)
+    => ToHie (TScoped (FamEqn GhcRn rhs)) where
   toHie (TS _ f) = toHie f
 
-instance ( ToHie pats
-         , ToHie rhs
-         , HasLoc pats
-         , HasLoc rhs
-         ) => ToHie (FamEqn GhcRn pats rhs) where
+instance (ToHie rhs, HasLoc rhs)
+    => ToHie (FamEqn GhcRn rhs) where
   toHie fe@(FamEqn _ var tybndrs pats _ rhs) = concatM $
     [ toHie $ C (Decl InstDec $ getRealSpan $ loc fe) var
     , toHie $ fmap (tvScopes (ResolvedScopes []) scope) tybndrs
diff --git a/compiler/hsSyn/Convert.hs b/compiler/hsSyn/Convert.hs
index 22e1a5a2ae..57aaefb830 100644
--- a/compiler/hsSyn/Convert.hs
+++ b/compiler/hsSyn/Convert.hs
@@ -243,27 +243,20 @@ cvtDec (NewtypeD ctxt tc tvs ksig constr derivs)
 cvtDec (ClassD ctxt cl tvs fds decs)
   = do  { (cxt', tc', tvs') <- cvt_tycl_hdr ctxt cl tvs
         ; fds'  <- mapM cvt_fundep fds
-        ; (binds', sigs', fams', ats', adts') <- cvt_ci_decs (text "a class declaration") decs
+        ; (binds', sigs', fams', at_defs', adts') <- cvt_ci_decs (text "a class declaration") decs
         ; unless (null adts')
             (failWith $ (text "Default data instance declarations"
                      <+> text "are not allowed:")
                    $$ (Outputable.ppr adts'))
-        ; at_defs <- mapM cvt_at_def ats'
         ; returnJustL $ TyClD noExt $
           ClassDecl { tcdCExt = noExt
                     , tcdCtxt = cxt', tcdLName = tc', tcdTyVars = tvs'
                     , tcdFixity = Prefix
                     , tcdFDs = fds', tcdSigs = Hs.mkClassOpSigs sigs'
                     , tcdMeths = binds'
-                    , tcdATs = fams', tcdATDefs = at_defs, tcdDocs = [] }
+                    , tcdATs = fams', tcdATDefs = at_defs', tcdDocs = [] }
                               -- no docs in TH ^^
         }
-  where
-    cvt_at_def :: LTyFamInstDecl GhcPs -> CvtM (LTyFamDefltEqn GhcPs)
-    -- Very similar to what happens in RdrHsSyn.mkClassDecl
-    cvt_at_def decl = case RdrHsSyn.mkATDefault decl of
-                        Right (def, _) -> return def
-                        Left (_, msg) -> failWith msg
 
 cvtDec (InstanceD o ctxt ty decs)
   = do  { let doc = text "an instance declaration"
diff --git a/compiler/hsSyn/HsDecls.hs b/compiler/hsSyn/HsDecls.hs
index e328bf43c7..388c770720 100644
--- a/compiler/hsSyn/HsDecls.hs
+++ b/compiler/hsSyn/HsDecls.hs
@@ -37,11 +37,11 @@ module HsDecls (
   -- ** Instance declarations
   InstDecl(..), LInstDecl, FamilyInfo(..),
   TyFamInstDecl(..), LTyFamInstDecl, instDeclDataFamInsts,
+  TyFamDefltDecl, LTyFamDefltDecl,
   DataFamInstDecl(..), LDataFamInstDecl,
-  pprDataFamInstFlavour, pprHsFamInstLHS,
+  pprDataFamInstFlavour, pprTyFamInstDecl, pprHsFamInstLHS,
   FamInstEqn, LFamInstEqn, FamEqn(..),
-  TyFamInstEqn, LTyFamInstEqn, TyFamDefltEqn, LTyFamDefltEqn,
-  HsTyPats,
+  TyFamInstEqn, LTyFamInstEqn, HsTyPats,
   LClsInstDecl, ClsInstDecl(..),
 
   -- ** Standalone deriving declarations
@@ -533,7 +533,7 @@ data TyClDecl pass
                 tcdSigs    :: [LSig pass],              -- ^ Methods' signatures
                 tcdMeths   :: LHsBinds pass,            -- ^ Default methods
                 tcdATs     :: [LFamilyDecl pass],       -- ^ Associated types;
-                tcdATDefs  :: [LTyFamDefltEqn pass],    -- ^ Associated type defaults
+                tcdATDefs  :: [LTyFamDefltDecl pass],   -- ^ Associated type defaults
                 tcdDocs    :: [LDocDecl]                -- ^ Haddock docs
     }
         -- ^ - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnClass',
@@ -726,7 +726,7 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (TyClDecl p) where
       | otherwise       -- Laid out
       = vcat [ top_matter <+> text "where"
              , nest 2 $ pprDeclList (map (pprFamilyDecl NotTopLevel . unLoc) ats ++
-                                     map ppr_fam_deflt_eqn at_defs ++
+                                     map (pprTyFamDefltDecl . unLoc) at_defs ++
                                      pprLHsBindsForUser methods sigs) ]
       where
         top_matter = text "class"
@@ -1507,28 +1507,23 @@ ppr_con_names = pprWithCommas (pprPrefixOcc . unLoc)
 Note [Type family instance declarations in HsSyn]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The data type FamEqn represents one equation of a type family instance.
-Aside from the pass, it is also parameterised over two fields:
-feqn_pats and feqn_rhs.
-
-feqn_pats is either LHsTypes (for ordinary data/type family instances) or
-LHsQTyVars (for associated type family default instances). In particular:
-
- * An ordinary type family instance declaration looks like this in source Haskell
-      type instance T [a] Int = a -> a
-   (or something similar for a closed family)
-   It is represented by a FamInstEqn, with a *type* (LHsType) in the feqn_pats
-   field.
-
- * On the other hand, the *default instance* of an associated type looks like
-   this in source Haskell
-      class C a where
-        type T a b
-        type T a b = a -> b   -- The default instance
-   It is represented by a TyFamDefltEqn, with *type variables* (LHsQTyVars) in
-   the feqn_pats field.
-
+Aside from the pass, it is also parameterised over another field, feqn_rhs.
 feqn_rhs is either an HsDataDefn (for data family instances) or an LHsType
 (for type family instances).
+
+Type family instances also include associated type family default equations.
+That is because a default for a type family looks like this:
+
+  class C a where
+    type family F a b :: Type
+    type F c d = (c,d)   -- Default instance
+
+The default declaration is really just a `type instance` declaration, but one
+with particularly simple patterns: they must all be distinct type variables.
+That's because we will instantiate it (in an instance declaration for `C`) if
+we don't give an explicit instance for `F`. Note that the names of the
+variables don't need to match those of the class: it really is like a
+free-standing `type instance` declaration.
 -}
 
 ----------------- Type synonym family instances -------------
@@ -1540,16 +1535,13 @@ type LTyFamInstEqn pass = Located (TyFamInstEqn pass)
 
 -- For details on above see note [Api annotations] in ApiAnnotation
 
--- | Located Type Family Default Equation
-type LTyFamDefltEqn pass = Located (TyFamDefltEqn pass)
-
 -- | Haskell Type Patterns
 type HsTyPats pass = [LHsTypeArg pass]
 
 {- Note [Family instance declaration binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For ordinary data/type family instances, the feqn_pats field of FamEqn stores
-the LHS type (and kind) patterns. Any type (and kind) variables contained
+The feqn_pats field of FamEqn (family instance equation) stores the LHS type
+(and kind) patterns. Any type (and kind) variables contained
 in these type patterns are bound in the hsib_vars field of the HsImplicitBndrs
 in FamInstEqn depending on whether or not an explicit forall is present. In
 the case of an explicit forall, the hsib_vars only includes kind variables not
@@ -1577,19 +1569,19 @@ the hsib_vars. In the latter case, note that in particular
    so that we can compare the type pattern in the 'instance' decl and
    in the associated 'type' decl
 
-For associated type family default instances (TyFamDefltEqn), instead of using
-type patterns with binders in a surrounding HsImplicitBndrs, we use raw type
-variables (LHsQTyVars) in the feqn_pats field of FamEqn.
-
-c.f. Note [TyVar binders for associated declarations]
+c.f. Note [TyVar binders for associated decls]
 -}
 
 -- | Type Family Instance Equation
 type TyFamInstEqn pass = FamInstEqn pass (LHsType pass)
 
--- | Type Family Default Equation
-type TyFamDefltEqn pass = FamEqn pass (LHsQTyVars pass) (LHsType pass)
-  -- See Note [Type family instance declarations in HsSyn]
+-- | Type family default declarations.
+-- A convenient synonym for 'TyFamInstDecl'.
+-- See @Note [Type family instance declarations in HsSyn]@.
+type TyFamDefltDecl = TyFamInstDecl
+
+-- | Located type family default declarations.
+type LTyFamDefltDecl pass = Located (TyFamDefltDecl pass)
 
 -- | Located Type Family Instance Declaration
 type LTyFamInstDecl pass = Located (TyFamInstDecl pass)
@@ -1625,8 +1617,7 @@ newtype DataFamInstDecl pass
 type LFamInstEqn pass rhs = Located (FamInstEqn pass rhs)
 
 -- | Family Instance Equation
-type FamInstEqn pass rhs
-  = HsImplicitBndrs pass (FamEqn pass (HsTyPats pass) rhs)
+type FamInstEqn pass rhs = HsImplicitBndrs pass (FamEqn pass rhs)
             -- ^ Here, the @pats@ are type patterns (with kind and type bndrs).
             -- See Note [Family instance declaration binders]
 
@@ -1636,23 +1627,23 @@ type FamInstEqn pass rhs
 -- declaration, or type family default.
 -- See Note [Type family instance declarations in HsSyn]
 -- See Note [Family instance declaration binders]
-data FamEqn pass pats rhs
+data FamEqn pass rhs
   = FamEqn
-       { feqn_ext    :: XCFamEqn pass pats rhs
+       { feqn_ext    :: XCFamEqn pass rhs
        , feqn_tycon  :: Located (IdP pass)
        , feqn_bndrs  :: Maybe [LHsTyVarBndr pass] -- ^ Optional quantified type vars
-       , feqn_pats   :: pats
+       , feqn_pats   :: HsTyPats pass
        , feqn_fixity :: LexicalFixity -- ^ Fixity used in the declaration
        , feqn_rhs    :: rhs
        }
     -- ^
     --  - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnEqual'
-  | XFamEqn (XXFamEqn pass pats rhs)
+  | XFamEqn (XXFamEqn pass rhs)
 
     -- For details on above see note [Api annotations] in ApiAnnotation
 
-type instance XCFamEqn    (GhcPass _) p r = NoExt
-type instance XXFamEqn    (GhcPass _) p r = NoExt
+type instance XCFamEqn    (GhcPass _) r = NoExt
+type instance XXFamEqn    (GhcPass _) r = NoExt
 
 ----------------- Class instances -------------
 
@@ -1723,6 +1714,10 @@ ppr_instance_keyword :: TopLevelFlag -> SDoc
 ppr_instance_keyword TopLevel    = text "instance"
 ppr_instance_keyword NotTopLevel = empty
 
+pprTyFamDefltDecl :: (OutputableBndrId (GhcPass p))
+                  => TyFamDefltDecl (GhcPass p) -> SDoc
+pprTyFamDefltDecl = pprTyFamInstDecl NotTopLevel
+
 ppr_fam_inst_eqn :: (OutputableBndrId (GhcPass p))
                  => TyFamInstEqn (GhcPass p) -> SDoc
 ppr_fam_inst_eqn (HsIB { hsib_body = FamEqn { feqn_tycon  = L _ tycon
@@ -1734,16 +1729,6 @@ ppr_fam_inst_eqn (HsIB { hsib_body = FamEqn { feqn_tycon  = L _ tycon
 ppr_fam_inst_eqn (HsIB { hsib_body = XFamEqn x }) = ppr x
 ppr_fam_inst_eqn (XHsImplicitBndrs x) = ppr x
 
-ppr_fam_deflt_eqn :: (OutputableBndrId (GhcPass p))
-                  => LTyFamDefltEqn (GhcPass p) -> SDoc
-ppr_fam_deflt_eqn (L _ (FamEqn { feqn_tycon  = tycon
-                               , feqn_pats   = tvs
-                               , feqn_fixity = fixity
-                               , feqn_rhs    = rhs }))
-    = text "type" <+> pp_vanilla_decl_head tycon tvs fixity noLHsContext
-                  <+> equals <+> ppr rhs
-ppr_fam_deflt_eqn (L _ (XFamEqn x)) = ppr x
-
 instance (p ~ GhcPass pass, OutputableBndrId p)
        => Outputable (DataFamInstDecl p) where
   ppr = pprDataFamInstDecl TopLevel
diff --git a/compiler/hsSyn/HsExtension.hs b/compiler/hsSyn/HsExtension.hs
index 1d14da20b9..0ae0dd01e3 100644
--- a/compiler/hsSyn/HsExtension.hs
+++ b/compiler/hsSyn/HsExtension.hs
@@ -355,12 +355,12 @@ type ForallXConDecl (c :: * -> Constraint) (x :: *) =
 
 -- -------------------------------------
 -- FamEqn type families
-type family XCFamEqn      x p r
-type family XXFamEqn      x p r
+type family XCFamEqn      x r
+type family XXFamEqn      x r
 
-type ForallXFamEqn (c :: * -> Constraint) (x :: *) (p :: *) (r :: *) =
-       ( c (XCFamEqn       x p r)
-       , c (XXFamEqn       x p r)
+type ForallXFamEqn (c :: * -> Constraint) (x :: *) (r :: *) =
+       ( c (XCFamEqn       x r)
+       , c (XXFamEqn       x r)
        )
 
 -- -------------------------------------
diff --git a/compiler/hsSyn/HsInstances.hs b/compiler/hsSyn/HsInstances.hs
index 39507362cf..9c0698b7ef 100644
--- a/compiler/hsSyn/HsInstances.hs
+++ b/compiler/hsSyn/HsInstances.hs
@@ -164,10 +164,10 @@ deriving instance Data (DataFamInstDecl GhcPs)
 deriving instance Data (DataFamInstDecl GhcRn)
 deriving instance Data (DataFamInstDecl GhcTc)
 
--- deriving instance (DataIdLR p p,Data pats,Data rhs)=>Data (FamEqn p pats rhs)
-deriving instance (Data pats,Data rhs) => Data (FamEqn GhcPs pats rhs)
-deriving instance (Data pats,Data rhs) => Data (FamEqn GhcRn pats rhs)
-deriving instance (Data pats,Data rhs) => Data (FamEqn GhcTc pats rhs)
+-- deriving instance (DataIdLR p p,Data rhs)=>Data (FamEqn p rhs)
+deriving instance Data rhs => Data (FamEqn GhcPs rhs)
+deriving instance Data rhs => Data (FamEqn GhcRn rhs)
+deriving instance Data rhs => Data (FamEqn GhcTc rhs)
 
 -- deriving instance (DataIdLR p p) => Data (ClsInstDecl p)
 deriving instance Data (ClsInstDecl GhcPs)
diff --git a/compiler/parser/RdrHsSyn.hs b/compiler/parser/RdrHsSyn.hs
index 490fed0384..c479ab0e1c 100644
--- a/compiler/parser/RdrHsSyn.hs
+++ b/compiler/parser/RdrHsSyn.hs
@@ -45,7 +45,6 @@ module   RdrHsSyn (
         mkExtName,    -- RdrName -> CLabelString
         mkGadtDecl,   -- [Located RdrName] -> LHsType RdrName -> ConDecl RdrName
         mkConDeclH98,
-        mkATDefault,
 
         -- Bunch of functions in the parser monad for
         -- checking and constructing values
@@ -173,14 +172,12 @@ mkClassDecl :: SrcSpan
             -> P (LTyClDecl GhcPs)
 
 mkClassDecl loc (dL->L _ (mcxt, tycl_hdr)) fds where_cls
-  = do { (binds, sigs, ats, at_insts, _, docs) <- cvBindsAndSigs where_cls
+  = do { (binds, sigs, ats, at_defs, _, docs) <- cvBindsAndSigs where_cls
        ; let cxt = fromMaybe (noLoc []) mcxt
        ; (cls, tparams, fixity, ann) <- checkTyClHdr True tycl_hdr
        ; addAnnsAt loc ann -- Add any API Annotations to the top SrcSpan
-       ; (tyvars,annst) <- checkTyVarsP (text "class") whereDots cls tparams
+       ; (tyvars,annst) <- checkTyVars (text "class") whereDots cls tparams
        ; addAnnsAt loc annst -- Add any API Annotations to the top SrcSpan
-       ; (at_defs, annsi) <- mapAndUnzipM (eitherToP . mkATDefault) at_insts
-       ; sequence_ annsi
        ; return (cL loc (ClassDecl { tcdCExt = noExt, tcdCtxt = cxt
                                    , tcdLName = cls, tcdTyVars = tyvars
                                    , tcdFixity = fixity
@@ -190,34 +187,6 @@ mkClassDecl loc (dL->L _ (mcxt, tycl_hdr)) fds where_cls
                                    , tcdATs = ats, tcdATDefs = at_defs
                                    , tcdDocs  = docs })) }
 
-mkATDefault :: LTyFamInstDecl GhcPs
-            -> Either (SrcSpan, SDoc) (LTyFamDefltEqn GhcPs, P ())
--- ^ Take a type-family instance declaration and turn it into
--- a type-family default equation for a class declaration.
--- We parse things as the former and use this function to convert to the latter
---
--- We use the Either monad because this also called from "Convert".
---
--- The @P ()@ we return corresponds represents an action which will add
--- some necessary paren annotations to the parsing context. Naturally, this
--- is not something that the "Convert" use cares about.
-mkATDefault (dL->L loc (TyFamInstDecl { tfid_eqn = HsIB { hsib_body = e }}))
-      | FamEqn { feqn_tycon = tc, feqn_bndrs = bndrs, feqn_pats = pats
-               , feqn_fixity = fixity, feqn_rhs = rhs } <- e
-      = do { (tvs, anns) <- checkTyVars (text "default") equalsDots tc pats
-           ; let f = cL loc (FamEqn { feqn_ext    = noExt
-                                    , feqn_tycon  = tc
-                                    , feqn_bndrs  = ASSERT( isNothing bndrs )
-                                                    Nothing
-                                    , feqn_pats   = tvs
-                                    , feqn_fixity = fixity
-                                    , feqn_rhs    = rhs })
-           ; pure (f, addAnnsAt loc anns) }
-mkATDefault (dL->L _ (TyFamInstDecl (HsIB _ (XFamEqn _)))) = panic "mkATDefault"
-mkATDefault (dL->L _ (TyFamInstDecl (XHsImplicitBndrs _))) = panic "mkATDefault"
-mkATDefault _ = panic "mkATDefault: Impossible Match"
-                                -- due to #15884
-
 mkTyData :: SrcSpan
          -> NewOrData
          -> Maybe (Located CType)
@@ -230,7 +199,7 @@ mkTyData loc new_or_data cType (dL->L _ (mcxt, tycl_hdr))
          ksig data_cons maybe_deriv
   = do { (tc, tparams, fixity, ann) <- checkTyClHdr False tycl_hdr
        ; addAnnsAt loc ann -- Add any API Annotations to the top SrcSpan
-       ; (tyvars, anns) <- checkTyVarsP (ppr new_or_data) equalsDots tc tparams
+       ; (tyvars, anns) <- checkTyVars (ppr new_or_data) equalsDots tc tparams
        ; addAnnsAt loc anns -- Add any API Annotations to the top SrcSpan
        ; defn <- mkDataDefn new_or_data cType mcxt ksig data_cons maybe_deriv
        ; return (cL loc (DataDecl { tcdDExt = noExt,
@@ -263,7 +232,7 @@ mkTySynonym :: SrcSpan
 mkTySynonym loc lhs rhs
   = do { (tc, tparams, fixity, ann) <- checkTyClHdr False lhs
        ; addAnnsAt loc ann -- Add any API Annotations to the top SrcSpan
-       ; (tyvars, anns) <- checkTyVarsP (text "type") equalsDots tc tparams
+       ; (tyvars, anns) <- checkTyVars (text "type") equalsDots tc tparams
        ; addAnnsAt loc anns -- Add any API Annotations to the top SrcSpan
        ; return (cL loc (SynDecl { tcdSExt = noExt
                                  , tcdLName = tc, tcdTyVars = tyvars
@@ -322,7 +291,7 @@ mkFamDecl :: SrcSpan
 mkFamDecl loc info lhs ksig injAnn
   = do { (tc, tparams, fixity, ann) <- checkTyClHdr False lhs
        ; addAnnsAt loc ann -- Add any API Annotations to the top SrcSpan
-       ; (tyvars, anns) <- checkTyVarsP (ppr info) equals_or_where tc tparams
+       ; (tyvars, anns) <- checkTyVars (ppr info) equals_or_where tc tparams
        ; addAnnsAt loc anns -- Add any API Annotations to the top SrcSpan
        ; return (cL loc (FamDecl noExt (FamilyDecl
                                            { fdExt       = noExt
@@ -804,56 +773,47 @@ to make setRdrNameSpace partial, so we just make an Unqual name instead. It
 really doesn't matter!
 -}
 
-checkTyVarsP :: SDoc -> SDoc -> Located RdrName -> [LHsTypeArg GhcPs]
-             -> P (LHsQTyVars GhcPs, [AddAnn])
--- Same as checkTyVars, but in the P monad
-checkTyVarsP pp_what equals_or_where tc tparms
-  = do { let checkedTvs = checkTyVars pp_what equals_or_where tc tparms
-       ; eitherToP checkedTvs }
-
 eitherToP :: Either (SrcSpan, SDoc) a -> P a
 -- Adapts the Either monad to the P monad
 eitherToP (Left (loc, doc)) = addFatalError loc doc
 eitherToP (Right thing)     = return thing
 
 checkTyVars :: SDoc -> SDoc -> Located RdrName -> [LHsTypeArg GhcPs]
-            -> Either (SrcSpan, SDoc)
-                      ( LHsQTyVars GhcPs  -- the synthesized type variables
-                      , [AddAnn] )        -- action which adds annotations
+            -> P ( LHsQTyVars GhcPs  -- the synthesized type variables
+                 , [AddAnn] )        -- action which adds annotations
 -- ^ Check whether the given list of type parameters are all type variables
 -- (possibly with a kind signature).
--- We use the Either monad because it's also called (via 'mkATDefault') from
--- "Convert".
 checkTyVars pp_what equals_or_where tc tparms
   = do { (tvs, anns) <- fmap unzip $ mapM check tparms
        ; return (mkHsQTvs tvs, concat anns) }
   where
     check (HsTypeArg _ ki@(L loc _))
-                              = Left (loc,
+                              = addFatalError loc $
                                       vcat [ text "Unexpected type application" <+>
                                             text "@" <> ppr ki
                                           , text "In the" <+> pp_what <+>
-                                            ptext (sLit "declaration for") <+> quotes (ppr tc)])
+                                            ptext (sLit "declaration for") <+> quotes (ppr tc)]
     check (HsValArg ty) = chkParens [] ty
-    check (HsArgPar sp) = Left (sp, vcat [text "Malformed" <+> pp_what
-                           <+> text "declaration for" <+> quotes (ppr tc)])
+    check (HsArgPar sp) = addFatalError sp $
+                          vcat [text "Malformed" <+> pp_what
+                            <+> text "declaration for" <+> quotes (ppr tc)]
         -- Keep around an action for adjusting the annotations of extra parens
     chkParens :: [AddAnn] -> LHsType GhcPs
-              -> Either (SrcSpan, SDoc) (LHsTyVarBndr GhcPs, [AddAnn])
+              -> P (LHsTyVarBndr GhcPs, [AddAnn])
     chkParens acc (dL->L l (HsParTy _ ty)) = chkParens (mkParensApiAnn l
                                                         ++ acc) ty
-    chkParens acc ty = case chk ty of
-      Left err -> Left err
-      Right tv -> Right (tv, reverse acc)
+    chkParens acc ty = do
+      tv <- chk ty
+      return (tv, reverse acc)
 
         -- Check that the name space is correct!
-    chk :: LHsType GhcPs -> Either (SrcSpan, SDoc) (LHsTyVarBndr GhcPs)
+    chk :: LHsType GhcPs -> P (LHsTyVarBndr GhcPs)
     chk (dL->L l (HsKindSig _ (dL->L lv (HsTyVar _ _ (dL->L _ tv))) k))
         | isRdrTyVar tv    = return (cL l (KindedTyVar noExt (cL lv tv) k))
     chk (dL->L l (HsTyVar _ _ (dL->L ltv tv)))
         | isRdrTyVar tv    = return (cL l (UserTyVar noExt (cL ltv tv)))
     chk t@(dL->L loc _)
-        = Left (loc,
+        = addFatalError loc $
                 vcat [ text "Unexpected type" <+> quotes (ppr t)
                      , text "In the" <+> pp_what
                        <+> ptext (sLit "declaration for") <+> quotes tc'
@@ -863,7 +823,7 @@ checkTyVars pp_what equals_or_where tc tparms
                        (pp_what
                         <+> tc'
                         <+> hsep (map text (takeList tparms allNameStrings))
-                        <+> equals_or_where) ] ])
+                        <+> equals_or_where) ] ]
 
     -- Avoid printing a constraint tuple in the error message. Print
     -- a plain old tuple instead (since that's what the user probably
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 537f283183..9e0d616ace 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -424,11 +424,11 @@ patchCCallTarget unitId callTarget =
 
 rnSrcInstDecl :: InstDecl GhcPs -> RnM (InstDecl GhcRn, FreeVars)
 rnSrcInstDecl (TyFamInstD { tfid_inst = tfi })
-  = do { (tfi', fvs) <- rnTyFamInstDecl Nothing tfi
+  = do { (tfi', fvs) <- rnTyFamInstDecl NonAssocTyFamEqn tfi
        ; return (TyFamInstD { tfid_ext = noExt, tfid_inst = tfi' }, fvs) }
 
 rnSrcInstDecl (DataFamInstD { dfid_inst = dfi })
-  = do { (dfi', fvs) <- rnDataFamInstDecl Nothing dfi
+  = do { (dfi', fvs) <- rnDataFamInstDecl NonAssocTyFamEqn dfi
        ; return (DataFamInstD { dfid_ext = noExt, dfid_inst = dfi' }, fvs) }
 
 rnSrcInstDecl (ClsInstD { cid_inst = cid })
@@ -666,21 +666,22 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
 rnClsInstDecl (XClsInstDecl _) = panic "rnClsInstDecl"
 
 rnFamInstEqn :: HsDocContext
-             -> Maybe (Name, [Name]) -- Nothing => not associated
-                                     -- Just (cls,tvs) => associated,
-                                     --   and gives class and tyvars of the
-                                     --   parent instance decl
+             -> AssocTyFamInfo
              -> [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 rhs_kvars
+rnFamInstEqn doc atfi rhs_kvars
     (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
                                , feqn_bndrs  = mb_bndrs
                                , feqn_pats   = pats
                                , feqn_fixity = fixity
                                , feqn_rhs    = payload }}) rn_payload
-  = do { tycon'   <- lookupFamInstName (fmap fst mb_cls) tycon
+  = do { let mb_cls = case atfi of
+                        NonAssocTyFamEqn     -> Nothing
+                        AssocTyFamDeflt cls  -> Just cls
+                        AssocTyFamInst cls _ -> Just cls
+       ; tycon'   <- lookupFamInstName mb_cls tycon
        ; let pat_kity_vars_with_dups = extractHsTyArgRdrKiTyVarsDup pats
              -- Use the "...Dups" form because it's needed
              -- below to report unsed binder on the LHS
@@ -730,9 +731,10 @@ rnFamInstEqn doc mb_cls rhs_kvars
                           --     Note [Unused type variables in family instances]
                     ; let nms_used = extendNameSetList rhs_fvs $
                                         inst_tvs ++ nms_dups
-                          inst_tvs = case mb_cls of
-                                       Nothing            -> []
-                                       Just (_, inst_tvs) -> inst_tvs
+                          inst_tvs = case atfi of
+                                       NonAssocTyFamEqn          -> []
+                                       AssocTyFamDeflt _         -> []
+                                       AssocTyFamInst _ inst_tvs -> inst_tvs
                           all_nms = all_imp_var_names ++ hsLTyVarNames bndrs'
                     ; warnUnusedTypePatterns all_nms nms_used
 
@@ -753,15 +755,27 @@ rnFamInstEqn doc mb_cls rhs_kvars
 rnFamInstEqn _ _ _ (HsIB _ (XFamEqn _)) _ = panic "rnFamInstEqn"
 rnFamInstEqn _ _ _ (XHsImplicitBndrs _) _ = panic "rnFamInstEqn"
 
-rnTyFamInstDecl :: Maybe (Name, [Name]) -- Just (cls,tvs) => associated,
-                                        --   and gives class and tyvars of
-                                        --   the parent instance decl
+rnTyFamInstDecl :: AssocTyFamInfo
                 -> TyFamInstDecl GhcPs
                 -> RnM (TyFamInstDecl GhcRn, FreeVars)
-rnTyFamInstDecl mb_cls (TyFamInstDecl { tfid_eqn = eqn })
-  = do { (eqn', fvs) <- rnTyFamInstEqn mb_cls NotClosedTyFam eqn
+rnTyFamInstDecl atfi (TyFamInstDecl { tfid_eqn = eqn })
+  = do { (eqn', fvs) <- rnTyFamInstEqn atfi NotClosedTyFam eqn
        ; return (TyFamInstDecl { tfid_eqn = eqn' }, fvs) }
 
+-- | Tracks whether we are renaming:
+--
+-- 1. A type family equation that is not associated
+--    with a parent type class ('NonAssocTyFamEqn')
+--
+-- 2. An associated type family default delcaration ('AssocTyFamDeflt')
+--
+-- 3. An associated type family instance declaration ('AssocTyFamInst')
+data AssocTyFamInfo
+  = NonAssocTyFamEqn
+  | AssocTyFamDeflt Name   -- Name of the parent class
+  | AssocTyFamInst  Name   -- Name of the parent class
+                    [Name] -- Names of the tyvars of the parent instance decl
+
 -- | Tracks whether we are renaming an equation in a closed type family
 -- equation ('ClosedTyFam') or not ('NotClosedTyFam').
 data ClosedTyFamInfo
@@ -769,17 +783,17 @@ data ClosedTyFamInfo
   | ClosedTyFam (Located RdrName) Name
                 -- The names (RdrName and Name) of the closed type family
 
-rnTyFamInstEqn :: Maybe (Name, [Name])
+rnTyFamInstEqn :: AssocTyFamInfo
                -> ClosedTyFamInfo
                -> TyFamInstEqn GhcPs
                -> RnM (TyFamInstEqn GhcRn, FreeVars)
-rnTyFamInstEqn mb_cls ctf_info
+rnTyFamInstEqn atfi ctf_info
     eqn@(HsIB { hsib_body = FamEqn { feqn_tycon = tycon
                                    , feqn_rhs   = rhs }})
   = do { let rhs_kvs = extractHsTyRdrTyVarsKindVars rhs
        ; (eqn'@(HsIB { hsib_body =
                        FamEqn { feqn_tycon = dL -> L _ tycon' }}), fvs)
-           <- rnFamInstEqn (TySynCtx tycon) mb_cls rhs_kvs eqn rnTySyn
+           <- rnFamInstEqn (TySynCtx tycon) atfi rhs_kvs eqn rnTySyn
        ; case ctf_info of
            NotClosedTyFam -> pure ()
            ClosedTyFam fam_rdr_name fam_name ->
@@ -790,38 +804,20 @@ rnTyFamInstEqn mb_cls ctf_info
 rnTyFamInstEqn _ _ (HsIB _ (XFamEqn _)) = panic "rnTyFamInstEqn"
 rnTyFamInstEqn _ _ (XHsImplicitBndrs _) = panic "rnTyFamInstEqn"
 
-rnTyFamDefltEqn :: Name
-                -> TyFamDefltEqn GhcPs
-                -> RnM (TyFamDefltEqn GhcRn, FreeVars)
-rnTyFamDefltEqn cls (FamEqn { feqn_tycon  = tycon
-                            , feqn_bndrs  = bndrs
-                            , feqn_pats   = tyvars
-                            , feqn_fixity = fixity
-                            , feqn_rhs    = rhs })
-  = do { let 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_ext    = noExt
-                        , feqn_tycon  = tycon'
-                        , feqn_bndrs  = ASSERT( isNothing bndrs )
-                                        Nothing
-                        , feqn_pats   = tyvars'
-                        , feqn_fixity = fixity
-                        , feqn_rhs    = rhs' }, fvs) } }
-  where
-    ctx = TyFamilyCtx tycon
-rnTyFamDefltEqn _ (XFamEqn _) = panic "rnTyFamDefltEqn"
+rnTyFamDefltDecl :: Name
+                 -> TyFamDefltDecl GhcPs
+                 -> RnM (TyFamDefltDecl GhcRn, FreeVars)
+rnTyFamDefltDecl cls = rnTyFamInstDecl (AssocTyFamDeflt cls)
 
-rnDataFamInstDecl :: Maybe (Name, [Name])
+rnDataFamInstDecl :: AssocTyFamInfo
                   -> DataFamInstDecl GhcPs
                   -> RnM (DataFamInstDecl GhcRn, FreeVars)
-rnDataFamInstDecl mb_cls (DataFamInstDecl { dfid_eqn = eqn@(HsIB { hsib_body =
-                           FamEqn { feqn_tycon = tycon
-                                  , feqn_rhs   = rhs }})})
+rnDataFamInstDecl atfi (DataFamInstDecl { dfid_eqn = eqn@(HsIB { hsib_body =
+                         FamEqn { feqn_tycon = tycon
+                                , feqn_rhs   = rhs }})})
   = do { let rhs_kvs = extractDataDefnKindVars rhs
        ; (eqn', fvs) <-
-           rnFamInstEqn (TyDataCtx tycon) mb_cls rhs_kvs eqn rnDataDefn
+           rnFamInstEqn (TyDataCtx tycon) atfi rhs_kvs eqn rnDataDefn
        ; return (DataFamInstDecl { dfid_eqn = eqn' }, fvs) }
 rnDataFamInstDecl _ (DataFamInstDecl (HsIB _ (XFamEqn _)))
   = panic "rnDataFamInstDecl"
@@ -837,8 +833,8 @@ rnATDecls :: Name      -- Class
 rnATDecls cls at_decls
   = rnList (rnFamDecl (Just cls)) at_decls
 
-rnATInstDecls :: (Maybe (Name, [Name]) -> -- The function that renames
-                  decl GhcPs ->            -- an instance. rnTyFamInstDecl
+rnATInstDecls :: (AssocTyFamInfo ->           -- The function that renames
+                  decl GhcPs ->               -- an instance. rnTyFamInstDecl
                   RnM (decl GhcRn, FreeVars)) -- or rnDataFamInstDecl
               -> Name      -- Class
               -> [Name]
@@ -850,7 +846,7 @@ rnATInstDecls :: (Maybe (Name, [Name]) -> -- The function that renames
 -- NB: We allow duplicate associated-type decls;
 --     See Note [Associated type instances] in TcInstDcls
 rnATInstDecls rnFun cls tv_ns at_insts
-  = rnList (rnFun (Just (cls, tv_ns))) at_insts
+  = rnList (rnFun (AssocTyFamInst cls tv_ns)) at_insts
     -- See Note [Renaming associated types]
 
 {- Note [Wildcards in family instances]
@@ -1585,7 +1581,7 @@ rnTyClDecl (ClassDecl { tcdCtxt = context, tcdLName = lcls,
                          fv_ats
              ; return ((tyvars', context', fds', ats'), fvs) }
 
-        ; (at_defs', fv_at_defs) <- rnList (rnTyFamDefltEqn cls') at_defs
+        ; (at_defs', fv_at_defs) <- rnList (rnTyFamDefltDecl cls') at_defs
 
         -- No need to check for duplicate associated type decls
         -- since that is done by RnNames.extendGlobalRdrEnvRn
@@ -1884,7 +1880,7 @@ rnFamDecl mb_cls (FamilyDecl { fdLName = tycon, fdTyVars = tyvars
              -> FamilyInfo GhcPs -> RnM (FamilyInfo GhcRn, FreeVars)
      rn_info (dL->L _ fam_name) (ClosedTypeFamily (Just eqns))
        = do { (eqns', fvs)
-                <- rnList (rnTyFamInstEqn Nothing (ClosedTyFam tycon fam_name))
+                <- rnList (rnTyFamInstEqn NonAssocTyFamEqn (ClosedTyFam tycon fam_name))
                                           -- no class context
                           eqns
             ; return (ClosedTypeFamily (Just eqns'), fvs) }
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index a825573dba..c00a8de378 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -74,6 +74,7 @@ import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
 import Data.Foldable
+import Data.Function ( on )
 import Data.List
 import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
@@ -1412,7 +1413,7 @@ tcTyClDecl1 _ _ (XTyClDecl _) = panic "tcTyClDecl1"
 
 tcClassDecl1 :: RolesInfo -> Name -> LHsContext GhcRn
              -> LHsBinds GhcRn -> [LHsFunDep GhcRn] -> [LSig GhcRn]
-             -> [LFamilyDecl GhcRn] -> [LTyFamDefltEqn GhcRn]
+             -> [LFamilyDecl GhcRn] -> [LTyFamDefltDecl GhcRn]
              -> TcM Class
 tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
   = fixM $ \ clas ->
@@ -1478,10 +1479,10 @@ Note that we can get default definitions only for type families, not data
 families.
 -}
 
-tcClassATs :: Name                   -- The class name (not knot-tied)
-           -> Class                  -- The class parent of this associated type
-           -> [LFamilyDecl GhcRn]    -- Associated types.
-           -> [LTyFamDefltEqn GhcRn] -- Associated type defaults.
+tcClassATs :: Name                    -- The class name (not knot-tied)
+           -> Class                   -- The class parent of this associated type
+           -> [LFamilyDecl GhcRn]     -- Associated types.
+           -> [LTyFamDefltDecl GhcRn] -- Associated type defaults.
            -> TcM [ClassATItem]
 tcClassATs class_name cls ats at_defs
   = do {  -- Complain about associated type defaults for non associated-types
@@ -1490,15 +1491,15 @@ tcClassATs class_name cls ats at_defs
                    , not (n `elemNameSet` at_names) ]
        ; mapM tc_at ats }
   where
-    at_def_tycon :: LTyFamDefltEqn GhcRn -> Name
-    at_def_tycon (dL->L _ eqn) = unLoc (feqn_tycon eqn)
+    at_def_tycon :: LTyFamDefltDecl GhcRn -> Name
+    at_def_tycon (dL->L _ eqn) = tyFamInstDeclName eqn
 
     at_fam_name :: LFamilyDecl GhcRn -> Name
     at_fam_name (dL->L _ decl) = unLoc (fdLName decl)
 
     at_names = mkNameSet (map at_fam_name ats)
 
-    at_defs_map :: NameEnv [LTyFamDefltEqn GhcRn]
+    at_defs_map :: NameEnv [LTyFamDefltDecl GhcRn]
     -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
     at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
                                           (at_def_tycon at_def) [at_def])
@@ -1511,61 +1512,61 @@ tcClassATs class_name cls ats at_defs
                   ; return (ATI fam_tc atd) }
 
 -------------------------
-tcDefaultAssocDecl :: TyCon                    -- ^ Family TyCon (not knot-tied)
-                   -> [LTyFamDefltEqn GhcRn]        -- ^ Defaults
-                   -> TcM (Maybe (KnotTied Type, SrcSpan))   -- ^ Type checked RHS
+tcDefaultAssocDecl ::
+     TyCon                                -- ^ Family TyCon (not knot-tied)
+  -> [LTyFamDefltDecl GhcRn]              -- ^ Defaults
+  -> TcM (Maybe (KnotTied Type, SrcSpan)) -- ^ Type checked RHS
 tcDefaultAssocDecl _ []
   = return Nothing  -- No default declaration
 
 tcDefaultAssocDecl _ (d1:_:_)
   = failWithTc (text "More than one default declaration for"
-                <+> ppr (feqn_tycon (unLoc d1)))
-
-tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
-                                             , feqn_pats = hs_tvs
-                                             , feqn_rhs = hs_rhs_ty })]
-  | HsQTvs { hsq_ext = imp_vars
-           , hsq_explicit = exp_vars } <- hs_tvs
+                <+> ppr (tyFamInstDeclName (unLoc d1)))
+
+tcDefaultAssocDecl fam_tc
+  [dL->L loc (TyFamInstDecl { tfid_eqn =
+         HsIB { hsib_ext  = imp_vars
+              , hsib_body = FamEqn { feqn_tycon = L _ tc_name
+                                   , feqn_bndrs = mb_expl_bndrs
+                                   , feqn_pats  = hs_pats
+                                   , feqn_rhs   = hs_rhs_ty }}})]
   = -- See Note [Type-checking default assoc decls]
     setSrcSpan loc $
     tcAddFamInstCtxt (text "default type instance") tc_name $
     do { traceTc "tcDefaultAssocDecl 1" (ppr tc_name)
        ; let fam_tc_name = tyConName fam_tc
-             fam_arity = length (tyConVisibleTyVars fam_tc)
+             vis_arity = length (tyConVisibleTyVars fam_tc)
+             vis_pats  = numVisibleArgs hs_pats
 
        -- Kind of family check
        ; ASSERT( fam_tc_name == tc_name )
          checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
        -- Arity check
-       ; checkTc (exp_vars `lengthIs` fam_arity)
-                 (wrongNumberOfParmsErr fam_arity)
+       ; checkTc (vis_pats == vis_arity)
+                 (wrongNumberOfParmsErr vis_arity)
 
        -- Typecheck RHS
-       ; let hs_pats = map (HsValArg . hsLTyVarBndrToType) exp_vars
-
-          -- NB: Use tcFamTyPats, not bindTyClTyVars. The latter expects to get
-          -- the LHsQTyVars used for declaring a tycon, but the names here
-          -- are different.
-
-          -- You might think we should pass in some AssocInstInfo, as we're looking
-          -- at an associated type. But this would be wrong, because an associated
-          -- type default LHS can mention *different* type variables than the
-          -- enclosing class. So it's treated more as a freestanding beast.
+       --
+       -- You might think we should pass in some AssocInstInfo, as we're looking
+       -- at an associated type. But this would be wrong, because an associated
+       -- type default LHS can mention *different* type variables than the
+       -- enclosing class. So it's treated more as a freestanding beast.
        ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc NotAssociated
-                                                    imp_vars exp_vars
+                                                    imp_vars (mb_expl_bndrs `orElse` [])
                                                     hs_pats hs_rhs_ty
 
-       ; let fam_tvs = tyConTyVars fam_tc
-             ppr_eqn = ppr_default_eqn pats rhs_ty
+       ; let fam_tvs  = tyConTyVars fam_tc
+             ppr_eqn  = ppr_default_eqn pats rhs_ty
+             pats_vis = tyConArgFlags fam_tc pats
        ; traceTc "tcDefaultAssocDecl 2" (vcat
            [ text "fam_tvs" <+> ppr fam_tvs
            , text "qtvs"    <+> ppr qtvs
            , text "pats"    <+> ppr pats
            , text "rhs_ty"  <+> ppr rhs_ty
            ])
-       ; pat_tvs <- traverse (extract_tv ppr_eqn) pats
-       ; check_all_distinct_tvs ppr_eqn pat_tvs
+       ; pat_tvs <- zipWithM (extract_tv ppr_eqn) pats pats_vis
+       ; check_all_distinct_tvs ppr_eqn $ zip pat_tvs pats_vis
        ; let subst = zipTvSubst pat_tvs (mkTyVarTys fam_tvs)
        ; pure $ Just (substTyUnchecked subst rhs_ty, loc)
            -- We also perform other checks for well-formedness and validity
@@ -1576,21 +1577,18 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
     -- variable. If so, return the underlying type variable, and if
     -- not, throw an error.
     -- See Note [Type-checking default assoc decls]
-    extract_tv :: SDoc   -- The pretty-printed default equation
-                         -- (only used for error message purposes)
-               -> Type   -- The particular type pattern from which to extract
-                         -- its underlying type variable
+    extract_tv :: SDoc    -- The pretty-printed default equation
+                          -- (only used for error message purposes)
+               -> Type    -- The particular type pattern from which to extract
+                          -- its underlying type variable
+               -> ArgFlag -- The visibility of the type pattern
+                          -- (only used for error message purposes)
                -> TcM TyVar
-    extract_tv ppr_eqn pat =
+    extract_tv ppr_eqn pat pat_vis =
       case getTyVar_maybe pat of
         Just tv -> pure tv
-        Nothing ->
-          -- Per Note [Type-checking default assoc decls], we already
-          -- know by this point that if any arguments in the default
-          -- instance aren't type variables, then they must be
-          -- invisible kind arguments. Therefore, always display the
-          -- error message with -fprint-explicit-kinds enabled.
-          failWithTc $ pprWithExplicitKindsWhen True $
+        Nothing -> failWithTc $
+          pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
           hang (text "Illegal argument" <+> quotes (ppr pat) <+> text "in:")
              2 (vcat [ppr_eqn, suggestion])
 
@@ -1598,22 +1596,21 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
     -- Checks that no type variables in an associated default declaration are
     -- duplicated. If that is the case, throw an error.
     -- See Note [Type-checking default assoc decls]
-    check_all_distinct_tvs :: SDoc    -- The pretty-printed default equation
-                                      -- (only used for error message purposes)
-                           -> [TyVar] -- The type variable arguments in the
-                                      -- associated default declaration
-                           -> TcM ()
-    check_all_distinct_tvs ppr_eqn tvs =
-      let dups = findDupsEq (==) tvs in
+    check_all_distinct_tvs ::
+         SDoc               -- The pretty-printed default equation (only used
+                            -- for error message purposes)
+      -> [(TyVar, ArgFlag)] -- The type variable arguments in the associated
+                            -- default declaration, along with their respective
+                            -- visibilities (the latter are only used for error
+                            -- message purposes)
+      -> TcM ()
+    check_all_distinct_tvs ppr_eqn pat_tvs_vis =
+      let dups = findDupsEq ((==) `on` fst) pat_tvs_vis in
       traverse_
-        (\d -> -- Per Note [Type-checking default assoc decls], we already
-               -- know by this point that if any arguments in the default
-               -- instance are duplicates, then they must be
-               -- invisible kind arguments. Therefore, always display the
-               -- error message with -fprint-explicit-kinds enabled.
-               failWithTc $ pprWithExplicitKindsWhen True $
+        (\d -> let (pat_tv, pat_vis) = NE.head d in failWithTc $
+               pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
                hang (text "Illegal duplicate variable"
-                       <+> quotes (ppr (NE.head d)) <+> text "in:")
+                       <+> quotes (ppr pat_tv) <+> text "in:")
                   2 (vcat [ppr_eqn, suggestion]))
         dups
 
@@ -1625,9 +1622,6 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
     suggestion :: SDoc
     suggestion = text "The arguments to" <+> quotes (ppr fam_tc)
              <+> text "must all be distinct type variables"
-tcDefaultAssocDecl _ [dL->L _ (XFamEqn _)] = panic "tcDefaultAssocDecl"
-tcDefaultAssocDecl _ [dL->L _ (FamEqn _ _ _ (XLHsQTyVars _) _ _)]
-  = panic "tcDefaultAssocDecl"
 tcDefaultAssocDecl _ [_]
   = panic "tcDefaultAssocDecl: Impossible Match" -- due to #15884
 
@@ -1653,11 +1647,10 @@ applying this substitution to the RHS.
 
 In order to create this substitution, we must first ensure that all of
 the arguments in the default instance consist of distinct type variables.
-This property has already been checked to some degree earlier in the compiler:
-RdrHsSyn.checkTyVars ensures that all visible type arguments are type
-variables, and RnTypes.bindLHsTyVarBndrs ensures that no visible type arguments
-are duplicated. But these only check /visible/ arguments, however, so we still
-must check the invisible kind arguments to see if these invariants are upheld.
+One might think that this is a simple task that could be implemented earlier
+in the compiler, perhaps in the parser or the renamer. However, there are some
+tricky corner cases that really do require the full power of typechecking to
+weed out, as the examples below should illustrate.
 
 First, we must check that all arguments are type variables. As a motivating
 example, consider this erroneous program (inspired by #11361):
@@ -1674,13 +1667,15 @@ example, this time taken from #13971:
 
    class C2 (a :: j) where
       type F2 (a :: j) (b :: k)
-      type F2 (x :: z) (y :: z) = z
+      type F2 (x :: z) y = SameKind x y
+   data SameKind :: k -> k -> Type
 
 All of the arguments in the default equation for `F2` are type variables, so
 that passes the first check. However, if we were to build this substitution,
 then both `j` and `k` map to `z`! In terms of visible kind application, it's as
-if we had written `type F2 @z @z x y = z`, which makes it clear that we have
-duplicated a use of `z`. Therefore, `F2`'s default is also rejected.
+if we had written `type F2 @z @z x y = SameKind @z x y`, which makes it clear
+that we have duplicated a use of `z` on the LHS. Therefore, `F2`'s default is
+also rejected.
 
 Since the LHS of an associated type family default is always just variables,
 it won't contain any tycons. Accordingly, the patterns used in the substitution
diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst
index ca34106eb4..f14271294c 100644
--- a/docs/users_guide/8.10.1-notes.rst
+++ b/docs/users_guide/8.10.1-notes.rst
@@ -54,6 +54,35 @@ Language
   See the `section on explicit kind quantification
   <#explicit-kind-quantification>`__ for more details.
 
+- Type variables in associated type family default declarations can now be
+  explicitly bound with a ``forall`` when :extension:`ExplicitForAll` is
+  enabled, as in the following example: ::
+
+    class C a where
+      type T a b
+      type forall a b. T a b = Either a b
+
+  This has a couple of knock-on consequences:
+
+  - Wildcard patterns are now permitted on the left-hand sides of default
+    declarations, whereas they were rejected by previous versions of GHC.
+
+  - It used to be the case that default declarations supported occurrences of
+    left-hand side arguments with higher-rank kinds, such as in the following
+    example: ::
+
+      class C a where
+        type T a (f :: forall k. k -> Type)
+        type T a (f :: forall k. k -> Type) = f Int
+
+    This will no longer work unless ``f`` is explicitly quantified with a
+    ``forall``, like so: ::
+
+      class C a where
+        type T a (f :: forall k. k -> Type)
+        type forall a (f :: forall k. k -> Type).
+             T a f = f Int
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index bce2bf8370..b1baa308c5 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -8166,14 +8166,15 @@ Note the following points:
 -  A default declaration is not permitted for an associated *data* type.
 
 -  The default declaration must mention only type *variables* on the
-   left hand side, and the right hand side must mention only type
+   left hand side, and type variables may not be repeated on the left-hand
+   side. The right hand side must mention only type
    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.
 
-   Because of this, unlike :ref:`assoc-inst`, explicit binding of type/kind
-   variables in default declarations is not permitted by
-   :extension:`ExplicitForAll`.
+   Like with :ref:`assoc-inst`, it is possible to explicitly bind type and kind
+   variables in default declarations with a ``forall`` by using the
+   :extension:`ExplicitForAll` language extension.
 
 -  Unlike the associated type family declaration itself, the type variables of
    the default instance are independent of those of the parent class.
@@ -8192,26 +8193,51 @@ Here are some examples:
         type instance F2 c d = c->d  -- OK; you don't have to use 'a' in the type instance
 
         type F3 a
-        type F3 [b] = b              -- BAD; only type variables allowed on the LHS
+        type F3 [b] = b              -- BAD; only type variables allowed on the
+                                             LHS, and the argument to F3 is
+                                             instantiated to [b], which is not
+                                             a bare type variable
 
-        type F4 a
-        type F4 b = a                -- BAD; 'a' is not in scope  in the RHS
+        type F4 x y
+        type F4 x x = x              -- BAD; the type variable x is repeated on
+                                             the LHS
 
-        type F5 a :: [k]
-        type F5 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
+        type F5 a
+        type F5 b = a                -- BAD; 'a' is not in scope  in the RHS
+
+        type F6 a :: [k]
+        type F6 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
                                             bound by an invisible kind pattern
                                             on the LHS
 
-        type F6 a
-        type F6 a =
+        type F7 a
+        type F7 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
+        type F8 (x :: a) :: [a]
+        type F8 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
                                             bound by the kind signature of the
                                             LHS type pattern
 
+        type F9 (a :: k)
+        type F9 a = Maybe a          -- BAD; the kind variable k is
+                                             instantiated to Type, which is not
+                                             a bare kind variable
+
+        type F10 (a :: j) (b :: k)
+        type F10 (a :: z) (b :: z)
+          = Proxy a                  -- BAD; the kind variable z is repeated,
+                                     -- as both j and k are instantiated to z
+
+        type F11 a b
+        type forall a b. F11 a b = a -- OK; LHS type variables can be
+                                        explicitly bound with 'forall'
+
+        type F12 (a :: k)
+        type F12 @k a = Proxy a      -- OK; visible kind application syntax is
+                                            permitted in default declarations
+
 .. _scoping-class-params:
 
 Scoping of class parameters
diff --git a/testsuite/tests/indexed-types/should_compile/T16110_Compile.hs b/testsuite/tests/indexed-types/should_compile/T16110_Compile.hs
new file mode 100644
index 0000000000..f05a4513fb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T16110_Compile.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16110_Compile where
+
+class C a where
+  type T1 a b
+  type forall a b. T1 a b = Either a b
+
+  type T2 a b
+  type forall x y. T2 x y = Either x y
+
+  type T3 a b
+  type forall. T3 _ _ = Int
diff --git a/testsuite/tests/indexed-types/should_compile/T16356_Compile1.hs b/testsuite/tests/indexed-types/should_compile/T16356_Compile1.hs
new file mode 100644
index 0000000000..74dee38ac4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T16356_Compile1.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16356_Compile1 where
+
+import Data.Kind (Type)
+
+data B (a :: k)
+
+type family FClosed :: k -> Type where
+  FClosed @k = B @k
+
+type family FOpen :: k -> Type
+type instance FOpen @k = B @k
+
+class FAssocClass k where
+  type FAssoc :: k -> Type
+
+instance FAssocClass k where
+  type FAssoc @k = B @k
+
+class FAssocDefaultClass k where
+  type FAssocDefault :: k -> Type
+  type FAssocDefault @k = B @k
diff --git a/testsuite/tests/indexed-types/should_compile/T16356_Compile2.hs b/testsuite/tests/indexed-types/should_compile/T16356_Compile2.hs
new file mode 100644
index 0000000000..46c8b00e1f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T16356_Compile2.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wunused-type-patterns #-}
+module T16356_Compile2 where
+
+class C (a :: j) where
+  type T1 (a :: j) (b :: k)
+  type T1 @j @_ a _ = Int
+
+  type T2 (a :: j) (b :: k)
+  type forall j (a :: j). T2 a _ = Int
+
+  type T3 (a :: j) (b :: k)
+  type forall j (a :: j). T3 @j @_ a _ = Int
diff --git a/testsuite/tests/indexed-types/should_compile/T16356_Compile2.stderr b/testsuite/tests/indexed-types/should_compile/T16356_Compile2.stderr
new file mode 100644
index 0000000000..3aceb43604
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T16356_Compile2.stderr
@@ -0,0 +1,18 @@
+
+T16356_Compile2.hs:10:12: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘j’
+
+T16356_Compile2.hs:10:17: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘a’
+
+T16356_Compile2.hs:13:15: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘j’
+
+T16356_Compile2.hs:13:18: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘a’
+
+T16356_Compile2.hs:16:15: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘j’
+
+T16356_Compile2.hs:16:18: warning: [-Wunused-type-patterns]
+    Defined but not used on the right hand side: type variable ‘a’
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index c268f2638d..9142b8edcd 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -286,4 +286,7 @@ test('T15711', normal, compile, ['-ddump-types'])
 test('T15852', normal, compile, ['-ddump-types'])
 test('T15764a', normal, compile, [''])
 test('T15740a', normal, compile, [''])
+test('T16110_Compile', normal, compile, [''])
+test('T16356_Compile1', normal, compile, [''])
+test('T16356_Compile2', normal, compile, [''])
 test('T16632', normal, compile, ['-Wunused-type-patterns -fdiagnostics-show-caret'])
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
index 8768c66613..b791ea7d82 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
@@ -1,6 +1,7 @@
 
-SimpleFail4.hs:10:11: error:
-    Unexpected type ‘Int’
-    In the default declaration for ‘S2’
-    A default declaration should have form
-      default S2 a = ...
+SimpleFail4.hs:10:3: error:
+    • Illegal argument ‘Int’ in:
+        ‘type S2 Int = Char’
+        The arguments to ‘S2’ must all be distinct type variables
+    • In the default type instance declaration for ‘S2’
+      In the class declaration for ‘C2’
diff --git a/testsuite/tests/indexed-types/should_fail/T16110_Fail1.hs b/testsuite/tests/indexed-types/should_fail/T16110_Fail1.hs
new file mode 100644
index 0000000000..2ec2332660
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail1.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16110_Fail1 where
+
+import Data.Kind
+
+class C (a :: Type) where
+  type T1 a b
+  type forall. T1 a b = Either a b
+
+  type T2 a b
+  type forall dup dup dup a b. T2 a b = Either a b
+
+  type T3 a b
+  type forall (a :: a) b. T3 a b = Either a b
+
+  type T4 a b
+  type forall (a :: k) k b. T4 a b = Either a b
diff --git a/testsuite/tests/indexed-types/should_fail/T16110_Fail1.stderr b/testsuite/tests/indexed-types/should_fail/T16110_Fail1.stderr
new file mode 100644
index 0000000000..2381655876
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail1.stderr
@@ -0,0 +1,18 @@
+
+T16110_Fail1.hs:10:19: error: Not in scope: type variable ‘a’
+
+T16110_Fail1.hs:10:21: error: Not in scope: type variable ‘b’
+
+T16110_Fail1.hs:10:32: error: Not in scope: type variable ‘a’
+
+T16110_Fail1.hs:10:34: error: Not in scope: type variable ‘b’
+
+T16110_Fail1.hs:13:15: error:
+    Conflicting definitions for ‘dup’
+    Bound at: T16110_Fail1.hs:13:15-17
+              T16110_Fail1.hs:13:19-21
+              T16110_Fail1.hs:13:23-25
+
+T16110_Fail1.hs:16:21: error: Not in scope: type variable ‘a’
+
+T16110_Fail1.hs:19:21: error: Not in scope: type variable ‘k’
diff --git a/testsuite/tests/indexed-types/should_fail/T16110_Fail2.hs b/testsuite/tests/indexed-types/should_fail/T16110_Fail2.hs
new file mode 100644
index 0000000000..fe0a9506ad
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail2.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16110_Fail2 where
+
+-- Ensure that kind variables don't leak into error messages if they're not
+-- pertitent to the issue at hand
+class C (a :: j) where
+  type T (a :: j) (b :: k) (c :: k)
+  type T a b b = Int
diff --git a/testsuite/tests/indexed-types/should_fail/T16110_Fail2.stderr b/testsuite/tests/indexed-types/should_fail/T16110_Fail2.stderr
new file mode 100644
index 0000000000..caa46af46a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail2.stderr
@@ -0,0 +1,7 @@
+
+T16110_Fail2.hs:9:3: error:
+    • Illegal duplicate variable ‘b’ in:
+        ‘type T a b b = Int’
+        The arguments to ‘T’ must all be distinct type variables
+    • In the default type instance declaration for ‘T’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T16110_Fail3.hs b/testsuite/tests/indexed-types/should_fail/T16110_Fail3.hs
new file mode 100644
index 0000000000..89b1f27bb6
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail3.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16110_Fail3 where
+
+import Data.Kind
+
+-- Ensure that kind variables don't leak into error messages if they're not
+-- pertitent to the issue at hand
+class C (a :: j) where
+  type T (a :: j) (b :: Type)
+  type T a Int = Int
diff --git a/testsuite/tests/indexed-types/should_fail/T16110_Fail3.stderr b/testsuite/tests/indexed-types/should_fail/T16110_Fail3.stderr
new file mode 100644
index 0000000000..0fdea6a63a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail3.stderr
@@ -0,0 +1,7 @@
+
+T16110_Fail3.hs:11:3: error:
+    • Illegal argument ‘Int’ in:
+        ‘type T a Int = Int’
+        The arguments to ‘T’ must all be distinct type variables
+    • In the default type instance declaration for ‘T’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T16356_Fail1.hs b/testsuite/tests/indexed-types/should_fail/T16356_Fail1.hs
new file mode 100644
index 0000000000..13a9cde2f3
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail1.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16356_Fail1 where
+
+import Data.Kind
+
+class C (a :: j) where
+  type T (a :: j)
+  type T @Type a = Maybe a
diff --git a/testsuite/tests/indexed-types/should_fail/T16356_Fail1.stderr b/testsuite/tests/indexed-types/should_fail/T16356_Fail1.stderr
new file mode 100644
index 0000000000..b354d1db00
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail1.stderr
@@ -0,0 +1,7 @@
+
+T16356_Fail1.hs:10:3: error:
+    • Illegal argument ‘*’ in:
+        ‘type T @* a = Maybe a’
+        The arguments to ‘T’ must all be distinct type variables
+    • In the default type instance declaration for ‘T’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T16356_Fail2.hs b/testsuite/tests/indexed-types/should_fail/T16356_Fail2.hs
new file mode 100644
index 0000000000..1ed53e02d9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail2.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16356_Fail2 where
+
+class C (a :: j) where
+  type T (a :: j) (b :: k)
+  type T @k @k a b = k
diff --git a/testsuite/tests/indexed-types/should_fail/T16356_Fail2.stderr b/testsuite/tests/indexed-types/should_fail/T16356_Fail2.stderr
new file mode 100644
index 0000000000..37f8159ae0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail2.stderr
@@ -0,0 +1,7 @@
+
+T16356_Fail2.hs:8:3: error:
+    • Illegal duplicate variable ‘k’ in:
+        ‘type T @k @k a b = k’
+        The arguments to ‘T’ must all be distinct type variables
+    • In the default type instance declaration for ‘T’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T16356_Fail3.hs b/testsuite/tests/indexed-types/should_fail/T16356_Fail3.hs
new file mode 100644
index 0000000000..da59f5399d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail3.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16356_Fail3 where
+
+import Data.Kind
+
+class C a where
+  type T1 a
+  type T1 @Type a = a
diff --git a/testsuite/tests/indexed-types/should_fail/T16356_Fail3.stderr b/testsuite/tests/indexed-types/should_fail/T16356_Fail3.stderr
new file mode 100644
index 0000000000..e8b59175f4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail3.stderr
@@ -0,0 +1,6 @@
+
+T16356_Fail3.hs:9:3: error:
+    • Cannot apply function of kind ‘* -> *’
+      to visible kind argument ‘Type’
+    • In the default type instance declaration for ‘T1’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index e154a31dd0..1ad9aa2504 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -153,3 +153,9 @@ test('T15870', normal, compile_fail, [''])
 test('T14887', normal, compile_fail, [''])
 test('T14230', normal, compile_fail, [''])
 test('T14230a', normal, compile_fail, [''])
+test('T16110_Fail1', normal, compile_fail, [''])
+test('T16110_Fail2', normal, compile_fail, [''])
+test('T16110_Fail3', normal, compile_fail, [''])
+test('T16356_Fail1', normal, compile_fail, [''])
+test('T16356_Fail2', normal, compile_fail, [''])
+test('T16356_Fail3', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr b/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr
index b310a79a6f..e76e8a89e2 100644
--- a/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr
+++ b/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr
@@ -1,6 +1,7 @@
 
-AssocTyDef02.hs:6:14:
-    Unexpected type ‘[b]’
-    In the default declaration for ‘Typ’
-    A default declaration should have form
-      default Typ a = ...
+AssocTyDef02.hs:6:5: error:
+    • Illegal argument ‘[b]’ in:
+        ‘type Typ [b] = Int’
+        The arguments to ‘Typ’ must all be distinct type variables
+    • In the default type instance declaration for ‘Typ’
+      In the class declaration for ‘Cls’
diff --git a/utils/haddock b/utils/haddock
-Subproject 65bbdfb6dc1b08f893187e1847985aad4505fcd
+Subproject 103a894471b18c9c3b0d9faffe2420e10b42068