[Git][ghc/ghc][wip/T22623] Fix an assertion check in addToEqualCtList

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T22623 at Glasgow Haskell Compiler / GHC


Commits:
e3289d7e by Simon Peyton Jones at 2022-12-19T23:26:06+00:00
Fix an assertion check in addToEqualCtList

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

- - - - -


4 changed files:

- compiler/GHC/Tc/Solver/Types.hs
- + testsuite/tests/typecheck/should_fail/T22645.hs
- + testsuite/tests/typecheck/should_fail/T22645.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
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


=====================================
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


=====================================
testsuite/tests/typecheck/should_fail/T22645.stderr
=====================================
@@ -0,0 +1,17 @@
+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)
+  |
+9 | p = coerce
+  |     ^^^^^^


=====================================
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, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e3289d7e1e554b3c54dd605125b63930b606dd5a

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e3289d7e1e554b3c54dd605125b63930b606dd5a
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221219/e6d37650/attachment-0001.html>