Postpone associated tyfam default checks until after typechecking

Previously, associated type family defaults were validity-checked
during typechecking. Unfortunately, the error messages that these
checks produce run the risk of printing knot-tied type constructors,
which will cause GHC to diverge. In order to preserve the current
error message's descriptiveness, this patch postpones these validity
checks until after typechecking, which are now located in the new
function `GHC.Tc.Validity.checkValidAssocTyFamDeflt`.

Fixes #18648.

17 files changed, 198 insertions, 108 deletions

diff --git a/compiler/GHC/Core/Class.hs b/compiler/GHC/Core/Class.hs
index f5d24aaf3c..57e6defca6 100644
--- a/compiler/GHC/Core/Class.hs
+++ b/compiler/GHC/Core/Class.hs
@@ -8,7 +8,7 @@
 module GHC.Core.Class (
         Class,
         ClassOpItem,
-        ClassATItem(..),
+        ClassATItem(..), ATValidityInfo(..),
         ClassMinimalDef,
         DefMethInfo, pprDefMethInfo,
 
@@ -97,10 +97,21 @@ type DefMethInfo = Maybe (Name, DefMethSpec Type)
 
 data ClassATItem
   = ATI TyCon         -- See Note [Associated type tyvar names]
-        (Maybe (Type, SrcSpan))
+        (Maybe (Type, ATValidityInfo))
                       -- Default associated type (if any) from this template
                       -- Note [Associated type defaults]
 
+-- | Information about an associated type family default implementation. This
+-- is used solely for validity checking.
+-- See @Note [Type-checking default assoc decls]@ in "GHC.Tc.TyCl".
+data ATValidityInfo
+  = NoATVI               -- Used for associated type families that are imported
+                         -- from another module, for which we don't need to
+                         -- perform any validity checking.
+
+  | ATVI SrcSpan [Type]  -- Used for locally defined associated type families.
+                         -- The [Type] are the LHS patterns.
+
 type ClassMinimalDef = BooleanFormula Name -- Required methods
 
 data ClassBody
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index bd576b26cf..b7d8f62401 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -215,7 +215,7 @@ data IfaceClassOp
                  -- and the default method, are *not* quantified
                  -- over the class variables
 
-data IfaceAT = IfaceAT  -- See Class.ClassATItem
+data IfaceAT = IfaceAT  -- See GHC.Core.Class.ClassATItem
                   IfaceDecl          -- The associated type declaration
                   (Maybe IfaceType)  -- Default associated type instance, if any
 
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index ae6461ce3a..b6183eae47 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -791,7 +791,7 @@ tc_iface_decl _parent ignore_prags
                       Just def -> forkM (mk_at_doc tc)                 $
                                   extendIfaceTyVarEnv (tyConTyVars tc) $
                                   do { tc_def <- tcIfaceType def
-                                     ; return (Just (tc_def, noSrcSpan)) }
+                                     ; return (Just (tc_def, NoATVI)) }
                   -- Must be done lazily in case the RHS of the defaults mention
                   -- the type constructor being defined here
                   -- e.g.   type AT a; type AT b = AT [b]   #8002
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 50eeb60930..2cefd67c7f 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -52,7 +52,7 @@ import GHC.Core.Coercion
 import GHC.Tc.Types.Origin
 import GHC.Core.Type
 import GHC.Core.TyCo.Rep   -- for checkValidRoles
-import GHC.Core.TyCo.Ppr( pprTyVars, pprWithExplicitKindsWhen )
+import GHC.Core.TyCo.Ppr( pprTyVars )
 import GHC.Core.Class
 import GHC.Core.Coercion.Axiom
 import GHC.Core.TyCon
@@ -79,11 +79,9 @@ import GHC.Types.Basic
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
-import Data.Foldable
 import Data.Function ( on )
 import Data.Functor.Identity
 import Data.List
-import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
 import qualified Data.Set as Set
 import Data.Tuple( swap )
@@ -2393,9 +2391,9 @@ tcClassATs class_name cls ats at_defs
 
 -------------------------
 tcDefaultAssocDecl ::
-     TyCon                                -- ^ Family TyCon (not knot-tied)
-  -> [LTyFamDefltDecl GhcRn]              -- ^ Defaults
-  -> TcM (Maybe (KnotTied Type, SrcSpan)) -- ^ Type checked RHS
+     TyCon                                       -- ^ Family TyCon (not knot-tied)
+  -> [LTyFamDefltDecl GhcRn]                     -- ^ Defaults
+  -> TcM (Maybe (KnotTied Type, ATValidityInfo)) -- ^ Type checked RHS
 tcDefaultAssocDecl _ []
   = return Nothing  -- No default declaration
 
