From 1eed645c8b03b19a14cf58d9be5317cb81cbd30a Mon Sep 17 00:00:00 2001
From: sheaf <sam.derbyshire@gmail.com>
Date: Tue, 19 Sep 2023 13:10:21 +0200
Subject: [PATCH] Validity: refactor treatment of data families

This commit refactors the reporting of unused type variables in type
and data family instances to be more principled. This avoids ad-hoc
logic in the treatment of data family instances.
---
 compiler/GHC/Rename/Module.hs                 |   9 +-
 compiler/GHC/Tc/Errors/Ppr.hs                 |  59 +++++++-
 compiler/GHC/Tc/Errors/Types.hs               |  40 +++++-
 compiler/GHC/Tc/Validity.hs                   | 134 +++++++-----------
 compiler/GHC/Utils/Outputable.hs              |  10 ++
 .../should_fail/ExplicitForAllFams4a.stderr   |  10 +-
 .../should_fail/ExplicitForAllFams4b.stderr   |  52 +++----
 .../should_fail/SimpleFail13.stderr           |  12 ++
 .../indexed-types/should_fail/T17008a.stderr  |   8 +-
 .../indexed-types/should_fail/T7536.stderr    |   8 +-
 .../tests/typecheck/should_fail/T23734.stderr |  22 +--
 .../tests/typecheck/should_fail/T23778.stderr |   4 +-
 12 files changed, 221 insertions(+), 147 deletions(-)

diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index a13e6a4e70c3..ecf1a3250a41 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -71,9 +71,9 @@ import GHC.Core.DataCon ( isSrcStrict )
 
 import Control.Monad
 import Control.Arrow ( first )
-import Data.Foldable ( toList )
+import Data.Foldable ( toList, for_ )
 import Data.List ( mapAccumL )
-import Data.List.NonEmpty ( NonEmpty(..), head )
+import Data.List.NonEmpty ( NonEmpty(..), head, nonEmpty )
 import Data.Maybe ( isNothing, fromMaybe, mapMaybe )
 import qualified Data.Set as Set ( difference, fromList, toList, null )
 import GHC.Types.GREInfo (ConInfo, mkConInfo, conInfoFields)
@@ -729,9 +729,10 @@ rnFamEqn doc atfi
                && not (cls_tkv `elemNameSet` pat_fvs)
                     -- ...but not bound on the LHS.
              bad_tvs = filter improperly_scoped inst_head_tvs
-       ; unless (null bad_tvs) $ addErr $
+       ; for_ (nonEmpty bad_tvs) $ \ ne_bad_tvs ->
+           addErr $
            TcRnIllegalInstance $ IllegalFamilyInstance $
-             FamInstRHSOutOfScopeTyVars Nothing bad_tvs
+             FamInstRHSOutOfScopeTyVars Nothing ne_bad_tvs
 
        ; let eqn_fvs = rhs_fvs `plusFV` pat_fvs
              -- See Note [Type family equations and occurrences]
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 223e2d5bafb5..e6f93b7f3a16 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -6181,7 +6181,7 @@ pprIllegalFamilyInstance = \case
     hang (text "Mismatched type name in type family instance.")
        2 (vcat [ text "Expected:" <+> ppr fam_tc_name
                , text "  Actual:" <+> ppr eqn_tc_name ])
-  FamInstRHSOutOfScopeTyVars mb_dodgy tvs ->
+  FamInstRHSOutOfScopeTyVars mb_dodgy (NE.toList -> tvs) ->
     hang (text "Out of scope type variable" <> plural tvs
          <+> pprWithCommas (quotes . ppr) tvs
          <+> text "in the RHS of a family instance.")
@@ -6194,13 +6194,60 @@ pprIllegalFamilyInstance = \case
     mk_extra = case mb_dodgy of
       Nothing -> empty
       Just (fam_tc, pats, dodgy_tvs) ->
-        ppWhen (any (`elemVarSetByKey` dodgy_tvs) (map nameUnique tvs)) $
+        ppWhen (any (`elemVarSetByKey` dodgy_tvs) (fmap nameUnique tvs)) $
           hang (text "The real LHS (expanding synonyms) is:")
              2 (pprTypeApp fam_tc (map expandTypeSynonyms pats))
