[Git][ghc/ghc][master] Fix non-termination bug in equality solver
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Tue Oct 31 00:37:43 UTC 2023
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>
More information about the ghc-commits
mailing list