[Git][ghc/ghc][master] Fix non-termination bug in equality solver

[Marge Bot (@marge-bot)]

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
21b76843 by Simon Peyton Jones at 2023-10-30T20:37:17-04:00
Fix non-termination bug in equality solver

constraint left-to-right then right to left, forever.

Easily fixed.

- - - - -


3 changed files:

- compiler/GHC/Tc/Solver/Equality.hs
- + testsuite/tests/indexed-types/should_compile/T24134.hs
- testsuite/tests/indexed-types/should_compile/all.T


Changes:

=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1721,12 +1721,16 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
              swap_for_size = typesSize fun_args2 > typesSize fun_args1
 
              -- See Note [Orienting TyFamLHS/TyFamLHS]
-             swap_for_rewriting = anyVarSet (isTouchableMetaTyVar tclvl) tvs2 &&
+             meta_tv_lhs = anyVarSet (isTouchableMetaTyVar tclvl) tvs1
+             meta_tv_rhs = anyVarSet (isTouchableMetaTyVar tclvl) tvs2
+             swap_for_rewriting = meta_tv_rhs && not meta_tv_lhs
                                   -- See Note [Put touchable variables on the left]
-                                  not (anyVarSet (isTouchableMetaTyVar tclvl) tvs1)
                                   -- This second check is just to avoid unfruitful swapping
 
-       ; if swap_for_rewriting || swap_for_size
+         -- It's important that we don't flip-flop (#T24134)
+         -- So swap_for_rewriting "wins", and we only try swap_for_size
+         -- if swap_for_rewriting doesn't care either way
+       ; if swap_for_rewriting || (meta_tv_lhs == meta_tv_rhs && swap_for_size)
          then finish_with_swapping
          else finish_without_swapping } }
   where
@@ -1945,7 +1949,9 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
               -- If we had F a ~ G (F a), which gives an occurs check,
               -- then swap it to G (F a) ~ F a, which does not
               -- However `swap_for_size` above will orient it with (G (F a)) on
-              -- the left anwyway, so the next four lines of code are redundant
+              -- the left anwyway.  `swap_for_rewriting` "wins", but that doesn't
+              -- matter: in the occurs check case swap_for_rewriting will be moot.
+              -- TL;DR: the next four lines of code are redundant
               -- I'm leaving them here in case they become relevant again
 --              | TyFamLHS {} <- lhs
 --              , Just can_rhs <- canTyFamEqLHS_maybe rhs


=====================================
testsuite/tests/indexed-types/should_compile/T24134.hs
=====================================
@@ -0,0 +1,54 @@
+{-# LANGUAGE GHC2021 #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module M where
+import Data.Kind (Type)
+
+type F :: Type -> Type
+type family F
+
+type Prod :: Type -> Type -> Type
+type family Prod (a :: Type) (b :: Type) :: Type
+
+und :: F Int
+und = und
+
+f :: a -> Prod (F Int) a -> Prod a a
+f = f
+
+repMap :: Prod (F Int) (F Int) -> Prod (F Int) (F Int)
+repMap = f und
+
+
+{- This is what went wrong in GHC 9.8
+
+Inert: [W] Prod (F Int) a ~ Prod a a
+Work: [W] Prod (F Int) (F Int) ~ Prof (F Int) a
+
+---> rewrite with inert
+  [W] Prod (F Int) (F Int) ~ Prod a a
+---> swap (meta-var to left)
+  [W] Prod a a ~ Prod (F Int) (F Int)
+
+Kick out the inert
+
+Inert: [W] Prod a a ~ Prod (F Int) (F Int)
+Work: [W] Prod (F Int) a ~ Prod a a
+
+--> rewrite with inert
+    [W] Prod (F Int) a ~ Prod (F Int) (F Int)
+--> swap (size)
+    [W] Prod (F Int) (F Int) ~ Prod (F Int) a
+
+Kick out the inert
+
+Inert: [W] Prod (F Int) (F Int) ~ Prod (F Int) a
+Work: [W] Prod a a ~ Prod (F Int) (F Int)
+
+--> rewrite with inert
+    [W] Prod a a ~ Prod (F Int) a
+--> swap (size)
+    [W] Prof (F Int) a ~ Prod a a
+
+
+-}


=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -309,3 +309,4 @@ test('T22547', normal, compile, [''])
 test('T22717', normal, makefile_test, ['T22717'])
 test('T22717_fam_orph', normal, multimod_compile, ['T22717_fam_orph', '-v0'])
 test('T23408', normal, compile, [''])
+test('T24134', normal, compile, [''])



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/21b76843e9b51cd27be32b8c595f29a784276229
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/20231030/9d28a1d6/attachment-0001.html>