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}.

11 files changed, 167 insertions, 73 deletions

diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs
index fbae18f797..f15b335fd7 100644
--- a/compiler/GHC/Core/Reduction.hs
+++ b/compiler/GHC/Core/Reduction.hs
@@ -469,7 +469,7 @@ unzipRedns = foldr accRedn (Reductions [] [])
 --
 --   unzipRedns <$> zipWithM f tys roles
 --
--- - GHC.Tc.Solver.Monad.breakTyVarCycle_maybe, with two calls of the form:
+-- - GHC.Tc.Solver.Monad.breakTyEqCycle_maybe, with two calls of the form:
 --
 --   unzipRedns <$> mapM f tys
 --
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index f63cb5c030..81aa291785 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -2354,7 +2354,6 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
      -- type families are OK here
      -- NB: no occCheckExpand here; see Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite
 
-
               -- a ~R# b a is soluble if b later turns out to be Identity
              result = case eq_rel of
                         NomEq  -> result0
@@ -2367,27 +2366,27 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
                  ; continueWith (CEqCan { cc_ev = new_ev, cc_lhs = lhs
                                         , cc_rhs = rhs, cc_eq_rel = eq_rel }) }
 
-         else do { m_stuff <- breakTyVarCycle_maybe ev result lhs rhs
-                           -- See Note [Type variable cycles];
+         else do { m_stuff <- breakTyEqCycle_maybe ev result lhs rhs
+                           -- See Note [Type equality cycles];
                            -- returning Nothing is the vastly common case
                  ; case m_stuff of
                      { Nothing ->
                          do { traceTcS "canEqCanLHSFinish can't make a canonical"
                                        (ppr lhs $$ ppr rhs)
                             ; continueWith (mkIrredCt reason new_ev) }
-                     ; Just (lhs_tv, rhs_redn@(Reduction _ new_rhs)) ->
+                     ; Just rhs_redn@(Reduction _ new_rhs) ->
               do { traceTcS "canEqCanLHSFinish breaking a cycle" $
                             ppr lhs $$ ppr rhs
                  ; traceTcS "new RHS:" (ppr new_rhs)
 
                    -- This check is Detail (1) in the Note
-                 ; if cterHasOccursCheck (checkTyVarEq lhs_tv new_rhs)
+                 ; if cterHasOccursCheck (checkTypeEq lhs new_rhs)
 
-                   then do { traceTcS "Note [Type variable cycles] Detail (1)"
+                   then do { traceTcS "Note [Type equality cycles] Detail (1)"
                                       (ppr new_rhs)
                            ; continueWith (mkIrredCt reason new_ev) }
 
-                   else do { -- See Detail (6) of Note [Type variable cycles]
+                   else do { -- See Detail (6) of Note [Type equality cycles]
                              new_new_ev <- rewriteEqEvidence emptyRewriterSet
                                              new_ev NotSwapped
                                              (mkReflRedn Nominal lhs_ty)
@@ -2553,7 +2552,7 @@ NOT (necessarily) expand the type synonym, since for the purpose of
 good error messages we want to leave type synonyms unexpanded as much
 as possible.  Hence the ps_xi1, ps_xi2 argument passed to canEqCanLHS.
 
-Note [Type variable cycles]
+Note [Type equality cycles]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this situation (from indexed-types/should_compile/GivenLoop):
 
@@ -2567,14 +2566,20 @@ or (typecheck/should_compile/T19682b):
   *[W] alpha ~ (Arg alpha -> Res alpha)
   [W] C alpha
 
+or (typecheck/should_compile/T21515):
+
+  type family Code a
+  *[G] Code a ~ '[ '[ Head (Head (Code a)) ] ]
+  [W] Code a ~ '[ '[ alpha ] ]
+
 In order to solve the final Wanted, we must use the starred constraint
-for rewriting. But note that both starred constraints have occurs-check failures,
+for rewriting. But note that all starred constraints have occurs-check failures,
 and so we can't straightforwardly add these to the inert set and
 use them for rewriting. (NB: A rigid type constructor is at the
-top of both RHSs. If the type family were at the top, we'd just reorient
-in canEqTyVarFunEq.)
+top of all RHSs, preventing reorienting in canEqTyVarFunEq in the tyvar
+cases.)
 
-The key idea is to replace the type family applications in the RHS of the
+The key idea is to replace the outermost type family applications in the RHS of the
 starred constraints with a fresh variable, which we'll call a cycle-breaker
 variable, or cbv. Then, relate the cbv back with the original type family application
 via new equality constraints. Our situations thus become:
@@ -2592,8 +2597,14 @@ or
   [W] Res alpha ~ cbv2
   [W] C alpha
 
+or
+
+  [G] Code a ~ '[ '[ cbv ] ]
+  [G] Head (Head (Code a)) ~ cbv
+  [W] Code a ~ '[ '[ alpha ] ]
+
 This transformation (creating the new types and emitting new equality
-constraints) is done in breakTyVarCycle_maybe.
+constraints) is done in breakTyEqCycle_maybe.
 
 The details depend on whether we're working with a Given or a Wanted.
 
@@ -2614,30 +2625,30 @@ Of course, we don't want our fresh variables leaking into e.g. error messages.
 So we fill in the metavariables with their original type family applications
 after we're done running the solver (in nestImplicTcS and runTcSWithEvBinds).
 This is done by restoreTyVarCycles, which uses the inert_cycle_breakers field in
-InertSet, which contains the pairings invented in breakTyVarCycle_maybe.
+InertSet, which contains the pairings invented in breakTyEqCycle_maybe.
 
 That is:
 
 We transform
-  [G] g : a ~ ...(F a)...
+  [G] g : lhs ~ ...(F lhs)...
 to
-  [G] (Refl a) : F a ~ cbv      -- CEqCan
-  [G] g        : a ~ ...cbv...  -- CEqCan
+  [G] (Refl lhs) : F lhs ~ cbv      -- CEqCan
+  [G] g          : lhs ~ ...cbv...  -- CEqCan
 
 Note that
 * `cbv` is a fresh cycle breaker variable.
 * `cbv` is a is a meta-tyvar, but it is completely untouchable.
 * We track the cycle-breaker variables in inert_cycle_breakers in InertSet
-* We eventually fill in the cycle-breakers, with `cbv := F a`.
+* We eventually fill in the cycle-breakers, with `cbv := F lhs`.
   No one else fills in cycle-breakers!
-* In inert_cycle_breakers, we remember the (cbv, F a) pair; that is, we
-  remember the /original/ type.  The [G] F a ~ cbv constraint may be rewritten
-  by other givens (eg if we have another [G] a ~ (b,c), but at the end we
-  still fill in with cbv := F a
+* The evidence for the new `F lhs ~ cbv` constraint is Refl, because we know
+  this fill-in is ultimately going to happen.
+* In inert_cycle_breakers, we remember the (cbv, F lhs) pair; that is, we
+  remember the /original/ type.  The [G] F lhs ~ cbv constraint may be rewritten
+  by other givens (eg if we have another [G] lhs ~ (b,c)), but at the end we
+  still fill in with cbv := F lhs
 * This fill-in is done when solving is complete, by restoreTyVarCycles
   in nestImplicTcS and runTcSWithEvBinds.
-* The evidence for the new `F a ~ cbv` constraint is Refl, because we know this fill-in is
-  ultimately going to happen.
 
 Wanted
 ------
@@ -2655,12 +2666,18 @@ and we turn this into
 
 where cbv1 and cbv2 are fresh TauTvs. Why TauTvs? See [Why TauTvs] below.
 
-Critically, we emit the constraint directly instead of calling unifyWanted.
+Critically, we emit the two new constraints (the last two above)
+directly instead of calling unifyWanted. (Otherwise, we'd end up unifying cbv1
+and cbv2 immediately, achieving nothing.)
 Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
-unification happens in the course of normal behavior of top-level
+unification -- which must be the next step after breaking the cycles --
+happens in the course of normal behavior of top-level
 interactions, later in the solver pipeline. We know this unification will
-indeed happen, because breakTyVarCycle_maybe, which decides whether to apply
-this logic, goes to pains to make sure unification will succeed. Now, we're
+indeed happen because breakTyEqCycle_maybe, which decides whether to apply
+this logic, checks to ensure unification will succeed in its final_check.
+(In particular, the LHS must be a touchable tyvar, never a type family. We don't
+yet have an example of where this logic is needed with a type family, and it's
+unclear how to handle this case, so we're skipping for now.) Now, we're
 here (including further context from our original example, from the top of the
 Note):
 
@@ -2735,8 +2752,9 @@ In all cases
 ------------
 
 We detect this scenario by the following characteristics:
- - a constraint with a tyvar on its LHS
- - with a soluble occurs-check failure
+ - a constraint with a soluble occurs-check failure
+   (as indicated by the cteSolubleOccurs bit set in a CheckTyEqResult
+   from checkTypeEq)
  - and a nominal equality
  - and either
     - a Given flavour (but see also Detail (7) below)
@@ -2761,29 +2779,31 @@ Details:
 
  (1) We don't look under foralls, at all, when substituting away type family
      applications, because doing so can never be fruitful. Recall that we
-     are in a case like [G] a ~ forall b. ... a ....   Until we have a type
-     family that can pull the body out from a forall, this will always be
+     are in a case like [G] lhs ~ forall b. ... lhs ....   Until we have a type
+     family that can pull the body out from a forall (e.g. type instance F (forall b. ty) = ty),
+     this will always be
      insoluble. Note also that the forall cannot be in an argument to a
      type family, or that outer type family application would already have
      been substituted away.
 
-     However, we still must check to make sure that breakTyVarCycle_maybe actually
-     succeeds in getting rid of all occurrences of the offending variable. If
+     However, we still must check to make sure that breakTyEqCycle_maybe actually
+     succeeds in getting rid of all occurrences of the offending lhs. If
      one is hidden under a forall, this won't be true. A similar problem can
      happen if the variable appears only in a kind
      (e.g. k ~ ... (a :: k) ...). So we perform an additional check after
-     performing the substitution. It is tiresome to re-run all of checkTyVarEq
+     performing the substitution. It is tiresome to re-run all of checkTypeEq
      here, but reimplementing just the occurs-check is even more tiresome.
 
      Skipping this check causes typecheck/should_fail/GivenForallLoop and
      polykinds/T18451 to loop.
 
  (2) Our goal here is to avoid loops in rewriting. We can thus skip looking
-     in coercions, as we don't rewrite in coercions. (This is another reason
+     in coercions, as we don't rewrite in coercions in the algorithm in
+     GHC.Solver.Rewrite. (This is another reason
      we need to re-check that we've gotten rid of all occurrences of the
      offending variable.)
 
- (3) As we're substituting, we can build ill-kinded
+ (3) As we're substituting as described in this Note, we can build ill-kinded
      types. For example, if we have Proxy (F a) b, where (b :: F a), then
      replacing this with Proxy cbv b is ill-kinded. However, we will later
      set cbv := F a, and so the zonked type will be well-kinded again.
@@ -2801,11 +2821,16 @@ Details:
 
  (4) The evidence for the produced Givens is all just reflexive, because
      we will eventually set the cycle-breaker variable to be the type family,
-     and then, after the zonk, all will be well.
-
- (5) The approach here is inefficient. For instance, we could choose to
-     affect only type family applications that mention the offending variable:
-     in a ~ (F b, G a), we need to replace only G a, not F b. Furthermore,
+     and then, after the zonk, all will be well. See also the notes at the
+     end of the Given section of this Note.
+
+ (5) The approach here is inefficient because it replaces every (outermost)
+     type family application with a type variable, regardless of whether that
+     particular appplication is implicated in the occurs check.  An alternative
+     would be to replce only type-family applications that meantion the offending LHS.
+     For instance, we could choose to
+     affect only type family applications that mention the offending LHS:
+     e.g. in a ~ (F b, G a), we need to replace only G a, not F b. Furthermore,
      we could try to detect cases like a ~ (F a, F a) and use the same
      tyvar to replace F a. (Cf.
      Note [Flattening type-family applications when matching instances]
@@ -2816,9 +2841,10 @@ Details:
      performant solution seems unworthwhile.
 
  (6) We often get the predicate associated with a constraint from its
-     evidence. We thus must not only make sure the generated CEqCan's
-     fields have the updated RHS type, but we must also update the
-     evidence itself. This is done by the call to rewriteEqEvidence
+     evidence with ctPred. We thus must not only make sure the generated
+     CEqCan's fields have the updated RHS type (that is, the one produced
+     by replacing type family applications with fresh variables),
+     but we must also update the evidence itself. This is done by the call to rewriteEqEvidence
      in canEqCanLHSFinish.
 
  (7) We don't wish to apply this magic on the equalities created
@@ -2858,12 +2884,14 @@ Details:
      occurs-check bit set (only).
 
      We track these equalities by giving them a special CtOrigin,
-     CycleBreakerOrigin. This works for both Givens and WDs, as
+     CycleBreakerOrigin. This works for both Givens and Wanteds, as
      we need the logic in the W case for e.g. typecheck/should_fail/T17139.
+     Because this logic needs to work for Wanteds, too, we cannot
+     simply look for a CycleBreakerTv on the left: Wanteds don't use them.
 
  (8) We really want to do this all only when there is a soluble occurs-check
      failure, not when other problems arise (such as an impredicative
-     equality like alpha ~ forall a. a -> a). That is why breakTyVarCycle_maybe
+     equality like alpha ~ forall a. a -> a). That is why breakTyEqCycle_maybe
      uses cterHasOnlyProblem when looking at the result of checkTypeEq, which
      checks for many of the invariants on a CEqCan.
 -}
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index f7d0eb0701..4de3ca8d1f 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -240,7 +240,7 @@ type CycleBreakerVarStack = NonEmpty [(TcTyVar, TcType)]
    -- first element in the stack corresponds to current implication;
    --   later elements correspond to outer implications
    -- used to undo the cycle-breaking needed to handle
-   -- Note [Type variable cycles] in GHC.Tc.Solver.Canonical
+   -- Note [Type equality cycles] in GHC.Tc.Solver.Canonical
    -- Why store the outer implications? For the use in mightEqualLater (only)
 
 data InertSet
@@ -1693,7 +1693,7 @@ This is best understood by example.
    where cbv = F a
 
    The cbv is a cycle-breaker var which stands for F a. See
-   Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
+   Note [Type equality cycles] in GHC.Tc.Solver.Canonical.
    This is just like case 6, and we say "no". Saying "no" here is
    essential in getting the parser to type-check, with its use of DisambECP.
 
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 8721068b8c..99c35f826d 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -113,7 +113,7 @@ module GHC.Tc.Solver.Monad (
                                              -- if the whole instance matcher simply belongs
                                              -- here
 
-    breakTyVarCycle_maybe, rewriterView
+    breakTyEqCycle_maybe, rewriterView
 ) where
 
 import GHC.Prelude
@@ -934,7 +934,7 @@ runTcSWithEvBinds = runTcSWithEvBinds' True False
 
 runTcSWithEvBinds' :: Bool -- ^ Restore type variable cycles afterwards?
                            -- Don't if you want to reuse the InertSet.
-                           -- See also Note [Type variable cycles]
+                           -- See also Note [Type equality cycles]
                            -- in GHC.Tc.Solver.Canonical
                    -> Bool
                    -> EvBindsVar
@@ -1898,21 +1898,20 @@ solverDepthError loc ty
 
 -- | Conditionally replace all type family applications in the RHS with fresh
 -- variables, emitting givens that relate the type family application to the
--- variable. See Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
+-- variable. See Note [Type equality cycles] in GHC.Tc.Solver.Canonical.
 -- This only works under conditions as described in the Note; otherwise, returns
 -- Nothing.
-breakTyVarCycle_maybe :: CtEvidence
-                      -> CheckTyEqResult   -- result of checkTypeEq
-                      -> CanEqLHS
-                      -> TcType     -- RHS
-                      -> TcS (Maybe (TcTyVar, ReductionN))
+breakTyEqCycle_maybe :: CtEvidence
+                     -> CheckTyEqResult   -- result of checkTypeEq
+                     -> CanEqLHS
+                     -> TcType     -- RHS
+                     -> TcS (Maybe ReductionN)
                          -- new RHS that doesn't have any type families
-                         -- TcTyVar is the LHS tv; convenient for the caller
-breakTyVarCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _
+breakTyEqCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _
   -- see Detail (7) of Note
   = return Nothing
 
-breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
+breakTyEqCycle_maybe ev cte_result lhs rhs
   | NomEq <- eq_rel
 
   , cte_result `cterHasOnlyProblem` cteSolubleOccurs
@@ -1921,7 +1920,7 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
 
   = do { should_break <- final_check
        ; if should_break then do { redn <- go rhs
-                                 ; return (Just (lhs_tv, redn)) }
+                                 ; return (Just redn) }
                          else return Nothing }
   where
     flavour = ctEvFlavour ev
