Fix an assertion check in addToEqualCtList

The old assertion saw that a constraint ct could rewrite itself
(of course it can) and complained (stupid).

Fixes #22645

4 files changed, 42 insertions, 9 deletions

diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs
index 4c52721638..e6ee09b0d8 100644
--- a/compiler/GHC/Tc/Solver/Types.hs
+++ b/compiler/GHC/Tc/Solver/Types.hs
@@ -273,21 +273,29 @@ addToEqualCtList ct old_eqs
   | debugIsOn
   = case ct of
       CEqCan { cc_lhs = TyVarLHS tv } ->
-        let shares_lhs (CEqCan { cc_lhs = TyVarLHS old_tv }) = tv == old_tv
-            shares_lhs _other                                = False
-        in
-        assert (all shares_lhs old_eqs) $
-        assert (null ([ (ct1, ct2) | ct1 <- ct : old_eqs
-                                   , ct2 <- ct : old_eqs
-                                   , let { fr1 = ctFlavourRole ct1
-                                         ; fr2 = ctFlavourRole ct2 }
-                                   , fr1 `eqCanRewriteFR` fr2 ])) $
+        assert (all (shares_lhs tv) old_eqs) $
+        assertPpr (null bad_prs)
+                  (vcat [ text "bad_prs" <+> ppr bad_prs
+                        , text "ct:old_eqs" <+> ppr (ct : old_eqs) ]) $
         (ct : old_eqs)
 
       _ -> pprPanic "addToEqualCtList not CEqCan" (ppr ct)
 
   | otherwise
   = ct : old_eqs
+  where
+    shares_lhs tv (CEqCan { cc_lhs = TyVarLHS old_tv }) = tv == old_tv
+    shares_lhs _ _ = False
+    bad_prs = filter is_bad_pair (distinctPairs (ct : old_eqs))
+    is_bad_pair (ct1,ct2) = ctFlavourRole ct1 `eqCanRewriteFR` ctFlavourRole ct2
+
+distinctPairs :: [a] -> [(a,a)]
+-- distinctPairs [x1,...xn] is the list of all pairs [ ...(xi, xj)...]
+--                             where i /= j
+-- NB: does not return pairs (xi,xi), which would be stupid in the
+--     context of addToEqualCtList (#22645)
+distinctPairs []     = []
+distinctPairs (x:xs) = concatMap (\y -> [(x,y),(y,x)]) xs ++ distinctPairs xs
 
 -- returns Nothing when the new list is empty, to keep the environments smaller
 filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
diff --git a/testsuite/tests/typecheck/should_fail/T22645.hs b/testsuite/tests/typecheck/should_fail/T22645.hs
new file mode 100644
index 0000000000..ee5f03d180
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22645.hs
@@ -0,0 +1,9 @@
+module T22645 where
+
+import Data.Coerce
+
+type T :: (* -> *) -> * -> *
+data T m a = MkT (m a)
+
+p :: Coercible a b => T Maybe a -> T Maybe b
+p = coerce
diff --git a/testsuite/tests/typecheck/should_fail/T22645.stderr b/testsuite/tests/typecheck/should_fail/T22645.stderr
new file mode 100644
index 0000000000..359d6c5b73
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22645.stderr
@@ -0,0 +1,15 @@
+
+T22645.hs:9:5: error: [GHC-25897]
+    • Couldn't match type ‘a’ with ‘b’ arising from a use of ‘coerce’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
+        at T22645.hs:8:1-44
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
+        at T22645.hs:8:1-44
+    • In the expression: coerce
+      In an equation for ‘p’: p = coerce
+    • Relevant bindings include
+        p :: T Maybe a -> T Maybe b (bound at T22645.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index a99792e5ab..7d7b7f0369 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -666,3 +666,4 @@ test('T21447', normal, compile_fail, [''])
 test('T21530a', normal, compile_fail, [''])
 test('T21530b', normal, compile_fail, [''])
 test('T22570', normal, compile_fail, [''])
+test('T22645', normal, compile_fail, [''])