Improve redundant-constraints warning

Previously, we reported things wrong with

  f :: (Eq a, Ord a) => a -> Bool
  f x = x == x

saying that Eq a was redundant. This is fixed now, along with
some simplification in Note [Replacement vs keeping]. There's
a tiny bit of extra complexity in setImplicationStatus, but
it's explained in Note [Tracking redundant constraints].

Close #20602

8 files changed, 158 insertions, 93 deletions

diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 0250078b62..a53f070e10 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1766,7 +1766,7 @@ tcPragExpr is_compulsory toplvl name expr
     core_expr' <- tcIfaceExpr expr
 
     -- Check for type consistency in the unfolding
-    -- See Note [Linting Unfoldings from Interfaces]
+    -- See Note [Linting Unfoldings from Interfaces] in GHC.Core.Lint
     when (isTopLevel toplvl) $
       whenGOptM Opt_DoCoreLinting $ do
         in_scope <- get_in_scope
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 2edd1bad8d..e276ad16d9 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -2055,19 +2055,28 @@ setImplicationStatus implic@(Implic { ic_status     = status
 
       ; bad_telescope <- checkBadTelescope implic
 
-      ; let dead_givens | warnRedundantGivens info
-                        = filterOut (`elemVarSet` need_inner) givens
-                        | otherwise = []   -- None to report
+      ; let (used_givens, unused_givens)
+              | warnRedundantGivens info
+              = partition (`elemVarSet` need_inner) givens
+              | otherwise = (givens, [])   -- None to report
+
+            minimal_used_givens = mkMinimalBySCs evVarPred used_givens
+            is_minimal = (`elemVarSet` mkVarSet minimal_used_givens)
+
+            warn_givens
+              | not (null unused_givens) = unused_givens
+              | warnRedundantGivens info = filterOut is_minimal used_givens
+              | otherwise                = []
 
             discard_entire_implication  -- Can we discard the entire implication?
-              =  null dead_givens           -- No warning from this implication
+              =  null warn_givens           -- No warning from this implication
               && not bad_telescope
               && isEmptyWC pruned_wc        -- No live children
               && isEmptyVarSet need_outer   -- No needed vars to pass up to parent
 
             final_status
               | bad_telescope = IC_BadTelescope
-              | otherwise     = IC_Solved { ics_dead = dead_givens }
+              | otherwise     = IC_Solved { ics_dead = warn_givens }
             final_implic = implic { ic_status = final_status
                                   , ic_wanted = pruned_wc }
 
@@ -2298,7 +2307,10 @@ Note [Tracking redundant constraints]
 With Opt_WarnRedundantConstraints, GHC can report which
 constraints of a type signature (or instance declaration) are
 redundant, and can be omitted.  Here is an overview of how it
-works:
+works.
+
+This is all tested in typecheck/should_compile/T20602 (among
+others).
 
 ----- What is a redundant constraint?
 
@@ -2306,29 +2318,26 @@ works:
   constraints of an implication.
 
 * A constraint can be redundant in two different ways:
-  a) It is implied by other givens.  E.g.
-       f :: (Eq a, Ord a)     => blah   -- Eq a unnecessary
-       g :: (Eq a, a~b, Eq b) => blah   -- Either Eq a or Eq b unnecessary
-  b) It is not needed by the Wanted constraints covered by the
+  a) It is not needed by the Wanted constraints covered by the
      implication E.g.
        f :: Eq a => a -> Bool
        f x = True  -- Equality not used
+  b) It is implied by other givens.  E.g.
+       f :: (Eq a, Ord a)     => blah   -- Eq a unnecessary
+       g :: (Eq a, a~b, Eq b) => blah   -- Either Eq a or Eq b unnecessary
 
-*  To find (a), when we have two Given constraints,
-   we must be careful to drop the one that is a naked variable (if poss).
-   So if we have
-       f :: (Eq a, Ord a) => blah
-   then we may find [G] sc_sel (d1::Ord a) :: Eq a
-                    [G] d2 :: Eq a
-   We want to discard d2 in favour of the superclass selection from
-   the Ord dictionary.  This is done by GHC.Tc.Solver.Interact.solveOneFromTheOther
-   See Note [Replacement vs keeping].
+*  To find (a) we need to know which evidence bindings are 'wanted';
+   hence the eb_is_given field on an EvBind.
 
-* To find (b) we need to know which evidence bindings are 'wanted';
-  hence the eb_is_given field on an EvBind.
+*  To find (b), we use mkMinimalBySCs on the Givens to see if any
+   are unnecessary.
 
 ----- How tracking works
 
+* When two Givens are the same, we drop the evidence for the one
+  that requires more superclass selectors. This is done
+  according to Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
+
 * The ic_need fields of an Implic records in-scope (given) evidence
   variables bound by the context, that were needed to solve this
   implication (so far).  See the declaration of Implication.
