Fix #17405 by not checking imported equationswip/rae/t17405

Previously, we checked all imported type family equations
for injectivity. This is very silly. Now, we check only
for conflicts.

Before I could even imagine doing the fix, I needed to untangle
several functions that were (in my opinion) overly complicated.
It's still not quite as perfect as I'd like, but it's good enough
for now.

Test case: typecheck/should_compile/T17405

17 files changed, 241 insertions, 177 deletions

diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 5ec8681623..c91b991ea8 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -10,7 +10,7 @@ module FamInst (
         newFamInst,
 
         -- * Injectivity
-        makeInjectivityErrors
+        reportInjectivityErrors, reportConflictingInjectivityErrs
     ) where
 
 import GhcPrelude
@@ -44,6 +44,7 @@ import VarSet
 import FV
 import Bag( Bag, unionBags, unitBag )
 import Control.Monad
+import Data.List.NonEmpty ( NonEmpty(..) )
 
 import qualified GHC.LanguageExtensions  as LangExt
 
@@ -682,10 +683,13 @@ addLocalFamInst (home_fie, my_fis) fam_inst
              home_fie' = extendFamInstEnv home_fie fam_inst
 
            -- Check for conflicting instance decls and injectivity violations
-       ; no_conflict    <- checkForConflicts            inst_envs fam_inst
-       ; injectivity_ok <- checkForInjectivityConflicts inst_envs fam_inst
+       ; ((), no_errs) <- askNoErrs $
+         do { checkForConflicts            inst_envs fam_inst
+            ; checkForInjectivityConflicts inst_envs fam_inst
+            ; checkInjectiveEquation       fam_inst
+            }
 
-       ; if no_conflict && injectivity_ok then
+       ; if no_errs then
             return (home_fie', fam_inst : my_fis)
          else
             return (home_fie,  my_fis) }
@@ -701,7 +705,8 @@ Check whether a single family instance conflicts with those in two instance
 environments (one for the EPS and one for the HPT).
 -}
 
-checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
+-- | Checks to make sure no two family instances overlap.
+checkForConflicts :: FamInstEnvs -> FamInst -> TcM ()
 checkForConflicts inst_envs fam_inst
   = do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
        ; traceTc "checkForConflicts" $
@@ -709,64 +714,70 @@ checkForConflicts inst_envs fam_inst
               , ppr fam_inst
               -- , ppr inst_envs
          ]
-       ; reportConflictInstErr fam_inst conflicts
-       ; return (null conflicts) }
+       ; reportConflictInstErr fam_inst conflicts }
+
+checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM ()
+  -- see Note [Verifying injectivity annotation] in FamInstEnv, check 1B1.
+checkForInjectivityConflicts instEnvs famInst
+    | isTypeFamilyTyCon tycon   -- as opposed to data family tycon
+    , Injective inj <- tyConInjectivityInfo tycon
+    = let conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst in
+      reportConflictingInjectivityErrs tycon conflicts (coAxiomSingleBranch (fi_axiom famInst))
+
+    | otherwise
+    = return ()
+
+    where tycon = famInstTyCon famInst
 
 -- | Check whether a new open type family equation can be added without
 -- violating injectivity annotation supplied by the user. Returns True when
 -- this is possible and False if adding this equation would violate injectivity
--- annotation.
-checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
-checkForInjectivityConflicts instEnvs famInst
+-- annotation. This looks only at the one equation; it does not look for
+-- interaction between equations. Use checkForInjectivityConflicts for that.
+-- Does checks (2)-(4) of Note [Verifying injectivity annotation] in FamInstEnv.
+checkInjectiveEquation :: FamInst -> TcM ()
+checkInjectiveEquation famInst
     | isTypeFamilyTyCon tycon
     -- type family is injective in at least one argument
     , Injective inj <- tyConInjectivityInfo tycon = do
     { dflags <- getDynFlags
     ; let axiom = coAxiomSingleBranch fi_ax
-          conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst
           -- see Note [Verifying injectivity annotation] in FamInstEnv
-          errs = makeInjectivityErrors dflags fi_ax axiom inj conflicts
-    ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err) errs
-    ; return (null errs)
+    ; reportInjectivityErrors dflags fi_ax axiom inj
     }
 
     -- if there was no injectivity annotation or tycon does not represent a
     -- type family we report no conflicts
-    | otherwise = return True
+    | otherwise
+    = return ()
+
     where tycon = famInstTyCon famInst
           fi_ax = fi_axiom famInst
 
