Generalize breakTyVarCycle to work with TyFamLHS

The function breakTyVarCycle_maybe has been installed
in a dark corner of GHC to catch some gremlins (a.k.a.
occurs-check failures) who lurk
there. But it previously only caught gremlins of the
form (a ~ ... F a ...), where some of our intrepid users
have spawned gremlins of the form (G a ~ ... F (G a) ...).
This commit improves breakTyVarCycle_maybe (and renames
it to breakTyEqCycle_maybe) to catch the new gremlins.

Happily, the change is remarkably small.

The gory details are in Note [Type equality cycles].

Test cases: typecheck/should_compile/{T21515,T21473}.

4 files changed, 64 insertions, 1 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T18875.hs b/testsuite/tests/indexed-types/should_compile/T18875.hs
index 0121f5ff12..f3874005b9 100644
--- a/testsuite/tests/indexed-types/should_compile/T18875.hs
+++ b/testsuite/tests/indexed-types/should_compile/T18875.hs
@@ -2,7 +2,7 @@
 
 module T18875 where
 
--- This exercises Note [Type variable cycles] in GHC.Tc.Solver.Canonical
+-- This exercises Note [Type equality cycles] in GHC.Tc.Solver.Canonical
 
 type family G a b where
   G (Maybe c) d = d
diff --git a/testsuite/tests/typecheck/should_compile/T21473.hs b/testsuite/tests/typecheck/should_compile/T21473.hs
new file mode 100644
index 0000000000..b9e4961f06
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21473.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE ConstraintKinds, DataKinds, TypeOperators, GADTs #-}
+{-# LANGUAGE TypeFamilies, KindSignatures, FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+module Reproducer where
+
+import Data.Kind (Type, Constraint)
+
+data Dict (c :: Constraint) where
+  Dict :: c => Dict c
+
+class Foo (e :: Type) (r :: [Type])
+
+instance Foo e (e ': r)
+
+type family R :: [Type]
+type family F (a :: [Type]) :: [Type]
+
+compiles :: (R ~ Int ': F R, r ~ R)
+         => Dict (Foo Int R)
+compiles = Dict
+
+errors :: (R ~ Int ': F R)
+       => Dict (Foo Int R)
+errors = Dict
diff --git a/testsuite/tests/typecheck/should_compile/T21515.hs b/testsuite/tests/typecheck/should_compile/T21515.hs
new file mode 100644
index 0000000000..c6f7181bd8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21515.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T21515 where
+
+import Data.Kind
+
+type family Code a :: [[Type]]
+
+type IsWrappedType a x = Code a ~ '[ '[ x ] ]
+type IsProductType a xs = Code a ~ '[ xs ]
+
+type family Head (xs :: [a]) :: a where
+  Head (x : xs) = x
+
+type ProductCode a = Head (Code a)
+type WrappedCode a = Head (Head (Code a))
+
+wrappedTypeTo :: IsWrappedType a x => x -> a
+wrappedTypeTo = undefined
+
+to :: SOP (Code a) -> a
+to = undefined
+
+data SOP (xss :: [[a]])
+
+type WrappedProduct a = (IsWrappedType a (WrappedCode a), IsProductType (WrappedCode a) (ProductCode (WrappedCode a)))
+
+process :: (SOP '[ xs ] -> a) -> a
+process = undefined
+
+-- works with 8.10 and 9.0, fails with 9.2
+test :: WrappedProduct a => a
+test = process (wrappedTypeTo . to)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 00d36bd3a4..f08828eeea 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -354,6 +354,8 @@ test('T5490', normal, compile, [''])
 test('T5514', normal, compile, [''])
 test('T5581', normal, compile, [''])
 test('T5655', normal, compile, [''])
+test('T21515', normal, compile, [''])
+test('T21473', normal, compile, [''])
 test('T5643', normal, compile, [''])
 test('T5595', normal, compile, [''])
 test('T5676', normal, compile, [''])