When solving one Given from another, use the depth to control which way round

See Note [Replacement vs keeping].

There's a bit further to go with this change (to report unused givens).
But it's already an improvement; see the latent bug described in the Note.

4 files changed, 60 insertions, 8 deletions

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 8b85a712e9..79a61a306a 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -450,7 +450,11 @@ interactWithInertsStage wi
                 -- CHoleCan are put straight into inert_frozen, so never get here
                 -- CNonCanonical have been canonicalised
 
-data InteractResult = IRKeep | IRReplace | IRDelete
+data InteractResult
+   = IRKeep      -- Keep the existing inert constraint in the inert set
+   | IRReplace   -- Replace the existing inert constraint with the work item
+   | IRDelete    -- Delete the existing inert constraint from the inert set
+
 instance Outputable InteractResult where
   ppr IRKeep    = ptext (sLit "keep")
   ppr IRReplace = ptext (sLit "replace")
@@ -479,12 +483,57 @@ solveOneFromTheOther ev_i ev_w
   = do { setEvBind ev_id (ctEvTerm ev_w)
        ; return (IRReplace, True) }
 
-  | otherwise      -- If both are Given, we already have evidence; no need to duplicate
-                   -- But the work item *overrides* the inert item (hence IRReplace)
-                   -- See Note [Shadowing of Implicit Parameters]
-  = return (IRReplace, True)
+  | otherwise   -- Both are Given
+  = return (if use_replacement then IRReplace else IRKeep, True)
+
+  where
+    pred  = ctEvPred ev_i
+    loc_i = ctEvLoc ev_i
+    loc_w = ctEvLoc ev_w
+    lvl_i = ctLocLevel loc_i
+    lvl_w = ctLocLevel loc_w
+
+    use_replacement  -- See Note [Replacement vs keeping]
+      | isIPPred pred = lvl_w > lvl_i
+      | otherwise     = lvl_w < lvl_i
 
 {-
+Note [Replacement vs keeping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we have two Given constraints both of type (C tys), say, which should
+we keep?
+
+  * For implicit parameters we want to keep the innermost (deepest)
+    one, so that it overrides the outer one.
+    See Note [Shadowing of Implicit Parameters]
+
+  * For everything else, we want to keep the outermost one.  Reason: that
+    makes it more likely that the inner one will turn out to be unused,
+    and can be reported as redundant.
+
+When there is a choice, use IRKeep rather than IRReplace, to avoid unnecesary
+munging of the inert set.
+
+Doing the depth-check for implicit parameters, rather than making the work item
+always overrride, is important.  Consider
+
+    data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
+
+    f :: (?x::a) => T a -> Int
+    f T1 = ?x
+    f T2 = 3
+
+We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
+two new givens in the work-list:  [G] (?x::Int)
+                                  [G] (a ~ Int)
+Now consider these steps
+  - process a~Int, kicking out (?x::a)
+  - process (?x::Int), the inner given, adding to inert set
+  - process (?x::a), the outer given, overriding the inner given
+Wrong!  The depth-check ensures that the inner implicit parameter wins.
+(Actually I think that the order in which the work-list is processed means
+that this chain of events won't happen, but that's very fragile.)
+
 *********************************************************************************
 *                                                                               *
                    interactIrred
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 31624a8b9e..c2cc36d7b9 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -67,7 +67,7 @@ module TcRnTypes(
         SubGoalCounter(..),
         SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
         bumpSubGoalDepth, subGoalCounterValue, subGoalDepthExceeded,
-        CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin,
+        CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin, setCtLocEnv, setCtLocSpan,
         CtOrigin(..), pprCtOrigin,
@@ -1835,6 +1835,9 @@ mkGivenLoc tclvl skol_info env
 ctLocEnv :: CtLoc -> TcLclEnv
 ctLocEnv = ctl_env
 
+ctLocLevel :: CtLoc -> TcLevel
+ctLocLevel loc = tcl_tclvl (ctLocEnv loc)
+
 ctLocDepth :: CtLoc -> SubGoalDepth
 ctLocDepth = ctl_depth
 
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index d62f098849..d7c58d502a 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -828,7 +828,7 @@ getNoGivenEqs tclvl skol_tvs
     -- i.e. the current level
     ev_given_here ev
       =  isGiven ev
-      && tclvl == tcl_tclvl (ctl_env (ctEvLoc ev))
+      && tclvl == ctLocLevel (ctEvLoc ev)
 
     add_fsk :: Ct -> VarSet -> VarSet
     add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index e760cc46ba..e0ce00f8ea 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -414,7 +414,7 @@ data UserTypeCtxt
 ************************************************************************
 -}
 
-newtype TcLevel = TcLevel Int deriving( Eq )
+newtype TcLevel = TcLevel Int deriving( Eq, Ord )
   -- See Note [TcLevel and untouchable type variables] for what this Int is
 
 {-