--- | Build a list of injectivity errors together with their source locations.
-makeInjectivityErrors
+-- | Report a list of injectivity errors together with their source locations.
+-- Looks only at one equation; does not look for conflicts *among* equations.
+reportInjectivityErrors
    :: DynFlags
    -> CoAxiom br   -- ^ Type family for which we generate errors
    -> CoAxBranch   -- ^ Currently checked equation (represented by axiom)
    -> [Bool]       -- ^ Injectivity annotation
-   -> [CoAxBranch] -- ^ List of injectivity conflicts
-   -> [(SDoc, SrcSpan)]
-makeInjectivityErrors dflags fi_ax axiom inj conflicts
+   -> TcM ()
+reportInjectivityErrors dflags fi_ax axiom inj
   = ASSERT2( any id inj, text "No injective type variables" )
-    let lhs             = coAxBranchLHS axiom
-        rhs             = coAxBranchRHS axiom
-        fam_tc          = coAxiomTyCon fi_ax
-        are_conflicts   = not $ null conflicts
-        (unused_inj_tvs, unused_vis, undec_inst_flag)
-                        = unusedInjTvsInRHS dflags fam_tc lhs rhs
-        inj_tvs_unused  = not $ isEmptyVarSet unused_inj_tvs
-        tf_headed       = isTFHeaded rhs
-        bare_variables  = bareTvInRHSViolated lhs rhs
-        wrong_bare_rhs  = not $ null bare_variables
-
-        err_builder herald eqns
-                        = ( hang herald
-                               2 (vcat (map (pprCoAxBranchUser fam_tc) eqns))
-                          , coAxBranchSpan (head eqns) )
-        errorIf p f     = if p then [f err_builder axiom] else []
-     in    errorIf are_conflicts  (conflictInjInstErr     conflicts     )
-        ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs
-                                     unused_vis undec_inst_flag)
-        ++ errorIf tf_headed       tfHeadedErr
-        ++ errorIf wrong_bare_rhs (bareVariableInRHSErr   bare_variables)
+    do let lhs             = coAxBranchLHS axiom
+           rhs             = coAxBranchRHS axiom
+           fam_tc          = coAxiomTyCon fi_ax
+           (unused_inj_tvs, unused_vis, undec_inst_flag)
+                           = unusedInjTvsInRHS dflags fam_tc lhs rhs
+           inj_tvs_unused  = not $ isEmptyVarSet unused_inj_tvs
+           tf_headed       = isTFHeaded rhs
+           bare_variables  = bareTvInRHSViolated lhs rhs
+           wrong_bare_rhs  = not $ null bare_variables
+
+       when inj_tvs_unused $ reportUnusedInjectiveVarsErr fam_tc unused_inj_tvs
+                                                          unused_vis undec_inst_flag axiom
+       when tf_headed      $ reportTfHeadedErr            fam_tc axiom
+       when wrong_bare_rhs $ reportBareVariableInRHSErr   fam_tc bare_variables axiom
 
 -- | Is type headed by a type family application?
 isTFHeaded :: Type -> Bool
@@ -906,8 +917,8 @@ unusedInjTvsInRHS :: DynFlags
                   -> [Type] -- LHS arguments
                   -> Type   -- the RHS
                   -> ( TyVarSet
-                     , Bool  -- True <=> one or more variable is used invisibly
-                     , Bool) -- True <=> suggest -XUndecidableInstances
+                     , Bool   -- True <=> one or more variable is used invisibly
+                     , Bool ) -- True <=> suggest -XUndecidableInstances
 -- See Note [Verifying injectivity annotation] in FamInstEnv.
 -- This function implements check (4) described there, further
 -- described in Note [Coverage condition for injective type families].
@@ -945,51 +956,42 @@ unusedInjTvsInRHS _ _ _ _ = (emptyVarSet, False, False)
 -- Producing injectivity error messages
 ---------------------------------------
 