@@ -1929,10 +1928,14 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
 
     final_check = case flavour of
       Given  -> return True
-      Wanted -> do { result <- touchabilityTest Wanted lhs_tv rhs
-                   ; return $ case result of
-                       Untouchable -> False
-                       _           -> True }
+      Wanted    -- Wanteds work only with a touchable tyvar on the left
+                -- See "Wanted" section of the Note.
+        | TyVarLHS lhs_tv <- lhs ->
+          do { result <- touchabilityTest Wanted lhs_tv rhs
+             ; return $ case result of
+                          Untouchable -> False
+                          _           -> True }
+        | otherwise -> return False
 
     -- This could be considerably more efficient. See Detail (5) of Note.
     go :: TcType -> TcS ReductionN
@@ -1977,7 +1980,7 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
                                                  fun_app new_ty
                  given_term = evCoercion $ mkNomReflCo new_ty  -- See Detail (4) of Note
            ; new_given <- newGivenEvVar new_loc (given_pred, given_term)
-           ; traceTcS "breakTyVarCycle replacing type family in Given" (ppr new_given)
+           ; traceTcS "breakTyEqCycle replacing type family in Given" (ppr new_given)
            ; emitWorkNC [new_given]
            ; updInertTcS $ \is ->
                is { inert_cycle_breakers = insertCycleBreakerBinding new_tv fun_app
@@ -1995,10 +1998,10 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
     new_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
 
 -- does not fit scenario from Note
-breakTyVarCycle_maybe _ _ _ _ = return Nothing
+breakTyEqCycle_maybe _ _ _ _ = return Nothing
 
 -- | Fill in CycleBreakerTvs with the variables they stand for.
--- See Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
+-- See Note [Type equality cycles] in GHC.Tc.Solver.Canonical.
 restoreTyVarCycles :: InertSet -> TcM ()
 restoreTyVarCycles is
   = forAllCycleBreakerBindings_ (inert_cycle_breakers is) TcM.writeMetaTyVar
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 8582d5c549..caee214db9 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -605,7 +605,7 @@ data CtOrigin
 
   | CycleBreakerOrigin
       CtOrigin   -- origin of the original constraint
-      -- See Detail (7) of Note [Type variable cycles] in GHC.Tc.Solver.Canonical
+      -- See Detail (7) of Note [Type equality cycles] in GHC.Tc.Solver.Canonical
   | FRROrigin
       FixedRuntimeRepOrigin
 
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 5561e9064e..c44ceba426 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -870,7 +870,7 @@ cloneAnonMetaTyVar info tv kind
         ; traceTc "cloneAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar))
         ; return tyvar }
 
--- Make a new CycleBreakerTv. See Note [Type variable cycles]
+-- Make a new CycleBreakerTv. See Note [Type equality cycles]
 -- in GHC.Tc.Solver.Canonical.
 newCycleBreakerTyVar :: TcKind -> TcM TcTyVar
 newCycleBreakerTyVar kind
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index b40c77c11b..e9c643fe71 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -640,7 +640,7 @@ data MetaInfo
                    -- It /is/ allowed to unify with a polytype, unlike TauTv
 
    | CycleBreakerTv  -- Used to fix occurs-check problems in Givens
-                     -- See Note [Type variable cycles] in
+                     -- See Note [Type equality cycles] in
                      -- GHC.Tc.Solver.Canonical
 
    | ConcreteTv ConcreteTvOrigin
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, [''])