@@ -2436,73 +2434,27 @@ tcDefaultAssocDecl fam_tc
                                                     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
-             pats_vis = tyConArgFlags fam_tc pats
+       ; let fam_tvs = tyConTyVars fam_tc
        ; traceTc "tcDefaultAssocDecl 2" (vcat
-           [ text "fam_tvs" <+> ppr fam_tvs
+           [ text "hs_pats"   <+> ppr hs_pats
+           , text "hs_rhs_ty" <+> ppr hs_rhs_ty
+           , text "fam_tvs" <+> ppr fam_tvs
            , text "qtvs"    <+> ppr qtvs
-           , text "pats"    <+> ppr pats
-           , text "rhs_ty"  <+> ppr rhs_ty
+             -- NB: Do *not* print `pats` or rhs_ty here, as they can mention
+             -- knot-tied TyCons. See #18648.
            ])
-       ; cpt_tvs <- zipWithM (extract_tv ppr_eqn) pats pats_vis
-       ; check_all_distinct_tvs ppr_eqn $ zip cpt_tvs pats_vis
-       ; let subst = zipTvSubst cpt_tvs (mkTyVarTys fam_tvs)
-       ; pure $ Just (substTyUnchecked subst rhs_ty, loc)
-           -- We also perform other checks for well-formedness and validity
-           -- later, in checkValidClass
+       ; let subst = case traverse getTyVar_maybe pats of
+                       Just cpt_tvs -> zipTvSubst cpt_tvs (mkTyVarTys fam_tvs)
+                       Nothing      -> emptyTCvSubst
+                       -- The Nothing case can only be reached in invalid
+                       -- associated type family defaults. In such cases, we
+                       -- simply create an empty substitution and let GHC fall
+                       -- over later, in GHC.Tc.Validity.checkValidAssocTyFamDeflt.
+                       -- See Note [Type-checking default assoc decls].
+       ; pure $ Just (substTyUnchecked subst rhs_ty, ATVI loc pats)
+           -- We perform checks for well-formedness and validity later, in
+           -- GHC.Tc.Validity.checkValidAssocTyFamDeflt.
      }