--- | Type of functions that use error message and a list of axioms to build full
--- error message (with a source location) for injective type families.
-type InjErrorBuilder = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
-
--- | Build injecivity error herald common to all injectivity errors.
-injectivityErrorHerald :: Bool -> SDoc
-injectivityErrorHerald isSingular =
-  text "Type family equation" <> s isSingular <+> text "violate" <>
-  s (not isSingular) <+> text "injectivity annotation" <>
-  if isSingular then dot else colon
-  -- Above is an ugly hack.  We want this: "sentence. herald:" (note the dot and
-  -- colon).  But if herald is empty we want "sentence:" (note the colon).  We
-  -- can't test herald for emptiness so we rely on the fact that herald is empty
-  -- only when isSingular is False.  If herald is non empty it must end with a
-  -- colon.
-    where
-      s False = text "s"
-      s True  = empty
-
--- | Build error message for a pair of equations violating an injectivity
--- annotation.
-conflictInjInstErr :: [CoAxBranch] -> InjErrorBuilder -> CoAxBranch
-                   -> (SDoc, SrcSpan)
-conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
-  | confEqn : _ <- conflictingEqns
-  = errorBuilder (injectivityErrorHerald False) [confEqn, tyfamEqn]
-  | otherwise
-  = panic "conflictInjInstErr"
+-- | Report error message for a pair of equations violating an injectivity
+-- annotation. No error message if there are no branches.
+reportConflictingInjectivityErrs :: TyCon -> [CoAxBranch] -> CoAxBranch -> TcM ()
+reportConflictingInjectivityErrs _ [] _ = return ()
+reportConflictingInjectivityErrs fam_tc (confEqn1:_) tyfamEqn
+  = addErrs [buildInjectivityError fam_tc herald (confEqn1 :| [tyfamEqn])]
+  where
+    herald = text "Type family equation right-hand sides overlap; this violates" $$
+             text "the family's injectivity annotation:"
+
+-- | Injectivity error herald common to all injectivity errors.
+injectivityErrorHerald :: SDoc
+injectivityErrorHerald =
+  text "Type family equation violates the family's injectivity annotation."
 
--- | Build error message for equation with injective type variables unused in
+
+-- | Report error message for equation with injective type variables unused in
 -- the RHS. Note [Coverage condition for injective type families], step 6
-unusedInjectiveVarsErr :: TyVarSet
-                       -> Bool   -- True <=> print invisible arguments
-                       -> Bool   -- True <=> suggest -XUndecidableInstances
-                       -> InjErrorBuilder -> CoAxBranch
-                       -> (SDoc, SrcSpan)
-unusedInjectiveVarsErr tvs has_kinds undec_inst errorBuilder tyfamEqn
-  = let (doc, loc) = errorBuilder (injectivityErrorHerald True $$ msg)
-                                  [tyfamEqn]
-    in (pprWithExplicitKindsWhen has_kinds doc, loc)
+reportUnusedInjectiveVarsErr :: TyCon
+                             -> TyVarSet
+                             -> Bool   -- True <=> print invisible arguments
+                             -> Bool   -- True <=> suggest -XUndecidableInstances
+                             -> CoAxBranch
+                             -> TcM ()
+reportUnusedInjectiveVarsErr fam_tc tvs has_kinds undec_inst tyfamEqn
+  = let (loc, doc) = buildInjectivityError fam_tc
+                                  (injectivityErrorHerald $$
+                                   herald $$
+                                   text "In the type family equation:")
+                                  (tyfamEqn :| [])
+    in addErrAt loc (pprWithExplicitKindsWhen has_kinds doc)
     where
-      doc = sep [ what <+> text "variable" <>
+      herald = sep [ what <+> text "variable" <>
                   pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . scopedSort)
                 , text "cannot be inferred from the right-hand side." ]
-            $$ extra
+               $$ extra
 
       what | has_kinds = text "Type/kind"
            | otherwise = text "Type"
@@ -997,28 +999,33 @@ unusedInjectiveVarsErr tvs has_kinds undec_inst errorBuilder tyfamEqn
       extra | undec_inst = text "Using UndecidableInstances might help"
             | otherwise  = empty
 
-      msg = doc $$ text "In the type family equation:"
-
--- | Build error message for equation that has a type family call at the top
+-- | Report error message for equation that has a type family call at the top
 -- level of RHS
-tfHeadedErr :: InjErrorBuilder -> CoAxBranch
-            -> (SDoc, SrcSpan)
-tfHeadedErr errorBuilder famInst
-  = errorBuilder (injectivityErrorHerald True $$
-                  text "RHS of injective type family equation cannot" <+>
-                  text "be a type family:") [famInst]
-
--- | Build error message for equation that has a bare type variable in the RHS
+reportTfHeadedErr :: TyCon -> CoAxBranch -> TcM ()
+reportTfHeadedErr fam_tc branch
+  = addErrs [buildInjectivityError fam_tc
+               (injectivityErrorHerald $$
+                 text "RHS of injective type family equation cannot" <+>
+                 text "be a type family:")
+               (branch :| [])]
+
+-- | Report error message for equation that has a bare type variable in the RHS
 -- but LHS pattern is not a bare type variable.