@@ -2342,9 +2351,15 @@ works:
 * We compute which evidence variables are needed by an implication
   in setImplicationStatus.  A variable is needed if
     a) it is free in the RHS of a Wanted EvBind,
-    b) it is free in the RHS of an EvBind whose LHS is needed,
+    b) it is free in the RHS of an EvBind whose LHS is needed, or
     c) it is in the ics_need of a nested implication.
 
+* After computing which variables are needed, we then look at the
+  remaining variables for internal redundancies. This is case (b)
+  from above. This is also done in setImplicationStatus.
+  Note that we only look for case (b) if case (a) shows up empty,
+  as exemplified below.
+
 * We need to be careful not to discard an implication
   prematurely, even one that is fully solved, because we might
   thereby forget which variables it needs, and hence wrongly
@@ -2353,6 +2368,32 @@ works:
   simply has no free vars. This careful discarding is also
   handled in setImplicationStatus.
 
+* Examples:
+
+    f, g, h :: (Eq a, Ord a) => a -> Bool
+    f x = x == x
+    g x = x > x
+    h x = x == x && x > x
+
+    All three will discover that they have two [G] Eq a constraints:
+    one as given and one extracted from the Ord a constraint. They will
+    both discard the latter, as noted above and in
+    Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
+
+    The body of f uses the [G] Eq a, but not the [G] Ord a. It will
+    report a redundant Ord a using the logic for case (a).
+
+    The body of g uses the [G] Ord a, but not the [G] Eq a. It will
+    report a redundant Eq a using the logic for case (a).
+
+    The body of h uses both [G] Ord a and [G] Eq a. Case (a) will
+    thus come up with nothing redundant. But then, the case (b)
+    check will discover that Eq a is redundant and report this.
+
+    If we did case (b) even when case (a) reports something, then
+    we would report both constraints as redundant for f, which is
+    terrible.
+
 ----- Reporting redundant constraints
 
 * GHC.Tc.Errors does the actual warning, in warnRedundantConstraints.
@@ -2383,13 +2424,18 @@ works:
 
 ----- Shortcomings
 
-Consider (see #9939)
-    f2 :: (Eq a, Ord a) => a -> a -> Bool
-    -- Ord a redundant, but Eq a is reported
-    f2 x y = (x == y)
+Consider
+
+  j :: (Eq a, a ~ b) => a -> Bool
+  j x = x == x
+
+  k :: (Eq a, b ~ a) => a -> Bool
+  k x = x == x
 
-We report (Eq a) as redundant, whereas actually (Ord a) is.  But it's
-really not easy to detect that!
+Currently (Nov 2021), j issues no warning, while k says that b ~ a
+is redundant. This is because j uses the a ~ b constraint to rewrite
+everything to be in terms of b, while k does none of that. This is
+ridiculous, but I (Richard E) don't see a good fix.
 
 -}
 
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index eb205e71cb..5a504211f0 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -588,11 +588,18 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
 
        | GivenOrigin skol_info <- ctLocOrigin loc
          -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-         -- for explantation of this transformation for givens
-       = case skol_info of
-            InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
-            InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
-            _        -> loc
+         -- for explantation of InstSC and Note [Replacement vs keeping] in
+         -- GHC.Tc.Solver.Interact for why we need OtherSC and depths
+       = let new_skol_info = case skol_info of
+            -- these cases are when we have something that's already a superclass constraint
+               InstSC  sc_depth n  -> InstSC  (sc_depth + 1) (n `max` size)
+               OtherSC sc_depth si -> OtherSC (sc_depth + 1) si
+
+            -- these cases do not already have a superclass constraint: depth starts at 1
+               InstSkol -> InstSC 1 size
+               _        -> OtherSC 1 skol_info
+         in
+         loc { ctl_origin = GivenOrigin new_skol_info }
 
        | otherwise  -- Probably doesn't happen, since this function
        = loc        -- is only used for Givens, but does no harm
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index f5e6fda5c3..0ab5f5facb 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -1649,7 +1649,7 @@ mightEqualLater (IS { inert_cycle_breakers = cbvs })
 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
 -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
 prohibitedSuperClassSolve from_loc solve_loc
-  | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
+  | GivenOrigin (InstSC _ given_size) <- ctLocOrigin from_loc
   , ScOrigin wanted_size <- ctLocOrigin solve_loc
   = given_size >= wanted_size
   | otherwise
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index ff3b3e7fcd..a1bd9f7d0b 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -50,7 +50,6 @@ import GHC.Types.SrcLoc
 import GHC.Types.Var.Env
 
 import Control.Monad
-import GHC.Data.Maybe( isJust )
 import GHC.Data.Pair (Pair(..))
 import GHC.Types.Unique( hasKey )
 import GHC.Driver.Session