-  where
-    -- Checks that a pattern on the LHS of a default is a type
-    -- 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
-               -> ArgFlag -- The visibility of the type pattern
-                          -- (only used for error message purposes)
-               -> TcM TyVar
-    extract_tv ppr_eqn pat pat_vis =
-      case getTyVar_maybe pat of
-        Just tv -> pure tv
-        Nothing -> failWithTc $
-          pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
-          hang (text "Illegal argument" <+> quotes (ppr pat) <+> text "in:")
-             2 (vcat [ppr_eqn, suggestion])
-
-
-    -- 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, 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 cpt_tvs_vis =
-      let dups = findDupsEq ((==) `on` fst) cpt_tvs_vis in
-      traverse_
-        (\d -> let (pat_tv, pat_vis) = NE.head d in failWithTc $
-               pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
-               hang (text "Illegal duplicate variable"
-                       <+> quotes (ppr pat_tv) <+> text "in:")
-                  2 (vcat [ppr_eqn, suggestion]))
-        dups
-
-    ppr_default_eqn :: [Type] -> Type -> SDoc
-    ppr_default_eqn pats rhs_ty =
-      quotes (text "type" <+> ppr (mkTyConApp fam_tc pats)
-                <+> equals <+> ppr rhs_ty)
-
-    suggestion :: SDoc
-    suggestion = text "The arguments to" <+> quotes (ppr fam_tc)
-             <+> text "must all be distinct type variables"
-
 
 {- Note [Type-checking default assoc decls]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2513,24 +2465,29 @@ Consider this default declaration for an associated type
       type F (x :: j) y = Proxy x -> y
 
 Note that the class variable 'a' doesn't scope over the default assoc
-decl (rather oddly I think), and (less oddly) neither does the second
-argument 'b' of the associated type 'F', or the kind variable 'k'.
-Instead, the default decl is treated more like a top-level type
-instance.
-
-However we store the default rhs (Proxy x -> y) in F's TyCon, using
-F's own type variables, so we need to convert it to (Proxy a -> b).
-We do this by creating a substitution [j |-> k, x |-> a, b |-> y] and
-applying this substitution to the RHS.
+decl, nor do the type variables `k` and `b`. Instead, the default decl is
+treated more like a top-level type instance. However, we store the default rhs
+(Proxy x -> y) in F's TyCon, using F's own type variables, so we need to
+convert it to (Proxy a -> b). We do this in the tcDefaultAssocDecl function by
+creating a substitution [j |-> k, x |-> a, b |-> y] and 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.
-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.
+Checking for this property proves surprisingly tricky. Three potential places
+where GHC could check for this property include:
+
+1. Before typechecking (in the parser or renamer)
+2. During typechecking (in tcDefaultAssocDecl)
+3. After typechecking (using GHC.Tc.Validity)
+
+Currently, GHC picks option (3) and implements this check using
+GHC.Tc.Validity.checkValidAssocTyFamDeflt. GHC previously used options (1) and
+(2), but neither option quite worked out for reasons that we will explain
+shortly.
 
-First, we must check that all arguments are type variables. As a motivating
+The first thing that checkValidAssocTyFamDeflt does is check that all arguments
+in an associated type family default are type variables. As a motivating
 example, consider this erroneous program (inspired by #11361):
 
    class C a where
@@ -2538,10 +2495,13 @@ example, consider this erroneous program (inspired by #11361):
       type F x        b = x
 
 If you squint, you'll notice that the kind of `x` is actually Type. However,
-we cannot substitute from [Type |-> k], so we reject this default.
+we cannot substitute from [Type |-> k], so we reject this default. This also
+explains why GHC no longer implements option (1) above, since figuring out that
+`x`'s kind is Type would be much more difficult without the knowledge that the
+typechecker provides.
 
-Next, we must check that all arguments are distinct. Here is another offending
-example, this time taken from #13971:
+Next, checkValidAssocTyFamDeflt checks that all arguments are distinct. Here is
+another offending example, this time taken from #13971:
 
    class C2 (a :: j) where
       type F2 (a :: j) (b :: k)
@@ -2555,10 +2515,37 @@ 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
-won't actually be knot-tied, even though we're in the knot. This is too
-delicate for my taste, but it works.
+There is one more design consideration in play here: what error message should
+checkValidAssocTyFamDeflt produce if one of its checks fails? Ideally, it would
+be something like this:
+
+  Illegal duplicate variable ‘z’ in:
+    ‘type F2 @z @z x y = ...’
+    The arguments to ‘F2’ must all be distinct type variables
+
+This requires printing out the arguments to the associated type family. This
+can be dangerous, however. Consider this example, adapted from #18648:
+
+  class C3 a where
+     type F3 a
+     type F3 (F3 a) = a
+
+F3's default is illegal, since its argument is not a bare type variable. But
+note that when we typecheck F3's default, the F3 type constructor is knot-tied.
+Therefore, if we print the type `F3 a` in an error message, GHC will diverge!
+This is the reason why GHC no longer implements option (2) above and instead
+waits until /after/ typechecking has finished, at which point the typechecker
+knot has been worked out.
+
+As one final point, one might worry that the typechecker knot could cause the
+substitution that tcDefaultAssocDecl creates to diverge, but this is not the
+case. Since the LHS of a valid associated type family default is always just
+variables, it won't contain any tycons. Accordingly, the patterns used in the
+substitution won't actually be knot-tied, even though we're in the knot. (This
+is too delicate for my taste, but it works.) If we're dealing with /invalid/
+default, such as F3's above, then we simply create an empty substitution and
+rely on checkValidAssocTyFamDeflt throwing an error message afterwards before
+any damage is done.
 -}
 
 {- *********************************************************************
@@ -4293,10 +4280,14 @@ checkValidClass cls
                         -- since there is no possible ambiguity (#10020)
 
              -- Check that any default declarations for associated types are valid
-           ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
-             setSrcSpan loc $
-             tcAddFamInstCtxt (text "default type instance") (getName fam_tc) $
-             checkValidTyFamEqn fam_tc fam_tvs (mkTyVarTys fam_tvs) rhs }
+           ; whenIsJust m_dflt_rhs $ \ (rhs, at_validity_info) ->
+             case at_validity_info of
+               NoATVI -> pure ()
+               ATVI loc pats ->
+                 setSrcSpan loc $
+                 tcAddFamInstCtxt (text "default type instance") (getName fam_tc) $
+                 do { checkValidAssocTyFamDeflt fam_tc pats
+                    ; checkValidTyFamEqn fam_tc fam_tvs (mkTyVarTys fam_tvs) rhs }}
         where
           fam_tvs = tyConTyVars fam_tc
 
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 678f2c6fc8..fba45562b7 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -14,7 +14,7 @@ module GHC.Tc.Validity (
   checkValidInstance, checkValidInstHead, validDerivPred,
   checkTySynRhs,
   checkValidCoAxiom, checkValidCoAxBranch,
-  checkValidTyFamEqn, checkConsistentFamInst,
+  checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
   badATErr, arityErr,
   checkTyConTelescope,
   allDistinctTyVars
@@ -73,6 +73,7 @@ import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
 import Data.Foldable
+import Data.Function
 import Data.List        ( (\\), nub )
 import qualified Data.List.NonEmpty as NE
 
@@ -2117,6 +2118,68 @@ checkValidTyFamEqn fam_tc qvs typats rhs
        ; unless undecidable_ok $
          mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
 
+-- | Checks that an associated type family default:
+--
+-- 1. Only consists of arguments that are bare type variables, and
+--
+-- 2. Has a distinct type variable in each argument.
+--
+-- See @Note [Type-checking default assoc decls]@ in "GHC.Tc.TyCl".
+checkValidAssocTyFamDeflt :: TyCon  -- ^ of the type family
+                          -> [Type] -- ^ Type patterns
+                          -> TcM ()
+checkValidAssocTyFamDeflt fam_tc pats =
+  do { cpt_tvs <- zipWithM extract_tv pats pats_vis
+     ; check_all_distinct_tvs $ zip cpt_tvs pats_vis }
+  where
+    pats_vis :: [ArgFlag]
+    pats_vis = tyConArgFlags fam_tc pats
+
+    -- Checks that a pattern on the LHS of a default is a type
+    -- variable. If so, return the underlying type variable, and if
+    -- not, throw an error.
+    -- See Note [Type-checking default assoc decls]
+    extract_tv :: 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 pat pat_vis =
+      case getTyVar_maybe pat of
+        Just tv -> pure tv
+        Nothing -> failWithTc $
+          pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
+          hang (text "Illegal argument" <+> quotes (ppr pat) <+> text "in:")
+             2 (vcat [ppr_eqn, suggestion])
+
+    -- 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 ::
+         [(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 cpt_tvs_vis =
+      let dups = findDupsEq ((==) `on` fst) cpt_tvs_vis in
+      traverse_
+        (\d -> let (pat_tv, pat_vis) = NE.head d in failWithTc $
+               pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $
+               hang (text "Illegal duplicate variable"
+                       <+> quotes (ppr pat_tv) <+> text "in:")
+                  2 (vcat [ppr_eqn, suggestion]))
+        dups
+
+    ppr_eqn :: SDoc
+    ppr_eqn =
+      quotes (text "type" <+> ppr (mkTyConApp fam_tc pats)
+                <+> equals <+> text "...")
+
+    suggestion :: SDoc
+    suggestion = text "The arguments to" <+> quotes (ppr fam_tc)
+             <+> text "must all be distinct type variables"
+
 -- Make sure that each type family application is
 --   (1) strictly smaller than the lhs,
 --   (2) mentions no type variable more often than the lhs, and
diff --git a/testsuite/tests/indexed-types/should_compile/T11361a.stderr b/testsuite/tests/indexed-types/should_compile/T11361a.stderr
index a7d5ad16af..ae2b832380 100644
--- a/testsuite/tests/indexed-types/should_compile/T11361a.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T11361a.stderr
@@ -1,7 +1,7 @@
 
 T11361a.hs:7:3: error:
     • Illegal argument ‘*’ in:
-        ‘type F @(*) x = x’
+        ‘type F @(*) x = ...’
         The arguments to ‘F’ must all be distinct type variables
     • In the default type instance declaration for ‘F’
       In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
index b791ea7d82..d23b24d824 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
@@ -1,7 +1,7 @@
 
 SimpleFail4.hs:10:3: error:
     • Illegal argument ‘Int’ in:
-        ‘type S2 Int = Char’
+        ‘type S2 Int = ...’
         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/T13971.stderr b/testsuite/tests/indexed-types/should_fail/T13971.stderr
index fe4ab4ca3c..2c46366295 100644
--- a/testsuite/tests/indexed-types/should_fail/T13971.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13971.stderr
@@ -1,7 +1,7 @@
 
 T13971.hs:7:3: error:
     • Illegal argument ‘*’ in:
-        ‘type T @{k} @(*) a = Int’
+        ‘type T @{k} @(*) 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/T13971b.stderr b/testsuite/tests/indexed-types/should_fail/T13971b.stderr
index cf64125fbb..afbd15d028 100644
--- a/testsuite/tests/indexed-types/should_fail/T13971b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13971b.stderr
@@ -1,7 +1,7 @@
 
 T13971b.hs:9:3: error:
     • Illegal duplicate variable ‘k’ in:
-        ‘type T @k @k a b = k’
+        ‘type T @k @k a b = ...’
         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_Fail2.stderr b/testsuite/tests/indexed-types/should_fail/T16110_Fail2.stderr
index caa46af46a..b901c28926 100644
--- a/testsuite/tests/indexed-types/should_fail/T16110_Fail2.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail2.stderr
@@ -1,7 +1,7 @@
 
 T16110_Fail2.hs:9:3: error:
     • Illegal duplicate variable ‘b’ in:
-        ‘type T a b b = Int’
+        ‘type T a b b = ...’
         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.stderr b/testsuite/tests/indexed-types/should_fail/T16110_Fail3.stderr
index 0fdea6a63a..a84cf1a95f 100644
--- a/testsuite/tests/indexed-types/should_fail/T16110_Fail3.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T16110_Fail3.stderr
@@ -1,7 +1,7 @@
 
 T16110_Fail3.hs:11:3: error:
     • Illegal argument ‘Int’ in:
-        ‘type T a Int = Int’
+        ‘type T a 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.stderr b/testsuite/tests/indexed-types/should_fail/T16356_Fail1.stderr
index 74935362b6..ce246c59fd 100644
--- a/testsuite/tests/indexed-types/should_fail/T16356_Fail1.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail1.stderr
@@ -1,7 +1,7 @@
 
 T16356_Fail1.hs:10:3: error:
     • Illegal argument ‘*’ in:
-        ‘type T @(*) a = Maybe a’
+        ‘type T @(*) 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.stderr b/testsuite/tests/indexed-types/should_fail/T16356_Fail2.stderr
index 37f8159ae0..3b1644d494 100644
--- a/testsuite/tests/indexed-types/should_fail/T16356_Fail2.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T16356_Fail2.stderr
@@ -1,7 +1,7 @@
 
 T16356_Fail2.hs:8:3: error:
     • Illegal duplicate variable ‘k’ in:
-        ‘type T @k @k a b = k’
+        ‘type T @k @k a b = ...’
         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/T18648.hs b/testsuite/tests/indexed-types/should_fail/T18648.hs
new file mode 100644
index 0000000000..92502b77c8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T18648.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+module T18648 where
+
+class Foo1 a where
+   type Bar1 a
+   type Bar1 (f a) = Bar1 a
+
+class Foo2 a where
+   type Bar2 a
+   type Bar2 (Bar2 a) = a
diff --git a/testsuite/tests/indexed-types/should_fail/T18648.stderr b/testsuite/tests/indexed-types/should_fail/T18648.stderr
new file mode 100644
index 0000000000..0fbb014b50
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T18648.stderr
@@ -0,0 +1,14 @@
+
+T18648.hs:6:4: error:
+    • Illegal argument ‘f a’ in:
+        ‘type Bar1 (f a) = ...’
+        The arguments to ‘Bar1’ must all be distinct type variables
+    • In the default type instance declaration for ‘Bar1’
+      In the class declaration for ‘Foo1’
+
+T18648.hs:10:4: error:
+    • Illegal argument ‘Bar2 a’ in:
+        ‘type Bar2 (Bar2 a) = ...’
+        The arguments to ‘Bar2’ must all be distinct type variables
+    • In the default type instance declaration for ‘Bar2’
+      In the class declaration for ‘Foo2’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index a419610f9e..428ab8d4f1 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -162,3 +162,4 @@ test('T16356_Fail3', normal, compile_fail, [''])
 test('T17008a', normal, compile_fail, ['-fprint-explicit-kinds'])
 test('T13571', normal, compile_fail, [''])
 test('T13571a', normal, compile_fail, [''])
+test('T18648', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr b/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr
index e76e8a89e2..79c3e86c67 100644
--- a/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr
+++ b/testsuite/tests/typecheck/should_fail/AssocTyDef02.stderr
@@ -1,7 +1,7 @@
 
 AssocTyDef02.hs:6:5: error:
     • Illegal argument ‘[b]’ in:
-        ‘type Typ [b] = Int’
+        ‘type Typ [b] = ...’
         The arguments to ‘Typ’ must all be distinct type variables
     • In the default type instance declaration for ‘Typ’
       In the class declaration for ‘Cls’