content: {-# LANGUAGE AllowAmbiguousTypes, TypeFamilies #-}
  
  module T5837 where
  
  import Data.Kind
  
  type family TF a :: Type
  type instance TF (a,b) = (TF a, TF b)
  
  t :: (a ~ TF (a,Int)) => Int
  t = undefined
  
  {-
  
           [G] a ~ TF (a,Int)               -- a = a_am1
  -->
           [G] TF (a,Int) ~ fsk             -- fsk = fsk_am8
  
  inert    [G] fsk ~ a
  
  ---> reduce
           [G] fsk ~ (TF a, TF Int)
  
  inert    [G] fsk ~ a
  
  ---> substitute for fsk and flatten
           [G] TF a ~ fsk1
           [G] TF Int ~ fsk2
  
  inert    [G] fsk ~ a
           [G] a ~ (fsk1, fsk2)
  
  ---> (substitute for a in first constraint)
           TF (fsk1, fsk2) ~ fsk1     (C1)
           TF Int ~ fsk2
  
  inert    a ~ (fsk2, TF Int)
  inert    fsk ~ (fsk2, TF Int)
  
  
  ------- At this point we are stuck because of
  --      the recursion in the first constraint C1
  --      Hooray
  
  -- Before, we reduced C1, which led to a loop
  
  ---> (top-level reduction, re-orient)
           fsk2 ~ (TF fsk2, TF Int)
  inert    a ~ (fsk2, TF Int)
  inert    fsk ~ (fsk2, TF Int)
  
  ---> (attempt to flatten (TF fsk2) to get rid of fsk2
           TF fsk2 ~ fsk3
           fsk2 ~ (fsk3, TF Int)
  inert    a   ~ (fsk2, TF Int)
  inert    fsk ~ (fsk2, TF Int)
  
  --->
           TF fsk2 ~ fsk3
  inert    fsk2 ~ (fsk3, TF Int)
  inert    a   ~ ((fsk3, TF Int), TF Int)
  inert    fsk ~ ((fsk3, TF Int), TF Int)
  
  -}
  