@@ -526,9 +525,7 @@ solveOneFromTheOther ev_i ev_w
   -- See Note [Replacement vs keeping]
 
   | lvl_i == lvl_w
-  = do { ev_binds_var <- getTcEvBindsVar
-       ; binds <- getTcEvBindsMap ev_binds_var
-       ; return (same_level_strategy binds) }
+  = return same_level_strategy
 
   | otherwise   -- Both are Given, levels differ
   = return different_level_strategy
@@ -538,8 +535,6 @@ solveOneFromTheOther ev_i ev_w
      loc_w = ctEvLoc ev_w
      lvl_i = ctLocLevel loc_i
      lvl_w = ctLocLevel loc_w
-     ev_id_i = ctEvEvId ev_i
-     ev_id_w = ctEvEvId ev_w
 
      different_level_strategy  -- Both Given
        | isIPLikePred pred = if lvl_w > lvl_i then KeepWork  else KeepInert
@@ -547,33 +542,40 @@ solveOneFromTheOther ev_i ev_w
        -- See Note [Replacement vs keeping] (the different-level bullet)
        -- For the isIPLikePred case see Note [Shadowing of Implicit Parameters]
 
-     same_level_strategy binds -- Both Given
-       | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
-       = case ctLocOrigin loc_w of
-            GivenOrigin (InstSC s_w) | s_w < s_i -> KeepWork
-                                     | otherwise -> KeepInert
-            _                                    -> KeepWork
+     same_level_strategy -- Both Given
+       = case (un_given (ctLocOrigin loc_i), un_given (ctLocOrigin loc_w)) of
+              -- case 2(b) from Note [Replacement vs keeping]
+           (InstSC _depth_i size_i, InstSC _depth_w size_w) | size_w < size_i -> KeepWork
+                                                            | otherwise       -> KeepInert
 
-       | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
-       = KeepInert
+              -- case 2(c) from Note [Replacement vs keeping]
+           (InstSC depth_i _, OtherSC depth_w _)  -> choose_shallower depth_i depth_w
+           (OtherSC depth_i _, InstSC depth_w _)  -> choose_shallower depth_i depth_w
+           (OtherSC depth_i _, OtherSC depth_w _) -> choose_shallower depth_i depth_w
 
-       | has_binding binds ev_id_w
-       , not (has_binding binds ev_id_i)
-       , not (ev_id_i `elemVarSet` findNeededEvVars binds (unitVarSet ev_id_w))
-       = KeepWork
+              -- case 2(a) from Note [Replacement vs keeping]
+           (InstSC {}, _)                         -> KeepWork
+           (OtherSC {}, _)                        -> KeepWork
 
-       | otherwise
-       = KeepInert
+             -- case 2(d) from Note [Replacement vs keeping]
+           _                                      -> KeepInert
+
+     un_given (GivenOrigin skol_info) = skol_info
+     un_given orig = pprPanic "Given without GivenOrigin in solveOneFromTheOther" $
+                     vcat [ppr ev_i, ppr ev_w, ppr orig]
 
-     has_binding binds ev_id = isJust (lookupEvBind binds ev_id)
+     choose_shallower depth_i depth_w | depth_w < depth_i = KeepWork
+                                      | otherwise         = KeepInert
+       -- favor KeepInert in the equals case, according to 2(d) from the Note
 
 {-
 Note [Replacement vs keeping]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we have two Given constraints both of type (C tys), say, which should
-we keep?  More subtle than you might think!
+we keep?  More subtle than you might think! This is all implemented in
+solveOneFromTheOther.
 
-  * Constraints come from different levels (different_level_strategy)
+  1) Constraints come from different levels (different_level_strategy)
 
       - For implicit parameters we want to keep the innermost (deepest)
         one, so that it overrides the outer one.
@@ -588,36 +590,33 @@ we keep?  More subtle than you might think!
         8% performance improvement in nofib cryptarithm2, compared to
         just rolling the dice.  I didn't investigate why.
 