-  FamInstLHSUnusedBoundTyVars tvs ->
-    hang (text "Type variable" <> plural tvs <+> pprQuotedList tvs
-          <+> isOrAre tvs <+> text "bound by a forall,")
-       2 (text "but not used in the family instance.")
+  FamInstLHSUnusedBoundTyVars (NE.toList -> bad_qtvs) ->
+    vcat [ not_bound_msg, not_used_msg, dodgy_msg ]
+    where
+
+      -- Filter to only keep user-written variables,
+      -- unless none were user-written in which case we report all of them
+      -- (as we need to report an error).
+      filter_user tvs
+        = map ifiqtv
+        $ case filter ifiqtv_user_written tvs of { [] -> tvs ; qvs -> qvs }
+
+      (not_bound, not_used, dodgy)
+        = case foldr acc_tv ([], [], []) bad_qtvs of
+            (nb, nu, d) -> (filter_user nb, filter_user nu, filter_user d)
+
+      acc_tv tv (nb, nu, d) = case ifiqtv_reason tv of
+        InvalidFamInstQTvNotUsedInRHS   -> (nb, tv : nu, d)
+        InvalidFamInstQTvNotBoundInPats -> (tv : nb, nu, d)
+        InvalidFamInstQTvDodgy          -> (nb, nu, tv : d)
+
+      -- Error message for type variables not bound in LHS patterns.
+      not_bound_msg
+        | null not_bound
+        = empty
+        | otherwise
+        = vcat [ text "The type variable" <> plural not_bound <+> pprQuotedList not_bound
+            <+> isOrAre not_bound <+> text "bound by a forall,"
+              , text "but" <+> doOrDoes not_bound <+> text "not appear in any of the LHS patterns of the family instance." ]
+
+      -- Error message for type variables bound by a forall but not used
+      -- in the RHS.
+      not_used_msg =
+        if null not_used
+        then empty
+        else text "The type variable" <> plural not_used <+> pprQuotedList not_used
+             <+> isOrAre not_used <+> text "bound by a forall," $$
+             text "but" <+> itOrThey not_used <+>
+             isOrAre not_used <> text "n't used in the family instance."
+
+      -- Error message for dodgy type variables.
+      -- See Note [Dodgy binding sites in type family instances] in GHC.Tc.Validity.
+      dodgy_msg
+        | null dodgy
+        = empty
+        | otherwise
+        = hang (text "Dodgy type variable" <> plural dodgy <+> pprQuotedList dodgy
+               <+> text "in the LHS of a family instance:")
+             2 (text "the type variable" <> plural dodgy <+> pprQuotedList dodgy
+                <+> text "syntactically appear" <> singular dodgy <+> text "in LHS patterns,"
+               $$ text "but" <+> itOrThey dodgy <+> doOrDoes dodgy <> text "n't appear in an injective position.")
+
 
 illegalFamilyInstanceHints :: IllegalFamilyInstanceReason -> [GhcHint]
 illegalFamilyInstanceHints = \case
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 5c77de7b7c1e..9c1f8a2fb879 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -138,6 +138,7 @@ module GHC.Tc.Errors.Types (
   , IllegalHasFieldInstance(..)
   , CoverageProblem(..), FailedCoverageCondition(..)
   , IllegalFamilyInstanceReason(..)
+  , InvalidFamInstQTv(..), InvalidFamInstQTvReason(..)
   , InvalidAssoc(..), InvalidAssocInstance(..)
   , InvalidAssocDefault(..), AssocDefaultBadArgs(..)
 
@@ -181,7 +182,7 @@ import GHC.Types.Avail
 import GHC.Types.Hint (UntickedPromotedThing(..))
 import GHC.Types.ForeignCall (CLabelString)
 import GHC.Types.Id.Info ( RecSelParent(..) )
-import GHC.Types.Name (Name, OccName, getSrcLoc, getSrcSpan)
+import GHC.Types.Name (NamedThing(..), Name, OccName, getSrcLoc, getSrcSpan)
 import qualified GHC.Types.Name.Occurrence as OccName
 import GHC.Types.Name.Reader
 import GHC.Types.SourceFile (HsBootOrSig(..))
@@ -4653,14 +4654,47 @@ data IllegalFamilyInstanceReason
         -- ^ family 'TyCon', arguments, and set of "dodgy" type variables
         -- See Note [Dodgy binding sites in type family instances]
         -- in GHC.Tc.Validity
-      ![Name] -- ^ the out-of-scope type variables
+      !(NE.NonEmpty Name) -- ^ the out-of-scope type variables
 
   | FamInstLHSUnusedBoundTyVars
-      ![Name] -- ^ the unused bound type variables
+      !(NE.NonEmpty InvalidFamInstQTv) -- ^ the unused bound type variables
 
   | InvalidAssoc !InvalidAssoc
   deriving Generic
 
+-- | A quantified type variable in a type or data family equation that
+-- is either not bound in any LHS patterns or not used in the RHS (or both).
+data InvalidFamInstQTv
+  = InvalidFamInstQTv
+    { ifiqtv :: TcTyVar
+    , ifiqtv_user_written :: Bool
+       -- ^ Did the user write this type variable, or was introduced by GHC?
+       -- For example: with @-XPolyKinds@, in @type instance forall a. F = ()@,
+       -- we have a user-written @a@ but GHC introduces a kind variable @k@
+       -- as well. See #23734.
+    , ifiqtv_reason       :: InvalidFamInstQTvReason
+      -- ^ For what reason was the quantified type variable invalid?
+    }
+
+data InvalidFamInstQTvReason
+  -- | A dodgy binder, i.e. a variable that syntactically appears in
+  -- LHS patterns but only in non-injective positions.
+  --
+  -- See Note [Dodgy binding sites in type family instances]
+  -- in GHC.Tc.Validity.
+  = InvalidFamInstQTvDodgy
+  -- | A quantified type variable in a type or data family equation
+  -- that is not bound in any LHS patterns.
+  | InvalidFamInstQTvNotBoundInPats
+  -- | A quantified type variable in a type or data family equation
+  -- that is not used on the RHS.
+  | InvalidFamInstQTvNotUsedInRHS
+
+-- The 'check_tvs' function in 'GHC.Tc.Validity.checkFamPatBinders'
+-- uses 'getSrcSpan', so this 'NamedThing' instance is convenient.
+instance NamedThing InvalidFamInstQTv where
+  getName = getName . ifiqtv
+
 data InvalidAssoc
   -- | An invalid associated family instance.
   --
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index b2f7830a52ff..797ee56e6146 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -47,7 +47,6 @@ import GHC.Core.Unify ( typesAreApart, tcMatchTyX_BM, BindFlag(..) )
 import GHC.Core.Coercion
 import GHC.Core.Coercion.Axiom
 import GHC.Core.Class
-import GHC.Core.DataCon
 import GHC.Core.TyCon
 import GHC.Core.Predicate
 import GHC.Core.TyCo.FVs
@@ -85,6 +84,8 @@ import Control.Monad
 import Data.Foldable
 import Data.Function
 import Data.List        ( (\\) )
+import qualified Data.List.NonEmpty as NE
+import Data.List.NonEmpty ( NonEmpty(..) )
 
 {-
 ************************************************************************
@@ -2164,6 +2165,10 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
 -- Check that a "type instance" is well-formed (which includes decidability
 -- unless -XUndecidableInstances is given).
 --
+-- See also the separate 'checkFamPatBinders' which performs scoping checks
+-- on a type family equation.
+-- (It's separate because it expects 'TyFamEqnValidityInfo', which comes from a
+-- separate place e.g. for associated type defaults.)
 checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM ()
 checkValidCoAxBranch fam_tc
                     (CoAxBranch { cab_lhs = typats
@@ -2174,6 +2179,11 @@ checkValidCoAxBranch fam_tc
 -- | Do validity checks on a type family equation, including consistency
 -- with any enclosing class instance head, termination, and lack of
 -- polytypes.
+--
+-- See also the separate 'checkFamPatBinders' which performs scoping checks
+-- on a type family equation.
+-- (It's separate because it expects 'TyFamEqnValidityInfo', which comes from a
+-- separate place e.g. for associated type defaults.)
 checkValidTyFamEqn :: TyCon    -- ^ of the type family
                    -> [Type]   -- ^ Type patterns
                    -> Type     -- ^ Rhs
@@ -2297,6 +2307,15 @@ checkTyFamEqnValidityInfo fam_tc = \ case
     setSrcSpan loc $
     checkFamPatBinders fam_tc qtvs non_user_tvs pats rhs
 
+-- | Check binders for a type or data family declaration.
+--
+-- Specifically, this function checks for:
+--
+--  - type variables used on the RHS but not bound (explicitly or implicitly)
+--    in the LHS,
+--  - variables bound by a forall in the LHS but not used in the RHS.
+--
+-- See Note [Check type family instance binders].
 checkFamPatBinders :: TyCon
                    -> [TcTyVar]   -- ^ Bound on LHS of family instance
                    -> TyVarSet    -- ^ non-user-written tyvars
@@ -2313,7 +2332,7 @@ checkFamPatBinders fam_tc qtvs non_user_tvs pats rhs
               , text "cpt_tvs:" <+> ppr cpt_tvs
               , text "inj_cpt_tvs:" <+> ppr inj_cpt_tvs
               , text "bad_rhs_tvs:" <+> ppr bad_rhs_tvs
-              , text "bad_qtvs:" <+> ppr bad_qtvs ]
+              , text "bad_qtvs:" <+> ppr (map ifiqtv bad_qtvs) ]
 
          -- Check for implicitly-bound tyvars, mentioned on the
          -- RHS but not bound on the LHS
@@ -2321,36 +2340,18 @@ checkFamPatBinders fam_tc qtvs non_user_tvs pats rhs
          --    data family D Int = MkD (forall (a::k). blah)
          -- In both cases, 'k' is not bound on the LHS, but is used on the RHS
          -- We catch the former in kcDeclHeader, and the latter right here
-         -- See Note [Check type-family instance binders]
+         -- See Note [Check type family instance binders]
        ; check_tvs (FamInstRHSOutOfScopeTyVars (Just (fam_tc, pats, dodgy_tvs)))
-                   bad_rhs_tvs
+                   (map tyVarName bad_rhs_tvs)
 
          -- Check for explicitly forall'd variable that is not bound on LHS
          --    data instance forall a.  T Int = MkT Int
          -- See Note [Unused explicitly bound variables in a family pattern]
-         -- See Note [Check type-family instance binders]
+         -- See Note [Check type family instance binders]
        ; check_tvs FamInstLHSUnusedBoundTyVars bad_qtvs
        }
   where
-    rhs_fvs
-      -- Special treatment for data family instances.
-      --
-      -- See Note [Out of scope tvs in data family instances].
-      | Just (tc_rep, _rep_args) <- splitTyConApp_maybe rhs
-      , Just (fam_tc', _fam_args, _) <- tyConFamInstSig_maybe tc_rep
-      , fam_tc' == fam_tc
-      = if isGadtSyntaxTyCon tc_rep
-        then emptyFV
-        else
-          let datacons_fvs =
-                unionsFV
-                  [ delFVs user_tvbs (tyCoFVsOfTypes arg_tys)
-                  | dc <- tyConDataCons tc_rep
-                  , let arg_tys = map scaledThing $ dataConOrigArgTys dc
-                        user_tvbs = mkVarSet $ dataConUserTyVars dc ]
-          in datacons_fvs
-      | otherwise
-      = tyCoFVsOfType rhs
+    rhs_fvs = tyCoFVsOfType rhs
 
     cpt_tvs     = tyCoVarsOfTypes pats
     inj_cpt_tvs = fvVarSet $ injectiveVarsOfTypes False pats
@@ -2363,71 +2364,40 @@ checkFamPatBinders fam_tc qtvs non_user_tvs pats rhs
       -- since the order of `inj_cpt_tvs` is never revealed in an error
       -- message.
 
-    used_tvs    = cpt_tvs `unionVarSet` fvVarSet rhs_fvs
-
     -- Bound but not used at all
-    bad_qtvs    = filterOut ((`elemVarSet` used_tvs) <||> (`elemVarSet` non_user_tvs))
-                  qtvs
-      -- Filter out non-user-tvs in order to only report user-written type variables,
-      -- e.g. type instance forall a. F = ()
-      -- -XPolyKinds introduces the binder 'k' for the kind of 'a', but
-      -- we don't want the error message to complain about 'k' being unused,
-      -- as the user has not written it.
+    bad_qtvs    = mapMaybe bad_qtv_maybe qtvs
+
+    bad_qtv_maybe qtv
+      | not_bound_in_pats
+      = let reason
+              | dodgy
+              = InvalidFamInstQTvDodgy
+              | used_in_rhs
+              = InvalidFamInstQTvNotBoundInPats
+              | otherwise
+              = InvalidFamInstQTvNotUsedInRHS
+        in Just $ InvalidFamInstQTv
+                    { ifiqtv = qtv
+                    , ifiqtv_user_written = not $ qtv `elemVarSet` non_user_tvs
+                    , ifiqtv_reason = reason
+                    }
+      | otherwise
+      = Nothing
+        where
+          not_bound_in_pats = not $ qtv `elemVarSet` inj_cpt_tvs
+          dodgy             = not_bound_in_pats && qtv `elemVarSet` cpt_tvs
+          used_in_rhs       = qtv `elemVarSet` fvVarSet rhs_fvs
 
     -- Used on RHS but not bound on LHS
-    bad_rhs_tvs = filterOut (`elemVarSet` inj_cpt_tvs) (fvVarList rhs_fvs)
+    bad_rhs_tvs = filterOut ((`elemVarSet` inj_cpt_tvs) <||> (`elem` qtvs)) (fvVarList rhs_fvs)
 
     dodgy_tvs   = cpt_tvs `minusVarSet` inj_cpt_tvs
 
     check_tvs mk_err tvs
-      = unless (null tvs) $ addErrAt (getSrcSpan (head tvs)) $
+      = for_ (NE.nonEmpty tvs) $ \ ne_tvs@(tv0 :| _) ->
+        addErrAt (getSrcSpan tv0) $
         TcRnIllegalInstance $ IllegalFamilyInstance $
-        mk_err (map tyVarName tvs)
-
-{- Note [Out of scope tvs in data family instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following data family instance declaration, which we want to reject:
-
-  type D :: Type
-  data family D
-  data instance forall (a :: Type). D = MkD
-
-The problem is that the user quantified the type variable `a` in the instance,
-but didn't use it anywhere.
-
-However, from the perspective of GHC, the RHS of the instance declaration
-is "R:D a", where "R:D" is the representation TyCon that
-GHC.Tc.TyCl.Instance.tcDataFamInstDecl builds; it always includes ALL the
-quantified variables. This means that naively computing the free tyvars of the
-RHS would cause us to report `a` as used on the RHS, which is rather confusing
-for the user (as reported in #23778):
-
-    * Type variable `a' is mentioned in the RHS,
-      but not bound on the LHS of the family instance
-
-To avoid this, we manually compute which type variables are used on the RHS
-of the data family instance in terms of the types of the data family instance
-constructors:
-
-  Vanilla data instance declarations
-
-    For a vanilla data declaration, we collect the free type variables of
-    the data constructors. For example
-
-      data instance D1 x a = K1 a | forall b. K2 a b c
-
-    will give rise to RHS FVs {a,c}.
-
-  GADT data instance declarations
-
-    A GADT data declarations brings its own type variables into scope, e.g.
-
-      data instance D3 y b where
-        C1 :: ...
-        C2 :: ...
-
-    So in this case we use emptyFVs for the RHS tyvars.
--}
+        mk_err ne_tvs
 
 -- | Checks that a list of type patterns is valid in a matching (LHS)
 -- position of a class instances or type/data family instance.
@@ -2533,7 +2503,7 @@ checkConsistentFamInst (InClsInst { ai_class = clas
                    | otherwise                   = BindMe
 
 
-{- Note [Check type-family instance binders]
+{- Note [Check type family instance binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In a type family instance, we require (of course), type variables
 used on the RHS are matched on the LHS. This is checked by
diff --git a/compiler/GHC/Utils/Outputable.hs b/compiler/GHC/Utils/Outputable.hs
index e08b61915c7f..a107d5e1000d 100644
--- a/compiler/GHC/Utils/Outputable.hs
+++ b/compiler/GHC/Utils/Outputable.hs
@@ -52,6 +52,7 @@ module GHC.Utils.Outputable (
         ppWhen, ppUnless, ppWhenOption, ppUnlessOption,
         speakNth, speakN, speakNOf, plural, singular,
         isOrAre, doOrDoes, itsOrTheir, thisOrThese, hasOrHave,
+        itOrThey,
         unicodeSyntax,
 
         coloured, keyword,
@@ -1546,6 +1547,15 @@ itsOrTheir :: [a] -> SDoc
 itsOrTheir [_] = text "its"
 itsOrTheir _   = text "their"
 
+-- | 'it' or 'they', depeneding on the length of the list.
+--
+-- > itOrThey [x]   = text "it"
+-- > itOrThey [x,y] = text "they"
+-- > itOrThey []    = text "they"  -- probably avoid this
+itOrThey :: [a] -> SDoc
+itOrThey [_] = text "it"
+itOrThey _   = text "they"
+
 
 -- | Determines the form of subject appropriate for the length of a list:
 --
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
index 07ed771a220a..8514caa2b2f2 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
@@ -1,12 +1,12 @@
 
 ExplicitForAllFams4a.hs:8:12: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but it isn't used in the family instance.
     • In the equations for closed type family ‘H’
       In the type family declaration for ‘H’
 
-ExplicitForAllFams4a.hs:9:10: error: [GHC-53634]
-    • Out of scope type variable ‘b’ in the RHS of a family instance.
-        All such variables must be bound on the LHS.
+ExplicitForAllFams4a.hs:9:10: error: [GHC-30337]
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the equations for closed type family ‘H’
       In the type family declaration for ‘H’
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
index 80bc9138403a..03c9d499ed78 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
@@ -1,7 +1,7 @@
 
 ExplicitForAllFams4b.hs:8:24: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but it isn't used in the family instance.
     • In the type instance declaration for ‘J’
 
 ExplicitForAllFams4b.hs:8:27: error: [GHC-34447]
@@ -9,14 +9,14 @@ ExplicitForAllFams4b.hs:8:27: error: [GHC-34447]
       J [a] = Float -- Defined at ExplicitForAllFams4b.hs:8:27
       J _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:9:27
 
-ExplicitForAllFams4b.hs:9:22: error: [GHC-53634]
-    • Out of scope type variable ‘b’ in the RHS of a family instance.
-        All such variables must be bound on the LHS.
+ExplicitForAllFams4b.hs:9:22: error: [GHC-30337]
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the type instance declaration for ‘J’
 
 ExplicitForAllFams4b.hs:12:24: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the data instance declaration for ‘K’
 
 ExplicitForAllFams4b.hs:12:27: error: [GHC-34447]
@@ -25,13 +25,13 @@ ExplicitForAllFams4b.hs:12:27: error: [GHC-34447]
       K _ -- Defined at ExplicitForAllFams4b.hs:13:27
 
 ExplicitForAllFams4b.hs:13:22: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the data instance declaration for ‘K’
 
 ExplicitForAllFams4b.hs:16:27: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the newtype instance declaration for ‘L’
 
 ExplicitForAllFams4b.hs:16:30: error: [GHC-34447]
@@ -40,8 +40,8 @@ ExplicitForAllFams4b.hs:16:30: error: [GHC-34447]
       L _ -- Defined at ExplicitForAllFams4b.hs:17:30
 
 ExplicitForAllFams4b.hs:17:25: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the newtype instance declaration for ‘L’
 
 ExplicitForAllFams4b.hs:24:3: error: [GHC-95424]
@@ -52,8 +52,8 @@ ExplicitForAllFams4b.hs:24:3: error: [GHC-95424]
       In the instance declaration for ‘C Int’
 
 ExplicitForAllFams4b.hs:24:17: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but it isn't used in the family instance.
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Int’
 
@@ -65,31 +65,31 @@ ExplicitForAllFams4b.hs:25:3: error: [GHC-95424]
       In the instance declaration for ‘C Int’
 
 ExplicitForAllFams4b.hs:25:17: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Int’
 
-ExplicitForAllFams4b.hs:28:15: error: [GHC-53634]
-    • Out of scope type variable ‘b’ in the RHS of a family instance.
-        All such variables must be bound on the LHS.
+ExplicitForAllFams4b.hs:28:15: error: [GHC-30337]
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Bool’
 
 ExplicitForAllFams4b.hs:29:15: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Bool’
 
 ExplicitForAllFams4b.hs:32:15: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but it isn't used in the family instance.
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Double’
 
 ExplicitForAllFams4b.hs:33:15: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘b’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Double’
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
index f110a9dbe1c5..933fdc41f672 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
@@ -4,7 +4,19 @@ SimpleFail13.hs:9:15: error: [GHC-73138]
         D [C a]
     • In the data instance declaration for ‘D’
 
+SimpleFail13.hs:9:17: error: [GHC-30337]
+    • Dodgy type variable ‘a’ in the LHS of a family instance:
+        the type variable ‘a’ syntactically appears in LHS patterns,
+        but it doesn't appear in an injective position.
+    • In the data instance declaration for ‘D’
+
 SimpleFail13.hs:13:15: error: [GHC-73138]
     • Illegal type synonym family application ‘C a’ in instance:
         E [C a]
     • In the type instance declaration for ‘E’
+
+SimpleFail13.hs:13:17: error: [GHC-30337]
+    • Dodgy type variable ‘a’ in the LHS of a family instance:
+        the type variable ‘a’ syntactically appears in LHS patterns,
+        but it doesn't appear in an injective position.
+    • In the type instance declaration for ‘E’
diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.stderr b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
index 600857e641f2..59b9a6dd8468 100644
--- a/testsuite/tests/indexed-types/should_fail/T17008a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
@@ -1,7 +1,7 @@
 
-T17008a.hs:12:5: error: [GHC-53634]
-    • Out of scope type variable ‘a’ in the RHS of a family instance.
-        All such variables must be bound on the LHS.
-      The real LHS (expanding synonyms) is: F @a x
+T17008a.hs:12:5: error: [GHC-30337]
+    • Dodgy type variable ‘a’ in the LHS of a family instance:
+        the type variable ‘a’ syntactically appears in LHS patterns,
+        but it doesn't appear in an injective position.
     • In the equations for closed type family ‘F’
       In the type family declaration for ‘F’
diff --git a/testsuite/tests/indexed-types/should_fail/T7536.stderr b/testsuite/tests/indexed-types/should_fail/T7536.stderr
index 557160f8a99a..73ebebc93e10 100644
--- a/testsuite/tests/indexed-types/should_fail/T7536.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7536.stderr
@@ -1,6 +1,6 @@
 
-T7536.hs:8:18: error: [GHC-53634]
-    • Out of scope type variable ‘a’ in the RHS of a family instance.
-        All such variables must be bound on the LHS.
-      The real LHS (expanding synonyms) is: TF Int
+T7536.hs:8:18: error: [GHC-30337]
+    • Dodgy type variable ‘a’ in the LHS of a family instance:
+        the type variable ‘a’ syntactically appears in LHS patterns,
+        but it doesn't appear in an injective position.
     • In the type instance declaration for ‘TF’
diff --git a/testsuite/tests/typecheck/should_fail/T23734.stderr b/testsuite/tests/typecheck/should_fail/T23734.stderr
index b5ffbca9fd02..1826957bf2f4 100644
--- a/testsuite/tests/typecheck/should_fail/T23734.stderr
+++ b/testsuite/tests/typecheck/should_fail/T23734.stderr
@@ -1,22 +1,22 @@
 
-T23734.hs:7:22: error: [GHC-30337]
-    • Type variable ‘a’ is bound by a forall,
-        but not used in the family instance.
+T23734.hs:7:25: error: [GHC-30337]
+    • The type variable ‘a’ is bound by a forall,
+      but it isn't used in the family instance.
     • In the type instance declaration for ‘F’
 
-T23734.hs:10:10: error: [GHC-30337]
-    • Type variable ‘b’ is bound by a forall,
-        but not used in the family instance.
+T23734.hs:10:3: error: [GHC-30337]
+    • The type variable ‘b’ is bound by a forall,
+      but it isn't used in the family instance.
     • In the equations for closed type family ‘G’
       In the type family declaration for ‘G’
 
-T23734.hs:14:15: error: [GHC-30337]
-    • Type variable ‘c’ is bound by a forall,
-        but not used in the family instance.
+T23734.hs:14:3: error: [GHC-30337]
+    • The type variable ‘c’ is bound by a forall,
+      but it isn't used in the family instance.
     • In the default type instance declaration for ‘H’
       In the class declaration for ‘C’
 
 T23734.hs:17:23: error: [GHC-30337]
-    • Type variable ‘d’ is bound by a forall,
-        but not used in the family instance.
+    • The type variable ‘d’ is bound by a forall,
+      but does not appear in any of the LHS patterns of the family instance.
     • In the data instance declaration for ‘D’
diff --git a/testsuite/tests/typecheck/should_fail/T23778.stderr b/testsuite/tests/typecheck/should_fail/T23778.stderr
index 1faf580c1896..429f6c299f48 100644
--- a/testsuite/tests/typecheck/should_fail/T23778.stderr
+++ b/testsuite/tests/typecheck/should_fail/T23778.stderr
@@ -1,5 +1,5 @@
 
 T23778.hs:7:22: error: [GHC-30337]
-    • Type variables ‘d’, ‘v’ are bound by a forall,
-        but not used in the family instance.
+    • The type variables ‘d’, ‘v’ are bound by a forall,
+      but do not appear in any of the LHS patterns of the family instance.
     • In the data instance declaration for ‘D’
-- 
GitLab