-bareVariableInRHSErr :: [Type] -> InjErrorBuilder -> CoAxBranch
-                     -> (SDoc, SrcSpan)
-bareVariableInRHSErr tys errorBuilder famInst
-  = errorBuilder (injectivityErrorHerald True $$
+reportBareVariableInRHSErr :: TyCon -> [Type] -> CoAxBranch -> TcM ()
+reportBareVariableInRHSErr fam_tc tys branch
+  = addErrs [buildInjectivityError fam_tc
+                 (injectivityErrorHerald $$
                   text "RHS of injective type family equation is a bare" <+>
                   text "type variable" $$
                   text "but these LHS type and kind patterns are not bare" <+>
-                  text "variables:" <+> pprQuotedList tys) [famInst]
-
+                  text "variables:" <+> pprQuotedList tys)
+                 (branch :| [])]
+
+buildInjectivityError :: TyCon -> SDoc -> NonEmpty CoAxBranch -> (SrcSpan, SDoc)
+buildInjectivityError fam_tc herald (eqn1 :| rest_eqns)
+  = ( coAxBranchSpan eqn1
+    , hang herald
+         2 (vcat (map (pprCoAxBranchUser fam_tc) (eqn1 : rest_eqns))) )
 
 reportConflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
 reportConflictInstErr _ []
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index ce9270c1f3..b882f88828 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -50,7 +50,7 @@ import TcEnv       ( tcInitTidyEnv, tcInitOpenTidyEnv )
 import FunDeps
 import FamInstEnv  ( isDominatedBy, injectiveBranches,
                      InjectivityCheckResult(..) )
-import FamInst     ( makeInjectivityErrors )
+import FamInst
 import Name
 import VarEnv
 import VarSet
@@ -2031,8 +2031,8 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
            ; let conflicts =
                      fst $ foldl' (gather_conflicts inj prev_branches cur_branch)
                                  ([], 0) prev_branches
-           ; mapM_ (\(err, span) -> setSrcSpan span $ addErr err)
-                   (makeInjectivityErrors dflags ax cur_branch inj conflicts) }
+           ; reportConflictingInjectivityErrs fam_tc conflicts cur_branch
+           ; reportInjectivityErrors dflags ax cur_branch inj }
       | otherwise
       = return ()
 
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 7695e31643..b99983f779 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -202,7 +202,7 @@ pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
        2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
 
 pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
--- Used when printing injectivity errors (FamInst.makeInjectivityErrors)
+-- Used when printing injectivity errors (FamInst.reportInjectivityErrors)
 -- and inaccessible branches (TcValidity.inaccessibleCoAxBranch)
 -- This happens in error messages: don't print the RHS of a data
 --   family axiom, which is meaningless to a user
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 7805bc8ca6..c0b6414f8c 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -895,6 +895,13 @@ conditions hold:
    There are subtleties here. See Note [Coverage condition for injective type families]
    in FamInst.
 
+Check (1) must be done for all family instances (transitively) imported. Other
+checks (2-4) should be done just for locally written equations, as they are checks
+involving just a single equation, not about interactions. Doing the other checks for
+imported equations led to #17405, as the behavior of check (4) depends on
+-XUndecidableInstances (see Note [Coverage condition for injective type families] in
+FamInst), which may vary between modules.
+
 See also Note [Injective type families] in TyCon
 -}
 
diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs
index c484ba90ea..e8d20e3208 100644
--- a/compiler/utils/Util.hs
+++ b/compiler/utils/Util.hs
@@ -49,6 +49,8 @@ module Util (
 
         changeLast,
 
+        whenNonEmpty,
+
         -- * Tuples
         fstOf3, sndOf3, thdOf3,
         firstM, first3M, secondM,
@@ -137,6 +139,7 @@ import Data.Data
 import Data.IORef       ( IORef, newIORef, atomicModifyIORef' )
 import System.IO.Unsafe ( unsafePerformIO )
 import Data.List        hiding (group)
+import Data.List.NonEmpty  ( NonEmpty(..) )
 
 import GHC.Exts
 import GHC.Stack (HasCallStack)
@@ -610,6 +613,10 @@ changeLast []     _  = panic "changeLast"
 changeLast [_]    x  = [x]
 changeLast (x:xs) x' = x : changeLast xs x'
 
+whenNonEmpty :: Applicative m => [a] -> (NonEmpty a -> m ()) -> m ()
+whenNonEmpty []     _ = pure ()
+whenNonEmpty (x:xs) f = f (x :| xs)
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/testsuite/tests/deriving/should_fail/T8165_fail1.stderr b/testsuite/tests/deriving/should_fail/T8165_fail1.stderr
index 43bca52aa5..c47ed702f4 100644
--- a/testsuite/tests/deriving/should_fail/T8165_fail1.stderr
+++ b/testsuite/tests/deriving/should_fail/T8165_fail1.stderr
@@ -7,11 +7,12 @@ T8165_fail1.hs:17:12: error:
     • In the newtype declaration for ‘MyInt’
 
 T8165_fail1.hs:25:8: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       S Int = Char -- Defined at T8165_fail1.hs:25:8
       S WrappedInt = S Int -- Defined at T8165_fail1.hs:28:12
 
 T8165_fail1.hs:28:12: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       S WrappedInt = S Int -- Defined at T8165_fail1.hs:28:12
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index b171221e17..bbea2d4398 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -1,44 +1,46 @@
 
 <interactive>:10:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       F Char Bool Int = Int -- Defined at <interactive>:10:15
       F Bool Int Char = Int -- Defined at <interactive>:11:15
 
 <interactive>:16:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       I Int Char Bool = Bool -- Defined at <interactive>:16:15
       I Int Int Int = Bool -- Defined at <interactive>:17:15
 
 <interactive>:26:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       IdProxy a = Id a -- Defined at <interactive>:26:15
 
 <interactive>:34:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘'Z’
       P 'Z m = m -- Defined at <interactive>:34:15
 
 <interactive>:40:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       J Int b c = Char -- Defined at <interactive>:40:15
 
 <interactive>:44:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘n’ cannot be inferred from the right-hand side.
     In the type family equation:
       K ('S n) m = 'S m -- Defined at <interactive>:44:15
 
 <interactive>:49:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       L a = MaybeSyn a -- Defined at <interactive>:49:15
 
 <interactive>:55:41: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variable ‘k1’
     cannot be inferred from the right-hand side.
     In the type family equation:
@@ -46,7 +48,7 @@
         -- Defined at <interactive>:55:41
 
 <interactive>:60:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variable ‘k1’
     cannot be inferred from the right-hand side.
     In the type family equation:
@@ -54,14 +56,14 @@
         -- Defined at <interactive>:60:15
 
 <interactive>:64:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variable ‘k’ cannot be inferred from the right-hand side.
     In the type family equation:
       forall k (a :: k) (b :: k).
         Fc @k a b = Int -- Defined at <interactive>:64:15
 
 <interactive>:68:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variables ‘k’, ‘a’, ‘b’
     cannot be inferred from the right-hand side.
     In the type family equation:
@@ -69,49 +71,54 @@
         Gc @k a b = Int -- Defined at <interactive>:68:15
 
 <interactive>:81:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       F1 [a] = Maybe (GF1 a) -- Defined at <interactive>:81:15
       F1 (Maybe a) = Maybe (GF2 a) -- Defined at <interactive>:82:15
 
 <interactive>:85:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘[a]’
       W1 [a] = a -- Defined at <interactive>:85:15
 
 <interactive>:88:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       W2 [a] = W2 a -- Defined at <interactive>:88:15
 
 <interactive>:92:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       Z1 [a] = (a, a) -- Defined at <interactive>:92:15
       Z1 (Maybe b) = (b, [b]) -- Defined at <interactive>:93:15
 
 <interactive>:96:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       G1 [a] = [a] -- Defined at <interactive>:96:15
       G1 (Maybe b) = [(b, b)] -- Defined at <interactive>:97:15
 
 <interactive>:100:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       G3 a Int = (a, Int) -- Defined at <interactive>:100:15
       G3 a Bool = (Bool, a) -- Defined at <interactive>:101:15
 
 <interactive>:104:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       G4 a b = [a] -- Defined at <interactive>:104:15
 
 <interactive>:107:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       G5 [a] = [GF1 a] -- Defined at <interactive>:107:15
       G5 Int = [Bool] -- Defined at <interactive>:108:15
 
 <interactive>:111:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘a’ cannot be inferred from the right-hand side.
     In the type family equation:
       G6 [a] = [HF1 a] -- Defined at <interactive>:111:15
diff --git a/testsuite/tests/indexed-types/should_compile/T17405a.hs b/testsuite/tests/indexed-types/should_compile/T17405a.hs
new file mode 100644
index 0000000000..9fb16aa825
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17405a.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilyDependencies, UndecidableInstances #-}
+module T17405a where
+
+data D a
+type family F a = r | r -> a
+type instance F (D a) = D (F a)
diff --git a/testsuite/tests/indexed-types/should_compile/T17405b.hs b/testsuite/tests/indexed-types/should_compile/T17405b.hs
new file mode 100644
index 0000000000..d21b3a588f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17405b.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
+module T17405b where
+
+type family F2 a
+type instance F2 Int = Bool
diff --git a/testsuite/tests/indexed-types/should_compile/T17405c.hs b/testsuite/tests/indexed-types/should_compile/T17405c.hs
new file mode 100644
index 0000000000..ec7c46a6a4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17405c.hs
@@ -0,0 +1,4 @@
+module T17405c where
+
+import T17405a
+import T17405b
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 1ee797ca41..8bda294207 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -293,3 +293,4 @@ test('T16632', normal, compile, ['-Wunused-type-patterns -fdiagnostics-show-care
 test('T16828', normal, compile, [''])
 test('T17008b', normal, compile, [''])
 test('T17056', normal, compile, [''])
+test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
diff --git a/testsuite/tests/th/T6018th.stderr b/testsuite/tests/th/T6018th.stderr
index 56e3f471f7..b905fe8bf1 100644
--- a/testsuite/tests/th/T6018th.stderr
+++ b/testsuite/tests/th/T6018th.stderr
@@ -1,5 +1,6 @@
 
 T6018th.hs:98:4: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       H Int Int Int = Bool -- Defined at T6018th.hs:98:4
       H Int Char Bool = Bool -- Defined at T6018th.hs:98:4
diff --git a/testsuite/tests/typecheck/should_fail/T10836.stderr b/testsuite/tests/typecheck/should_fail/T10836.stderr
index 2e92e6135a..bcbfde7694 100644
--- a/testsuite/tests/typecheck/should_fail/T10836.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10836.stderr
@@ -1,14 +1,16 @@
 
 T10836.hs:5:5: error:
-    Type family equations violate injectivity annotation:
-      Foo Int = Int -- Defined at T10836.hs:5:5
-      Foo Bool = Int -- Defined at T10836.hs:6:5
-    In the equations for closed type family ‘Foo’
-    In the type family declaration for ‘Foo’
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
+        Foo Int = Int -- Defined at T10836.hs:5:5
+        Foo Bool = Int -- Defined at T10836.hs:6:5
+    • In the equations for closed type family ‘Foo’
+      In the type family declaration for ‘Foo’
 
 T10836.hs:9:5: error:
-    Type family equations violate injectivity annotation:
-      Bar Int = Int -- Defined at T10836.hs:9:5
-      Bar Bool = Int -- Defined at T10836.hs:10:5
-    In the equations for closed type family ‘Bar’
-    In the type family declaration for ‘Bar’
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
+        Bar Int = Int -- Defined at T10836.hs:9:5
+        Bar Bool = Int -- Defined at T10836.hs:10:5
+    • In the equations for closed type family ‘Bar’
+      In the type family declaration for ‘Bar’
diff --git a/testsuite/tests/typecheck/should_fail/T12430.stderr b/testsuite/tests/typecheck/should_fail/T12430.stderr
index c3d9446197..fd73b40fc4 100644
--- a/testsuite/tests/typecheck/should_fail/T12430.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12430.stderr
@@ -1,6 +1,6 @@
 
 T12430.hs:6:3: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       Type variable ‘x’ cannot be inferred from the right-hand side.
       In the type family equation:
         F x = C x -- Defined at T12430.hs:6:3
diff --git a/testsuite/tests/typecheck/should_fail/T16512b.stderr b/testsuite/tests/typecheck/should_fail/T16512b.stderr
index 82a33117e4..649957c43d 100644
--- a/testsuite/tests/typecheck/should_fail/T16512b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16512b.stderr
@@ -1,6 +1,6 @@
 
 T16512b.hs:6:3: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       Type variable ‘a’ cannot be inferred from the right-hand side.
       Using UndecidableInstances might help
       In the type family equation:
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 8fb124adb9..64eba564f4 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -5,60 +5,65 @@
 [5 of 5] Compiling T6018fail        ( T6018fail.hs, T6018fail.o )
 
 T6018Afail.hs:9:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       G Char Bool Int = Int -- Defined at T6018Afail.hs:9:15
       G Bool Int Char = Int -- Defined at T6018fail.hs:17:15
 
 T6018Cfail.hs:8:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       T6018Bfail.H Char Bool Int = Int -- Defined at T6018Cfail.hs:8:15
       T6018Bfail.H Bool Int Char = Int -- Defined at T6018Dfail.hs:7:15
 
 T6018fail.hs:15:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       F Bool Int Char = Int -- Defined at T6018fail.hs:15:15
       F Char Bool Int = Int -- Defined at T6018fail.hs:14:15
 
 T6018fail.hs:21:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       I Int Int Int = Bool -- Defined at T6018fail.hs:21:15
       I Int Char Bool = Bool -- Defined at T6018fail.hs:20:15
 
 T6018fail.hs:30:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       IdProxy a = Id a -- Defined at T6018fail.hs:30:15
 
 T6018fail.hs:38:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘'Z’
       P 'Z m = m -- Defined at T6018fail.hs:38:15
 
 T6018fail.hs:39:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       P ('S n) m = 'S (P n m) -- Defined at T6018fail.hs:39:15
       P 'Z m = m -- Defined at T6018fail.hs:38:15
 
 T6018fail.hs:44:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       J Int b c = Char -- Defined at T6018fail.hs:44:15
 
 T6018fail.hs:48:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘n’ cannot be inferred from the right-hand side.
     In the type family equation:
       K ('S n) m = 'S m -- Defined at T6018fail.hs:48:15
 
 T6018fail.hs:53:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       L a = MaybeSyn a -- Defined at T6018fail.hs:53:15
 
 T6018fail.hs:61:10: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variable ‘k1’
     cannot be inferred from the right-hand side.
     In the type family equation:
@@ -66,7 +71,7 @@ T6018fail.hs:61:10: error:
         -- Defined at T6018fail.hs:61:10
 
 T6018fail.hs:64:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variable ‘k1’
     cannot be inferred from the right-hand side.
     In the type family equation:
@@ -74,14 +79,14 @@ T6018fail.hs:64:15: error:
         -- Defined at T6018fail.hs:64:15
 
 T6018fail.hs:68:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variable ‘k’ cannot be inferred from the right-hand side.
     In the type family equation:
       forall k (a :: k) (b :: k).
         Fc @k a b = Int -- Defined at T6018fail.hs:68:15
 
 T6018fail.hs:72:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variables ‘k’, ‘a’, ‘b’
     cannot be inferred from the right-hand side.
     In the type family equation:
@@ -89,55 +94,60 @@ T6018fail.hs:72:15: error:
         Gc @k a b = Int -- Defined at T6018fail.hs:72:15
 
 T6018fail.hs:76:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       F1 [a] = Maybe (GF1 a) -- Defined at T6018fail.hs:76:15
       F1 (Maybe a) = Maybe (GF2 a) -- Defined at T6018fail.hs:77:15
 
 T6018fail.hs:89:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘[a]’
       W1 [a] = a -- Defined at T6018fail.hs:89:15
 
 T6018fail.hs:92:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       W2 [a] = W2 a -- Defined at T6018fail.hs:92:15
 
 T6018fail.hs:97:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       Z1 (Maybe b) = (b, [b]) -- Defined at T6018fail.hs:97:15
       Z1 [a] = (a, a) -- Defined at T6018fail.hs:96:15
 
 T6018fail.hs:101:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       G1 (Maybe b) = [(b, b)] -- Defined at T6018fail.hs:101:15
       G1 [a] = [a] -- Defined at T6018fail.hs:100:15
 
 T6018fail.hs:105:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       G3 a Bool = (Bool, a) -- Defined at T6018fail.hs:105:15
       G3 a Int = (a, Int) -- Defined at T6018fail.hs:104:15
 
 T6018fail.hs:108:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘b’ cannot be inferred from the right-hand side.
     In the type family equation:
       G4 a b = [a] -- Defined at T6018fail.hs:108:15
 
 T6018fail.hs:112:15: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       G5 Int = [Bool] -- Defined at T6018fail.hs:112:15
       G5 [a] = [GF1 a] -- Defined at T6018fail.hs:111:15
 
 T6018fail.hs:115:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type variable ‘a’ cannot be inferred from the right-hand side.
     In the type family equation:
       G6 [a] = [HF1 a] -- Defined at T6018fail.hs:115:15
 
 T6018fail.hs:120:15: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     Type/kind variables ‘k’, ‘c’
     cannot be inferred from the right-hand side.
     In the type family equation:
@@ -145,12 +155,13 @@ T6018fail.hs:120:15: error:
         G7 @k a b c = [G7a @k a b c] -- Defined at T6018fail.hs:120:15
 
 T6018fail.hs:131:1: error:
-    Type family equations violate injectivity annotation:
+    Type family equation right-hand sides overlap; this violates
+    the family's injectivity annotation:
       FC Int Bool = Bool -- Defined at T6018fail.hs:131:1
       FC Int Char = Bool -- Defined at T6018fail.hs:127:10
 
 T6018fail.hs:136:1: error:
-    Type family equation violates injectivity annotation.
+    Type family equation violates the family's injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘*’,
                                                                  ‘Char’
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index adb2c9ccb0..32bcf83ba5 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -1,13 +1,13 @@
 
 T6018failclosed.hs:11:5: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       RHS of injective type family equation cannot be a type family:
         IdProxyClosed a = IdClosed a -- Defined at T6018failclosed.hs:11:5
     • In the equations for closed type family ‘IdProxyClosed’
       In the type family declaration for ‘IdProxyClosed’
 
 T6018failclosed.hs:19:5: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       RHS of injective type family equation is a bare type variable
       but these LHS type and kind patterns are not bare variables: ‘'Z’
         PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5
@@ -15,7 +15,8 @@ T6018failclosed.hs:19:5: error:
       In the type family declaration for ‘PClosed’
 
 T6018failclosed.hs:19:5: error:
-    • Type family equations violate injectivity annotation:
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
         PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5
         PClosed ('S n) m = 'S (PClosed n m)
           -- Defined at T6018failclosed.hs:20:5
@@ -23,7 +24,7 @@ T6018failclosed.hs:19:5: error:
       In the type family declaration for ‘PClosed’
 
 T6018failclosed.hs:25:5: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       Type/kind variables ‘k1’, ‘b’
       cannot be inferred from the right-hand side.
       In the type family equation:
@@ -34,7 +35,7 @@ T6018failclosed.hs:25:5: error:
       In the type family declaration for ‘JClosed’
 
 T6018failclosed.hs:30:5: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       Type variable ‘n’ cannot be inferred from the right-hand side.
       In the type family equation:
         KClosed ('S n) m = 'S m -- Defined at T6018failclosed.hs:30:5
@@ -42,7 +43,7 @@ T6018failclosed.hs:30:5: error:
       In the type family declaration for ‘KClosed’
 
 T6018failclosed.hs:35:5: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       RHS of injective type family equation cannot be a type family:
         forall k (a :: k).
           LClosed a = MaybeSynClosed a -- Defined at T6018failclosed.hs:35:5
@@ -50,28 +51,31 @@ T6018failclosed.hs:35:5: error:
       In the type family declaration for ‘LClosed’
 
 T6018failclosed.hs:39:5: error:
-    • Type family equations violate injectivity annotation:
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
         FClosed Char Bool Int = Int -- Defined at T6018failclosed.hs:39:5
         FClosed Bool Int Char = Int -- Defined at T6018failclosed.hs:40:5
     • In the equations for closed type family ‘FClosed’
       In the type family declaration for ‘FClosed’
 
 T6018failclosed.hs:43:5: error:
-    • Type family equations violate injectivity annotation:
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
         IClosed Int Char Bool = Bool -- Defined at T6018failclosed.hs:43:5
         IClosed Int Int Int = Bool -- Defined at T6018failclosed.hs:44:5
     • In the equations for closed type family ‘IClosed’
       In the type family declaration for ‘IClosed’
 
 T6018failclosed.hs:49:3: error:
-    • Type family equations violate injectivity annotation:
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
         E2 'True = 'False -- Defined at T6018failclosed.hs:49:3
         E2 a = 'False -- Defined at T6018failclosed.hs:50:3
     • In the equations for closed type family ‘E2’
       In the type family declaration for ‘E2’
 
 T6018failclosed.hs:50:3: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       Type variable ‘a’ cannot be inferred from the right-hand side.
       In the type family equation:
         E2 a = 'False -- Defined at T6018failclosed.hs:50:3
@@ -79,14 +83,15 @@ T6018failclosed.hs:50:3: error:
       In the type family declaration for ‘E2’
 
 T6018failclosed.hs:61:3: error:
-    • Type family equations violate injectivity annotation:
+    • Type family equation right-hand sides overlap; this violates
+      the family's injectivity annotation:
         F a IO = IO a -- Defined at T6018failclosed.hs:61:3
         F Char b = b Int -- Defined at T6018failclosed.hs:62:3
     • In the equations for closed type family ‘F’
       In the type family declaration for ‘F’
 
 T6018failclosed.hs:66:5: error:
-    • Type family equation violates injectivity annotation.
+    • Type family equation violates the family's injectivity annotation.
       Type/kind variable ‘k’ cannot be inferred from the right-hand side.
       In the type family equation:
         forall k (a :: k) (b :: k).