-  * Constraints coming from the same level (i.e. same implication)
-
-       (a) Always get rid of InstSC ones if possible, since they are less
-           useful for solving.  If both are InstSC, choose the one with
-           the smallest TypeSize
-           See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-
-       (b) Keep the one that has a non-trivial evidence binding.
-              Example:  f :: (Eq a, Ord a) => blah
-              then we may find [G] d3 :: Eq a
-                               [G] d2 :: Eq a
-                with bindings  d3 = sc_sel (d1::Ord a)
-            We want to discard d2 in favour of the superclass selection from
-            the Ord dictionary.
-            Why? See Note [Tracking redundant constraints] in GHC.Tc.Solver again.
-
-       (c) But don't do (b) if the evidence binding depends transitively on the
-           one without a binding.  Example (with RecursiveSuperClasses)
-              class C a => D a
-              class D a => C a
-           Inert:     d1 :: C a, d2 :: D a
-           Binds:     d3 = sc_sel d2, d2 = sc_sel d1
-           Work item: d3 :: C a
-           Then it'd be ridiculous to replace d1 with d3 in the inert set!
-           Hence the findNeedEvVars test.  See #14774.
-
-  * Finally, when there is still a choice, use KeepInert rather than
-    KeepWork, for two reasons:
-      - to avoid unnecessary munging of the inert set.
-      - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Canonical
+  2) Constraints coming from the same level (i.e. same implication)
+
+       (a) Prefer constraints that are not superclass selections. Example:
+
+             f :: (Eq a, Ord a) => a -> Bool
+             f x = x == x
+
+           Eager superclass expansion gives us two [G] Eq a constraints. We
+           want to keep the one from the user-written Eq a, not the superclass
+           selection. This means we report the Ord a as redundant with
+           -Wredundant-constraints, not the Eq a.
+
+           Getting this wrong was #20602. See also
+           Note [Tracking redundant constraints] in GHC.Tc.Solver.
+
+       (b) If both are InstSC, choose the one with the smallest TypeSize,
+           according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
+
+       (c) If both are superclass selections (but not both InstSC), choose the one
+           with the shallower superclass-selection depth, in the hope of identifying
+           more correct redundant constraints. This is really a generalization of
+           point (a).
+
+       (d) Finally, when there is still a choice, use KeepInert rather than
+           KeepWork, for two reasons:
+             - to avoid unnecessary munging of the inert set.
+             - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Canonical
 
 Doing the depth-check for implicit parameters, rather than making the work item
 always override, is important.  Consider
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index f6ebd07c04..26e1689e59 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -1604,7 +1604,8 @@ Answer:
     a SkolemInfo of (InstSC size), where 'size' is the size of
     the constraint whose superclass we are taking.  A similarly
     when taking the superclass of an InstSC.  This is implemented
-    in GHC.Tc.Solver.Canonical.newSCWorkFromFlavored
+    in GHC.Tc.Solver.Canonical.mk_strict_superclasses (in the
+    mk_given_loc helper function).
 
 Note [Silent superclass arguments] (historical interest only)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index a88bf27480..7953336a6b 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -219,12 +219,22 @@ data SkolemInfo
                         -- the type is the instance we are trying to derive
 
   | InstSkol            -- Bound at an instance decl
-  | InstSC TypeSize     -- A "given" constraint obtained by superclass selection.
-                        -- If (C ty1 .. tyn) is the largest class from
+
+  -- | A "given" constraint obtained by superclass selection.
+  | InstSC Int          -- ^ The number of superclass selections necessary to
+                        -- get this constraint; see Note [Replacement vs keeping] in
+                        -- GHC.Tc.Solver.Interact
+           TypeSize     -- ^ If @(C ty1 .. tyn)@ is the largest class from
                         --    which we made a superclass selection in the chain,
-                        --    then TypeSize = sizeTypes [ty1, .., tyn]
+                        --    then @TypeSize = sizeTypes [ty1, .., tyn]@
                         -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
 
+  -- | A "given" constraint obtained by superclass selection, but not from an instance context.
+  -- Needed for Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
+  | OtherSC Int    -- ^ The number of superclass selections necessary to
+                   -- get this constraint
+            SkolemInfo   -- ^ Where the sub-class constraint arose from
+
   | FamInstSkol         -- Bound at a family instance decl
   | PatSkol             -- An existential type variable bound by a pattern for
       ConLike           -- a data constructor with an existential type.
@@ -274,7 +284,8 @@ pprSkolInfo (IPSkol ips)      = text "the implicit-parameter binding" <> plural
                                  <+> pprWithCommas ppr ips
 pprSkolInfo (DerivSkol pred)  = text "the deriving clause for" <+> quotes (ppr pred)
 pprSkolInfo InstSkol          = text "the instance declaration"
-pprSkolInfo (InstSC n)        = text "the instance declaration" <> whenPprDebug (parens (ppr n))
+pprSkolInfo (InstSC _ n)      = text "the instance declaration" <> whenPprDebug (parens (ppr n))
+pprSkolInfo (OtherSC _ si)    = pprSkolInfo si  -- superclass constraints don't bind skolems
 pprSkolInfo FamInstSkol       = text "a family instance declaration"
 pprSkolInfo BracketSkol       = text "a Template Haskell bracket"
 pprSkolInfo (RuleSkol name)   = text "the RULE" <+> pprRuleName name
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index d4637705b0..65c5d3a50e 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -2428,6 +2428,7 @@ zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
                                      ; return (InferSkol ntys') }
   where
     do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
+zonkSkolemInfo (OtherSC depth si) = OtherSC depth <$> zonkSkolemInfo si
 zonkSkolemInfo skol_info = return skol_info
 
 {-