Fix scoping of implicit parameterswip/T17104

There was an outright bug in TcInteract.solveOneFromTheOther
which meant that we did not always pick the innermost
implicit parameter binding, causing #17104.

The fix is easy, just a rearrangement of conditional tests

4 files changed, 33 insertions, 3 deletions

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index f6a4f92164..e946d04a23 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -559,9 +559,10 @@ solveOneFromTheOther ev_i ev_w
      ev_id_w = ctEvEvId ev_w
 
      different_level_strategy  -- Both Given
-       | isIPPred pred, lvl_w > lvl_i = KeepWork
-       | lvl_w < lvl_i                = KeepWork
-       | otherwise                    = KeepInert
+       | isIPPred pred = if lvl_w > lvl_i then KeepWork  else KeepInert
+       | otherwise     = if lvl_w > lvl_i then KeepInert else KeepWork
+       -- See Note [Replacement vs keeping] (the different-level bullet)
+       -- For the isIPPred case see Note [Shadowing of Implicit Parameters]
 
      same_level_strategy binds -- Both Given
        | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
@@ -1246,6 +1247,9 @@ This should probably be well typed, with
 
 So the inner binding for ?x::Bool *overrides* the outer one.
 
+See ticket #17104 for a rather tricky example of this overriding
+behaviour.
+
 All this works for the normal cases but it has an odd side effect in
 some pathological programs like this:
 -- This is accepted, the second parameter shadows
diff --git a/testsuite/tests/typecheck/should_run/T17104.hs b/testsuite/tests/typecheck/should_run/T17104.hs
new file mode 100644
index 0000000000..8cf3b5fda1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T17104.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Main where
+
+import GHC.Exts
+import Data.Type.Equality
+
+type family F x :: Constraint
+type instance F Int = (?x :: String)
+
+data Box where MkBox :: (?x :: String) => Box
+data Box2 a where MkBox2 :: F a => Box2 a
+
+f :: Box2 a -> Box -> a :~: Int -> String
+f MkBox2 MkBox Refl = ?x
+
+main :: IO ()
+main = do { let mb  = let ?x = "right"  in MkBox
+          ; let mb2 = let ?x = "wrong" in MkBox2
+          ; print (f mb2 mb Refl) }
diff --git a/testsuite/tests/typecheck/should_run/T17104.stdout b/testsuite/tests/typecheck/should_run/T17104.stdout
new file mode 100644
index 0000000000..f2bb7441cf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T17104.stdout
@@ -0,0 +1 @@
+"right"
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index 05fddcb0b0..512362f1bb 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -140,3 +140,4 @@ test('UnliftedNewtypesFamilyRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesDependentFamilyRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesIdentityRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesCoerceRun', normal, compile_and_run, [''])
+test('T17104', normal, compile_and_run, [''])