From 21b76843e9b51cd27be32b8c595f29a784276229 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date: Sun, 29 Oct 2023 21:26:54 +0000
Subject: [PATCH] Fix non-termination bug in equality solver
constraint left-to-right then right to left, forever.
Easily fixed.
---
compiler/GHC/Tc/Solver/Equality.hs | 14 +++--
.../indexed-types/should_compile/T24134.hs | 54 +++++++++++++++++++
.../tests/indexed-types/should_compile/all.T | 1 +
3 files changed, 65 insertions(+), 4 deletions(-)
create mode 100644 testsuite/tests/indexed-types/should_compile/T24134.hs
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index e9411481a2bd..dec78905f6d6 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/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
diff --git a/testsuite/tests/indexed-types/should_compile/T24134.hs b/testsuite/tests/indexed-types/should_compile/T24134.hs
new file mode 100644
index 000000000000..0c60855a6e05
--- /dev/null
+++ b/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
+
+
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 35fa39086087..e4d3c3c8d50e 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/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, [''])
--
GitLab