unusedInjTvsInRHS :: DynFlags
                  -> TyCon  -- type family
                  -> [Type] -- LHS arguments
                  -> Type   -- the RHS
                  -> ( TyVarSet
                     , 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].
-- In theory (and modulo the -XUndecidableInstances wrinkle),
-- instead of implementing this whole check in this way, we could
-- attempt to unify equation with itself.  We would reject exactly the same
-- equations but this method gives us more precise error messages by returning
-- precise names of variables that are not mentioned in the RHS.
unusedInjTvsInRHS dflags tycon@(tyConInjectivityInfo -> Injective inj_list) lhs rhs =
  -- Note [Coverage condition for injective type families], step 5
  (bad_vars, any_invisible, suggest_undec)
    where
      undec_inst = xopt LangExt.UndecidableInstances dflags

      inj_lhs = filterByList inj_list lhs
      lhs_vars = tyCoVarsOfTypes inj_lhs

      rhs_inj_vars = fvVarSet $ injectiveVarsOfType undec_inst rhs

      bad_vars = lhs_vars `minusVarSet` rhs_inj_vars

      any_bad = not $ isEmptyVarSet bad_vars

      invis_vars = fvVarSet $ invisibleVarsOfTypes [mkTyConApp tycon lhs, rhs]

      any_invisible = any_bad && (bad_vars `intersectsVarSet` invis_vars)
      suggest_undec = any_bad &&
                      not undec_inst &&
                      (lhs_vars `subVarSet` fvVarSet (injectiveVarsOfType True rhs))

-- When the type family is not injective in any arguments
unusedInjTvsInRHS :: DynFlags
                  -> TyCon  -- type family
                  -> [Type] -- LHS arguments
                  -> Type   -- the RHS
                  -> ( TyVarSet
                     , Bool   -- True <=> one or more variable is used invisibly
                     , Bool )
unusedInjTvsInRHS dflags tycon@(tyConInjectivityInfo -> Injective inj_list) lhs rhs =
  -- Note [Coverage condition for injective type families], step 5
  (bad_vars, any_invisible, suggest_undec)
    where
      undec_inst = xopt LangExt.UndecidableInstances dflags

      inj_lhs = filterByList inj_list lhs
      lhs_vars = tyCoVarsOfTypes inj_lhs

      rhs_inj_vars = fvVarSet $ injectiveVarsOfType undec_inst rhs

      bad_vars = lhs_vars `minusVarSet` rhs_inj_vars

      any_bad = not $ isEmptyVarSet bad_vars

      invis_vars = fvVarSet $ invisibleVarsOfTypes [mkTyConApp tycon lhs, rhs]

      any_invisible = any_bad && (bad_vars `intersectsVarSet` invis_vars)
      suggest_undec = any_bad &&
                      not undec_inst &&
                      (lhs_vars `subVarSet` fvVarSet (injectiveVarsOfType True rhs))

-- When the type family is not injective in any arguments
unusedInjTvsInRHS dflags tycon@(tyConInjectivityInfo -> Injective inj_list) lhs rhs =
  -- Note [Coverage condition for injective type families], step 5
  (bad_vars, any_invisible, suggest_undec)
    where
      undec_inst = xopt LangExt.UndecidableInstances dflags

      inj_lhs = filterByList inj_list lhs
      lhs_vars = tyCoVarsOfTypes inj_lhs

      rhs_inj_vars = fvVarSet $ injectiveVarsOfType undec_inst rhs

      bad_vars = lhs_vars `minusVarSet` rhs_inj_vars

      any_bad = not $ isEmptyVarSet bad_vars

      invis_vars = fvVarSet $ invisibleVarsOfTypes [mkTyConApp tycon lhs, rhs]

      any_invisible = any_bad && (bad_vars `intersectsVarSet` invis_vars)
      suggest_undec = any_bad &&
                      not undec_inst &&
                      (lhs_vars `subVarSet` fvVarSet (injectiveVarsOfType True rhs))

-- When the type family is not injective in any arguments