Do proper depth checking in the flattener to avoid looping.

This implements (roughly) the plan put forward in comment:14:ticket:7788,
fixing #7788, #8550, #9554, #10139, and addressing concerns raised in #10079.
There are some regressions w.r.t. GHC 7.8, but only with pathological type
families (like F a = F a). This also (hopefully -- don't have a test case)
fixes #10158. Unsolved problems include #10184 and #10185, which are both
known deficiencies of the approach used here.

As part of this change, the plumbing around detecting infinite loops has
changed. Instead of -fcontext-stack and -ftype-function-depth, we now have
one combined -freduction-depth parameter. Setting it to 0 disbales the
check, which is now the recommended way to get (terminating) code to
typecheck in releases. (The number of reduction steps may well change between
minor GHC releases!)

This commit also introduces a new IntWithInf type in BasicTypes
that represents an integer+infinity. This type is used in a few
places throughout the code.

Tests in
  indexed-types/should_fail/T7788
  indexed-types/should_fail/T8550
  indexed-types/should_fail/T9554
  indexed-types/should_compile/T10079
  indexed-types/should_compile/T10139
  typecheck/should_compile/T10184  (expected broken)
  typecheck/should_compile/T10185  (expected broken)

This commit also changes performance testsuite numbers, for the better.

59 files changed, 1136 insertions, 1048 deletions

diff --git a/compiler/basicTypes/BasicTypes.hs b/compiler/basicTypes/BasicTypes.hs
index 973666d0f8..cf1bf58e9d 100644
--- a/compiler/basicTypes/BasicTypes.hs
+++ b/compiler/basicTypes/BasicTypes.hs
@@ -86,7 +86,9 @@ module BasicTypes(
 
         HValue(..),
 
-        SourceText
+        SourceText,
+
+        IntWithInf, infinity, treatZeroAsInf, mkIntWithInf
    ) where
 
 import FastString
@@ -1113,3 +1115,68 @@ instance Outputable FractionalLit where
   ppr = text . fl_text
 
 newtype HValue = HValue Any
+
+{-
+************************************************************************
+*                                                                      *
+    IntWithInf
+*                                                                      *
+************************************************************************
+
+Represents an integer or positive infinity
+
+-}
+
+-- | An integer or infinity
+data IntWithInf = Int {-# UNPACK #-} !Int
+                | Infinity
+  deriving Eq
+
+-- | A representation of infinity
+infinity :: IntWithInf
+infinity = Infinity
+
+instance Ord IntWithInf where
+  compare Infinity Infinity = EQ
+  compare (Int _)  Infinity = LT
+  compare Infinity (Int _)  = GT
+  compare (Int a)  (Int b)  = a `compare` b
+
+instance Outputable IntWithInf where
+  ppr Infinity = char '∞'
+  ppr (Int n)  = int n
+
+instance Num IntWithInf where
+  (+) = plusWithInf
+  (*) = mulWithInf
+
+  abs Infinity = Infinity
+  abs (Int n)  = Int (abs n)
+
+  signum Infinity = Int 1
+  signum (Int n)  = Int (signum n)
+
+  fromInteger = Int . fromInteger
+
+  (-) = panic "subtracting IntWithInfs"
+
+-- | Add two 'IntWithInf's
+plusWithInf :: IntWithInf -> IntWithInf -> IntWithInf
+plusWithInf Infinity _        = Infinity
+plusWithInf _        Infinity = Infinity
+plusWithInf (Int a)  (Int b)  = Int (a + b)
+
+-- | Multiply two 'IntWithInf's
+mulWithInf :: IntWithInf -> IntWithInf -> IntWithInf
+mulWithInf Infinity _        = Infinity
+mulWithInf _        Infinity = Infinity
+mulWithInf (Int a)  (Int b)  = Int (a * b)
+
+-- | Turn a positive number into an 'IntWithInf', where 0 represents infinity
+treatZeroAsInf :: Int -> IntWithInf
+treatZeroAsInf 0 = Infinity
+treatZeroAsInf n = Int n
+
+-- | Inject any integer into an 'IntWithInf'
+mkIntWithInf :: Int -> IntWithInf
+mkIntWithInf = Int
diff --git a/compiler/main/Constants.hs b/compiler/main/Constants.hs
index 0054888df3..0f23fc242e 100644
--- a/compiler/main/Constants.hs
+++ b/compiler/main/Constants.hs
@@ -17,13 +17,10 @@ mAX_TUPLE_SIZE :: Int
 mAX_TUPLE_SIZE = 62 -- Should really match the number
                     -- of decls in Data.Tuple
 
-mAX_CONTEXT_REDUCTION_DEPTH :: Int
-mAX_CONTEXT_REDUCTION_DEPTH = 100
-  -- Trac #5395 reports at least one library that needs depth 37 here
-
-mAX_TYPE_FUNCTION_REDUCTION_DEPTH :: Int
-mAX_TYPE_FUNCTION_REDUCTION_DEPTH = 200
-  -- Needs to be much higher than mAX_CONTEXT_REDUCTION_DEPTH; see Trac #5395
+-- | Default maximum depth for both class instance search and type family
+-- reduction. See also Trac #5395.
+mAX_REDUCTION_DEPTH :: Int
+mAX_REDUCTION_DEPTH = 200
 
 wORD64_SIZE :: Int
 wORD64_SIZE = 8
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 8e0499f249..eea16ddbe4 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -168,6 +168,7 @@ import Maybes
 import MonadUtils
 import qualified Pretty
 import SrcLoc
+import BasicTypes       ( IntWithInf, treatZeroAsInf )
 import FastString
 import Outputable
 #ifdef GHCI
@@ -692,8 +693,7 @@ data DynFlags = DynFlags {
   importPaths           :: [FilePath],
   mainModIs             :: Module,
   mainFunIs             :: Maybe String,
-  ctxtStkDepth          :: Int,         -- ^ Typechecker context stack depth
-  tyFunStkDepth         :: Int,         -- ^ Typechecker type function stack depth
+  reductionDepth        :: IntWithInf,   -- ^ Typechecker maximum stack depth
 
   thisPackage           :: PackageKey,   -- ^ name of package currently being compiled
 
@@ -1451,8 +1451,7 @@ defaultDynFlags mySettings =
         importPaths             = ["."],
         mainModIs               = mAIN,
         mainFunIs               = Nothing,
-        ctxtStkDepth            = mAX_CONTEXT_REDUCTION_DEPTH,
-        tyFunStkDepth           = mAX_TYPE_FUNCTION_REDUCTION_DEPTH,
+        reductionDepth          = treatZeroAsInf mAX_REDUCTION_DEPTH,
 
         thisPackage             = mainPackageKey,
 
@@ -2610,10 +2609,16 @@ dynamic_flags = [
       (noArg (\d -> d{ liberateCaseThreshold = Nothing }))
   , defFlag "frule-check"
       (sepArg (\s d -> d{ ruleCheck = Just s }))
+  , defFlag "freduction-depth"
+      (intSuffix (\n d -> d{ reductionDepth = treatZeroAsInf n }))
   , defFlag "fcontext-stack"
-      (intSuffix (\n d -> d{ ctxtStkDepth = n }))
+      (intSuffixM (\n d ->
+       do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
+          ; return $ d{ reductionDepth = treatZeroAsInf n } }))
   , defFlag "ftype-function-depth"
-      (intSuffix (\n d -> d{ tyFunStkDepth = n }))
+      (intSuffixM (\n d ->
+       do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
+          ; return $ d{ reductionDepth = treatZeroAsInf n } }))
   , defFlag "fstrictness-before"
       (intSuffix (\n d -> d{ strictnessBefore = n : strictnessBefore d }))
   , defFlag "ffloat-lam-args"
@@ -3566,6 +3571,9 @@ sepArg fn = SepArg (upd . fn)
 intSuffix :: (Int -> DynFlags -> DynFlags) -> OptKind (CmdLineP DynFlags)
 intSuffix fn = IntSuffix (\n -> upd (fn n))
 
+intSuffixM :: (Int -> DynFlags -> DynP DynFlags) -> OptKind (CmdLineP DynFlags)
+intSuffixM fn = IntSuffix (\n -> updM (fn n))
+
 floatSuffix :: (Float -> DynFlags -> DynFlags) -> OptKind (CmdLineP DynFlags)
 floatSuffix fn = FloatSuffix (\n -> upd (fn n))
 
diff --git a/compiler/simplCore/SimplMonad.hs b/compiler/simplCore/SimplMonad.hs
index fbf23d7436..7eb6a54ced 100644
--- a/compiler/simplCore/SimplMonad.hs
+++ b/compiler/simplCore/SimplMonad.hs
@@ -30,6 +30,7 @@ import Outputable
 import FastString
 import MonadUtils
 import ErrUtils
+import BasicTypes          ( IntWithInf, treatZeroAsInf, mkIntWithInf )
 import Control.Monad       ( when, liftM, ap )
 
 {-
@@ -52,11 +53,10 @@ newtype SimplM result
   -- we only need IO here for dump output
 
 data SimplTopEnv
-  = STE { st_flags :: DynFlags
-        , st_max_ticks :: Int  -- Max #ticks in this simplifier run
-                               -- Zero means infinity!
-        , st_rules :: RuleBase
-        , st_fams  :: (FamInstEnv, FamInstEnv) }
+  = STE { st_flags     :: DynFlags
+        , st_max_ticks :: IntWithInf  -- Max #ticks in this simplifier run
+        , st_rules     :: RuleBase
+        , st_fams      :: (FamInstEnv, FamInstEnv) }
 
 initSmpl :: DynFlags -> RuleBase -> (FamInstEnv, FamInstEnv)
          -> UniqSupply          -- No init count; set to 0
@@ -73,14 +73,15 @@ initSmpl dflags rules fam_envs us size m
               , st_max_ticks = computeMaxTicks dflags size
               , st_fams = fam_envs }
 
-computeMaxTicks :: DynFlags -> Int -> Int
+computeMaxTicks :: DynFlags -> Int -> IntWithInf
 -- Compute the max simplifier ticks as
 --     (base-size + pgm-size) * magic-multiplier * tick-factor/100
 -- where
 --    magic-multiplier is a constant that gives reasonable results
 --    base-size is a constant to deal with size-zero programs
 computeMaxTicks dflags size
-  = fromInteger ((toInteger (size + base_size)
+  = treatZeroAsInf $
+    fromInteger ((toInteger (size + base_size)
                   * toInteger (tick_factor * magic_multiplier))
           `div` 100)
   where
@@ -195,7 +196,7 @@ tick t = SM (\st_env us sc -> let sc' = doSimplTick (st_flags st_env) t sc
 checkedTick :: Tick -> SimplM ()
 -- Try to take a tick, but fail if too many
 checkedTick t
-  = SM (\st_env us sc -> if st_max_ticks st_env <= simplCountN sc
+  = SM (\st_env us sc -> if st_max_ticks st_env <= mkIntWithInf (simplCountN sc)
                          then pprPanic "Simplifier ticks exhausted" (msg sc)
                          else let sc' = doSimplTick (st_flags st_env) t sc
                               in sc' `seq` return ((), us, sc'))
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 0f4d97f17f..bdc67940e8 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -224,13 +224,13 @@ tcInstNewTyCon_maybe tc tys = fmap (second TcCoercion) $
 -- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
 -- there is no data family to unwrap.
 tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
-                    -> (TyCon, [TcType], TcCoercion)
+                    -> (TyCon, [TcType], Coercion)
 tcLookupDataFamInst fam_inst_envs tc tc_args
   | Just (rep_tc, rep_args, co)
       <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
-  = (rep_tc, rep_args, TcCoercion co)
+  = (rep_tc, rep_args, co)
   | otherwise
-  = (tc, tc_args, mkTcRepReflCo (mkTyConApp tc tc_args))
+  = (tc, tc_args, mkReflCo Representational (mkTyConApp tc tc_args))
 
 tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
                           -> Maybe (TyCon, [TcType], Coercion)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 6512343d9b..bb86fcd661 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -23,20 +23,19 @@ import Coercion
 import FamInstEnv ( FamInstEnvs )
 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
 import Var
-import DataCon ( dataConName )
 import Name( isSystemName, nameOccName )
 import OccName( OccName )
 import Outputable
 import DynFlags( DynFlags )
 import VarSet
 import RdrName
+import DataCon ( dataConName )
 
 import Pair
 import Util
 import MonadUtils ( zipWith3M, zipWith3M_ )
 import Data.List  ( zip4 )
 import BasicTypes
-import Data.Maybe ( isJust )
 import FastString
 
 {-
@@ -150,7 +149,9 @@ canonicalize (CTyEqCan { cc_ev = ev
                        , cc_rhs    = xi
                        , cc_eq_rel = eq_rel })
   = {-# SCC "canEqLeafTyVarEq" #-}
-    canEqTyVar ev eq_rel NotSwapped tv xi xi
+    canEqNC ev eq_rel (mkTyVarTy tv) xi
+      -- NB: Don't use canEqTyVar because that expects flattened types,
+      -- and tv and xi may not be flat w.r.t. an updated inert set
 
 canonicalize (CFunEqCan { cc_ev = ev
                         , cc_fun    = fn
@@ -409,27 +410,42 @@ canHole ev occ hole_sort
 *        Equalities
 *                                                                      *
 ************************************************************************
+
+Note [Canonicalising equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In order to canonicalise an equality, we look at the structure of the
+two types at hand, looking for similarities. A difficulty is that the
+types may look dissimilar before flattening but similar after flattening.
+However, we don't just want to jump in and flatten right away, because
+this might be wasted effort. So, after looking for similarities and failing,
+we flatten and then try again. Of course, we don't want to loop, so we
+track whether or not we've already flattened.
+
+It is conceivable to do a better job at tracking whether or not a type
+is flattened, but this is left as future work. (Mar '15)
 -}
 
 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
 canEqNC ev eq_rel ty1 ty2
-  = can_eq_nc ev eq_rel ty1 ty1 ty2 ty2
+  = can_eq_nc False ev eq_rel ty1 ty1 ty2 ty2
 
 can_eq_nc
-   :: CtEvidence
+   :: Bool            -- True => both types are flat
+   -> CtEvidence
    -> EqRel
    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp
    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp
    -> TcS (StopOrContinue Ct)
-can_eq_nc ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2 ps_ty2
   = do { traceTcS "can_eq_nc" $
          vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
        ; rdr_env <- getGlobalRdrEnvTcS
        ; fam_insts <- getFamInstEnvs
-       ; can_eq_nc' rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
+       ; can_eq_nc' flat rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
 
 can_eq_nc'
-   :: GlobalRdrEnv   -- needed to see which newtypes are in scope
+   :: Bool           -- True => both input types are flattened
+   -> GlobalRdrEnv   -- needed to see which newtypes are in scope
    -> FamInstEnvs    -- needed to unwrap data instances
    -> CtEvidence
    -> EqRel
@@ -438,41 +454,30 @@ can_eq_nc'
    -> TcS (StopOrContinue Ct)
 
 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
-can_eq_nc' _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-  | Just ty1' <- tcView ty1 = can_eq_nc ev eq_rel ty1' ps_ty1 ty2  ps_ty2
-  | Just ty2' <- tcView ty2 = can_eq_nc ev eq_rel ty1  ps_ty1 ty2' ps_ty2
-
--- Type family on LHS or RHS take priority over tyvars,
--- so that  tv ~ F ty gets flattened
--- Otherwise  F a ~ F a  might not get solved!
-can_eq_nc' _rdr_env _envs ev eq_rel (TyConApp fn1 tys1) _ ty2 ps_ty2
-  | isTypeFamilyTyCon fn1
-  = can_eq_fam_nc ev eq_rel NotSwapped fn1 tys1 ty2 ps_ty2
-can_eq_nc' _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyConApp fn2 tys2) _
-  | isTypeFamilyTyCon fn2
-  = can_eq_fam_nc ev eq_rel IsSwapped fn2 tys2 ty1 ps_ty1
-
--- When working with ReprEq, unwrap newtypes next.
--- Otherwise, a ~ Id a wouldn't get solved
-can_eq_nc' rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
+can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+  | Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2  ps_ty2
+  | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1  ps_ty1 ty2' ps_ty2
+
+-- need to check for reflexivity in the ReprEq case.
+-- See Note [AppTy reflexivity check] and Note [Eager reflexivity check]
+can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1 _ ty2 _
+  | ty1 `eqType` ty2
+  = canEqReflexive ev ReprEq ty1
+
+-- When working with ReprEq, unwrap newtypes.
+can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
   | Just (co, ty1') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
   = can_eq_newtype_nc rdr_env ev NotSwapped co ty1 ty1' ty2 ps_ty2
-can_eq_nc' rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
+can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
   | Just (co, ty2') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
   = can_eq_newtype_nc rdr_env ev IsSwapped  co ty2 ty2' ty1 ps_ty1
 
--- Type variable on LHS or RHS are next
-can_eq_nc' _rdr_env _envs ev eq_rel (TyVarTy tv1) _ ty2 ps_ty2
-  = canEqTyVar ev eq_rel NotSwapped tv1 ty2 ps_ty2
-can_eq_nc' _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) _
-  = canEqTyVar ev eq_rel IsSwapped tv2 ty1 ps_ty1
-
 ----------------------
 -- Otherwise try to decompose
 ----------------------
 
 -- Literals
-can_eq_nc' _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
+can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
  | l1 == l2
   = do { setEvBindIfWanted ev (EvCoercion $
                                mkTcReflCo (eqRelRole eq_rel) ty1)
@@ -481,27 +486,31 @@ can_eq_nc' _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
 -- Decomposable type constructor applications
 -- Synonyms and type functions (which are not decomposable)
 -- have already been dealt with
-can_eq_nc' _rdr_env _envs ev eq_rel (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
+can_eq_nc' _flat _rdr_env _envs ev eq_rel
+          (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
   | isDecomposableTyCon tc1
   , isDecomposableTyCon tc2
   = canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
 
-can_eq_nc' _rdr_env _envs ev eq_rel (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
+can_eq_nc' _flat _rdr_env _envs ev eq_rel
+           (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
   | isDecomposableTyCon tc1
       -- The guard is important
       -- e.g.  (x -> y) ~ (F x y) where F has arity 1
       --       should not fail, but get the app/app case
   = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
 
-can_eq_nc' _rdr_env _envs ev eq_rel (FunTy s1 t1) _ (FunTy s2 t2) _
+can_eq_nc' _flat _rdr_env _envs ev eq_rel (FunTy s1 t1) _ (FunTy s2 t2) _
   = do { canDecomposableTyConAppOK ev eq_rel funTyCon [s1,t1] [s2,t2]
        ; stopWith ev "Decomposed FunTyCon" }
 
-can_eq_nc' _rdr_env _envs ev eq_rel (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
+can_eq_nc' _flat _rdr_env _envs ev eq_rel
+          (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
   | isDecomposableTyCon tc2
   = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
 
-can_eq_nc' _rdr_env _envs ev eq_rel s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
+can_eq_nc' _flat _rdr_env _envs ev eq_rel
+           s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
  | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev
  = do { let (tvs1,body1) = tcSplitForAllTys s1
             (tvs2,body2) = tcSplitForAllTys s2
@@ -518,33 +527,59 @@ can_eq_nc' _rdr_env _envs ev eq_rel s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
       ; stopWith ev "Discard given polytype equality" }
 
-can_eq_nc' _rdr_env _envs ev eq_rel ty1@(AppTy {}) _ ty2 _
-  | isGiven ev = try_decompose_app ev eq_rel ty1 ty2
-  | otherwise  = can_eq_wanted_app ev eq_rel ty1 ty2
-can_eq_nc' _rdr_env _envs ev eq_rel ty1 _ ty2@(AppTy {}) _
-  | isGiven ev = try_decompose_app ev eq_rel ty1 ty2
-  | otherwise  = can_eq_wanted_app ev eq_rel ty1 ty2
-
--- Everything else is a definite type error, eg LitTy ~ TyConApp
-can_eq_nc' _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
-  = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
+-- AppTys only decompose for nominal equality
+-- See Note [Canonicalising type applications] about why we require flat types
+can_eq_nc' True _rdr_env _envs ev NomEq (AppTy t1 s1) _ ty2 _
+  | Just (t2, s2) <- tcSplitAppTy_maybe ty2
+  = can_eq_app ev t1 s1 t2 s2
+can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ (AppTy t2 s2) _
+  | Just (t1, s1) <- tcSplitAppTy_maybe ty1
+  = can_eq_app ev t1 s1 t2 s2
+
+-- See Note [AppTy reflexivity check]
+can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1@(AppTy {}) _ ty2@(AppTy {}) _
+  | ty1 `eqType` ty2
+  = canEqReflexive ev ReprEq ty1
 
-------------
-can_eq_fam_nc :: CtEvidence -> EqRel -> SwapFlag
-              -> TyCon -> [TcType]
-              -> TcType -> TcType
-              -> TcS (StopOrContinue Ct)
--- Canonicalise a non-canonical equality of form (F tys ~ ty)
---   or the swapped version thereof
--- Flatten the LHS and go round again
-can_eq_fam_nc ev eq_rel swapped fn tys rhs ps_rhs
-  = do { (xi_lhs, co_lhs) <- flattenFamApp FM_FlattenAll ev fn tys
-       ; rewriteEqEvidence ev eq_rel swapped xi_lhs rhs co_lhs
-                           (mkTcReflCo (eqRelRole eq_rel) rhs)
+-- No similarity in type structure detected. Flatten and try again!
+can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
+  = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
+       ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
+       ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2
          `andWhenContinue` \ new_ev ->
-         can_eq_nc new_ev eq_rel xi_lhs xi_lhs rhs ps_rhs }
+         can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
+
+-- Type variable on LHS or RHS are last. We want only flat types sent
+-- to canEqTyVar.
+-- See also Note [No top-level newtypes on RHS of representational equalities]
+can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
+  = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
+can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
+  = canEqTyVar ev eq_rel IsSwapped  tv2 ps_ty1
+
+-- We've flattened and the types don't match. Give up.
+can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
+  = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
 
 {-
+Note [Newtypes can blow the stack]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+
+  newtype X = MkX (Int -> X)
+  newtype Y = MkY (Int -> Y)
+
+and now wish to prove
+
+  [W] X ~R Y
+
+This Wanted will loop, expanding out the newtypes ever deeper looking
+for a solid match or a solid discrepancy. Indeed, there is something
+appropriate to this looping, because X and Y *do* have the same representation,
+in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
+coercion will ever witness it. This loop won't actually cause GHC to hang,
+though, because we check our depth when unwrapping newtypes.
+
 Note [Eager reflexivity check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have
@@ -560,21 +595,8 @@ we do this eager reflexivity check. This is necessary only for representational
 equality because the flattener technology deals with the similar case
 (recursive type families) for nominal equality.
 
-As an alternative, suppose we also have
-
-  newtype Y = MkY (Int -> Y)
-
-and now wish to prove
-
-  [W] X ~R Y
-
-This new Wanted will loop, expanding out the newtypes ever deeper looking
-for a solid match or a solid discrepancy. Indeed, there is something
-appropriate to this looping, because X and Y *do* have the same representation,
-in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
-coercion will ever witness it. This loop won't actually cause GHC to hang,
-though, because of the stack-blowing check in can_eq_newtype_nc, along
-with the fact that rewriteEqEvidence bumps the stack depth.
+Note that this check does not catch all cases, but it will catch the cases
+we're most worried about, types like X above that are actually inhabited.
 
 Note [AppTy reflexivity check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -605,25 +627,16 @@ can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2
          vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ]
 
          -- check for blowing our stack:
-         -- See Note [Eager reflexivity check] for an example of
-         -- when this is necessary
-       ; dflags <- getDynFlags
-       ; if isJust $ subGoalDepthExceeded (maxSubGoalDepth dflags)
-                                          (ctLocDepth (ctEvLoc ev))
-         then do { emitInsoluble (mkNonCanonical ev)
-                 ; stopWith ev "unwrapping newtypes blew stack" }
-         else do
-       { if ty1 `eqType` ty2   -- See Note [Eager reflexivity check]
-         then canEqReflexive ev ReprEq ty1
-         else do
-       { markDataConsAsUsed rdr_env (tyConAppTyCon ty1)
+         -- See Note [Newtypes can blow the stack]
+       ; checkReductionDepth (ctEvLoc ev) ty1
+       ; markDataConsAsUsed rdr_env (tyConAppTyCon ty1)
            -- we have actually used the newtype constructor here, so
            -- make sure we don't warn about importing it!
 
        ; rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2
                            (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
          `andWhenContinue` \ new_ev ->
-         can_eq_nc new_ev ReprEq ty1' ty1' ty2 ps_ty2 }}}
+         can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
 
 -- | Mark all the datacons of the given 'TyCon' as used in this module,
 -- avoiding "redundant import" warnings.
@@ -636,98 +649,33 @@ markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
   , gre : _               <- return $ lookupGRE_Name rdr_env dc_name
   , Imported (imp_spec:_) <- return $ gre_prov gre ]
 
--------------------------------------------------
-can_eq_wanted_app :: CtEvidence -> EqRel -> TcType -> TcType
-                  -> TcS (StopOrContinue Ct)
--- One or the other is an App; neither is a type variable
--- See Note [Canonicalising type applications]
-can_eq_wanted_app ev eq_rel ty1 ty2
-  = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
-       ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
-        ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2
-          `andWhenContinue` \ new_ev ->
-          try_decompose_app new_ev eq_rel xi1 xi2 }
-
 ---------
-try_decompose_app :: CtEvidence -> EqRel
-                  -> TcType -> TcType -> TcS (StopOrContinue Ct)
--- Preconditions: one or the other is an App;
---                but neither is a type variable
---                so can't turn it into an application if it
---                   doesn't look like one already
--- See Note [Canonicalising type applications]
-try_decompose_app ev eq_rel ty1 ty2
-  = case eq_rel of
-      NomEq  -> try_decompose_nom_app  ev ty1 ty2
-      ReprEq -> try_decompose_repr_app ev ty1 ty2
-
----------
-try_decompose_repr_app :: CtEvidence
-                       -> TcType -> TcType -> TcS (StopOrContinue Ct)
--- Preconditions: like try_decompose_app, but also
---                ev has a representational
-try_decompose_repr_app ev ty1 ty2
-  | ty1 `eqType` ty2   -- See Note [AppTy reflexivity check]
-  = canEqReflexive ev ReprEq ty1
-
-  | AppTy {} <- ty1
-  = canEqFailure ev ReprEq ty1 ty2
-
-  | AppTy {} <- ty2
-  = canEqFailure ev ReprEq ty1 ty2
-
-  | otherwise  -- flattening in can_eq_wanted_app exposed some TyConApps!
-  = ASSERT2( isJust (tcSplitTyConApp_maybe ty1) || isJust (tcSplitTyConApp_maybe ty2)
-            , ppr ty1 $$ ppr ty2 )  -- If this assertion fails, we may fall
-                                    -- into an infinite loop
-    canEqNC ev ReprEq ty1 ty2
-
----------
-try_decompose_nom_app :: CtEvidence
-                      -> TcType -> TcType -> TcS (StopOrContinue Ct)
--- Preconditions: like try_decompose_app, but also
---                ev has a nominal role
-try_decompose_nom_app ev ty1 ty2
-   | AppTy s1 t1 <- ty1
-   = case tcSplitAppTy_maybe ty2 of
-       Nothing      -> canEqHardFailure ev NomEq ty1 ty2
-       Just (s2,t2) -> do_decompose s1 t1 s2 t2
-
-   | AppTy s2 t2 <- ty2
-   = case tcSplitAppTy_maybe ty1 of
-       Nothing      -> canEqHardFailure ev NomEq ty1 ty2
-       Just (s1,t1) -> do_decompose s1 t1 s2 t2
-
-   | otherwise  -- Neither is an AppTy; but one or other started that way
-                -- (precondition to can_eq_wanted_app)
-                -- So presumably one has become a TyConApp, which
-                -- is good: See Note [Canonicalising type applications]
-   = ASSERT2( isJust (tcSplitTyConApp_maybe ty1) || isJust (tcSplitTyConApp_maybe ty2)
-            , ppr ty1 $$ ppr ty2 )  -- If this assertion fails, we may fall
-                                    -- into an infinite loop (Trac #9971)
-     canEqNC ev NomEq ty1 ty2
-   where
-     -- Recurses to try_decompose_nom_app to decompose a chain of AppTys
-     do_decompose s1 t1 s2 t2
-       | CtDerived { ctev_loc = loc } <- ev
-       = do { emitNewDerived loc (mkTcEqPred t1 t2)
-            ; canEqNC ev NomEq s1 s2 }
-       | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
-       = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
-            ; co_t <- unifyWanted loc Nominal t1 t2
-            ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
-            ; setWantedEvBind evar (EvCoercion co)
-            ; canEqNC ev_s NomEq s1 s2 }
-       | CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- ev
-       = do { let co   = evTermCoercion ev_tm
-                  co_s = mkTcLRCo CLeft  co
-                  co_t = mkTcLRCo CRight co
-            ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
-            ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
-            ; emitWorkNC [evar_t]
-            ; canEqNC evar_s NomEq s1 s2 }
-       | otherwise  -- Can't happen
-       = error "try_decompose_app"
+-- ^ Decompose a type application. Nominal equality only!
+-- All input types must be flat. See Note [Canonicalising type applications]
+can_eq_app :: CtEvidence       -- :: s1 t1 ~N s2 t2
+           -> Xi -> Xi         -- s1 t1
+           -> Xi -> Xi         -- s2 t2
+           -> TcS (StopOrContinue Ct)
+can_eq_app ev s1 t1 s2 t2
+  | CtDerived { ctev_loc = loc } <- ev
+  = do { emitNewDerived loc (mkTcEqPred t1 t2)
+       ; canEqNC ev NomEq s1 s2 }
+  | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
+  = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
+       ; co_t <- unifyWanted loc Nominal t1 t2
+       ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
+       ; setWantedEvBind evar (EvCoercion co)
+       ; canEqNC ev_s NomEq s1 s2 }
+  | CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- ev
+  = do { let co   = evTermCoercion ev_tm
+             co_s = mkTcLRCo CLeft  co
+             co_t = mkTcLRCo CRight co
+       ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
+       ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t)
+       ; emitWorkNC [evar_t]
+       ; canEqNC evar_s NomEq s1 s2 }
+  | otherwise  -- Can't happen
+  = error "can_eq_app"
 
 ------------------------
 canDecomposableTyConApp :: CtEvidence -> EqRel
@@ -796,20 +744,19 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
 
 -- | Call when canonicalizing an equality fails, but if the equality is
 -- representational, there is some hope for the future.
--- Examples in Note [Flatten irreducible representational equalities]
+-- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
 canEqFailure :: CtEvidence -> EqRel
              -> TcType -> TcType -> TcS (StopOrContinue Ct)
 canEqFailure ev ReprEq ty1 ty2
-  = do { -- See Note [Flatten irreducible representational equalities]
-         (xi1, co1) <- flatten FM_FlattenAll ev ty1
+  = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
        ; (xi2, co2) <- flatten FM_FlattenAll ev ty2
        ; traceTcS "canEqFailure with ReprEq" $
          vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
-       ; if xi1 `eqType` ty1 && xi2 `eqType` ty2
-         then continueWith (CIrredEvCan { cc_ev = ev })  -- co1/2 must be refl
+       ; if isTcReflCo co1 && isTcReflCo co2
+         then continueWith (CIrredEvCan { cc_ev = ev })
          else rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2
               `andWhenContinue` \ new_ev ->
-              can_eq_nc new_ev ReprEq xi1 xi1 xi2 xi2 }
+              can_eq_nc True new_ev ReprEq xi1 xi1 xi2 xi2 }
 canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev NomEq ty1 ty2
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
@@ -825,27 +772,6 @@ canEqHardFailure ev eq_rel ty1 ty2
        ; stopWith new_ev "Definitely not equal" }}
 
 {-
-Note [Flatten irreducible representational equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we can't make any progress with a representational equality, but
-we haven't given up all hope, we must flatten before producing the
-CIrredEvCan. There are two reasons to do this:
-
-  * See case in Note [Use canEqFailure in canDecomposableTyConApp].
-    Flattening here can expose that we know enough information to unwrap
-    a newtype.
-
-  * This case, which was encountered in the testsuite (T9117_3):
-
-      work item: [W] c1: f a ~R g a
-      inert set: [G] c2: g ~R f
-
-    In can_eq_app, we try to flatten the LHS of c1. This causes no effect,
-    because `f` cannot be rewritten. So, we go to can_eq_flat_app. Without
-    flattening the RHS, the reflexivity check fails, and we give up. However,
-    flattening the RHS rewrites `g` to `f`, the reflexivity check succeeds,
-    and we go on to glory.
-
 Note [Decomposing TyConApps]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
@@ -925,16 +851,10 @@ Suppose we're in this situation:
 where
   newtype Id a = Id a
 
-Further, suppose flattening `a` doesn't do anything. Then, we'll flatten the
-RHS of c1 and have a new [W] c3 : a ~R Id a. If we just blindly proceed, we'll
-fail in canEqTyVar2 with an occurs-check. What we really need to do is to
-unwrap the `Id a` in the RHS. This is exactly analogous to the requirement for
-no top-level type families on the RHS of a nominal equality. The only
-annoyance is that the flattener doesn't do this work for us when flattening
-the RHS, so we have to catch this case here and then go back to the beginning
-of can_eq_nc. We know that this can't loop forever because we require that
-flattening the RHS actually made progress. (If it didn't, then we really
-*should* fail with an occurs-check!)
+We want to make sure canEqTyVar sees [W] a ~R a, after b is flattened
+and the Id newtype is unwrapped. This is assured by requiring only flat
+types in canEqTyVar *and* having the newtype-unwrapping check above
+the tyvar check in can_eq_nc.
 
 -}
 
@@ -962,72 +882,42 @@ canCFunEqCan ev fn tys fsk
 
 ---------------------
 canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
-           -> TcTyVar
-           -> TcType -> TcType
+           -> TcTyVar             -- already flat
+           -> TcType              -- already flat
            -> TcS (StopOrContinue Ct)
 -- A TyVar on LHS, but so far un-zonked
-canEqTyVar ev eq_rel swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
-  = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
-       ; mb_yes <- flattenTyVar ev tv1
-       ; case mb_yes of
-         { Right (ty1, co1) -> -- co1 :: ty1 ~ tv1
-             do { traceTcS "canEqTyVar2"
-                           (vcat [ ppr tv1, ppr ty2, ppr swapped
-                                 , ppr ty1 , ppUnless (isDerived ev) (ppr co1)])
-                ; rewriteEqEvidence ev eq_rel swapped ty1 ps_ty2
-                                    co1 (mkTcReflCo (eqRelRole eq_rel) ps_ty2)
-                  `andWhenContinue` \ new_ev ->
-                  can_eq_nc new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
-
-         ; Left tv1' ->
-    do { -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
+canEqTyVar ev eq_rel swapped tv1 ps_ty2              -- ev :: tv ~ s2
+  = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
+         -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
          -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
          -- Flatten the RHS less vigorously, to avoid gratuitous flattening
          -- True <=> xi2 should not itself be a type-function application
-       ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2 -- co2 :: xi2 ~ ps_ty2
-                      -- Use ps_ty2 to preserve type synonyms if poss
-       ; traceTcS "canEqTyVar flat LHS"
-           (vcat [ ppr tv1, ppr tv1', ppr ty2, ppr swapped, ppr xi2 ])
        ; dflags <- getDynFlags
-       ; case eq_rel of
-      -- See Note [No top-level newtypes on RHS of representational equalities]
-           ReprEq
-             | Just (tc2, _) <- tcSplitTyConApp_maybe xi2
-             , isNewTyCon tc2
-             , not (ps_ty2 `eqType` xi2)
-             -> do { let xi1  = mkTyVarTy tv1'
-                         role = eqRelRole eq_rel
-                   ; traceTcS "canEqTyVar exposed newtype"
-                       (vcat [ ppr tv1', ppr ps_ty2, ppr xi2, ppr tc2 ])
-                   ; rewriteEqEvidence ev eq_rel swapped xi1 xi2
-                                       (mkTcReflCo role xi1) co2
-                     `andWhenContinue` \ new_ev ->
-                     can_eq_nc new_ev eq_rel xi1 xi1 xi2 xi2 }
-           _ -> canEqTyVar2 dflags ev eq_rel swapped tv1' xi2 co2 } } }
+       ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
 
 canEqTyVar2 :: DynFlags
-            -> CtEvidence   -- olhs ~ orhs (or, if swapped, orhs ~ olhs)
+            -> CtEvidence   -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
             -> EqRel
             -> SwapFlag
-            -> TcTyVar      -- olhs
-            -> TcType       -- nrhs
-            -> TcCoercion   -- nrhs ~ orhs
+            -> TcTyVar      -- lhs, flat
+            -> TcType       -- rhs, flat
             -> TcS (StopOrContinue Ct)
 -- LHS is an inert type variable,
 -- and RHS is fully rewritten, but with type synonyms
 -- preserved as much as possible
 
-canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 co2
+canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
   | Just tv2 <- getTyVar_maybe xi2
-  = canEqTyVarTyVar ev eq_rel swapped tv1 tv2 co2
+  = canEqTyVarTyVar ev eq_rel swapped tv1 tv2
 
   | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2  -- No occurs check
+     -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
+     -- to establish the invariant that a does not appear in the
+     -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
+     -- see Note [Occurs check expansion] in TcType
   = do { let k1 = tyVarKind tv1
              k2 = typeKind xi2'
-       ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 co2
-                -- Ensure that the new goal has enough type synonyms
-                -- expanded by the occurCheckExpand; hence using xi2' here
-                -- See Note [occurCheckExpand]
+       ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 (mkTcReflCo role xi2')
          `andWhenContinue` \ new_ev ->
          if k2 `isSubKind` k1
          then   -- Establish CTyEqCan kind invariant
@@ -1042,7 +932,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 co2
   = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
     `andWhenContinue` \ new_ev ->
     case eq_rel of
-      NomEq  -> do { emitInsoluble (mkNonCanonical new_ev)
+      NomEq  -> do { emitInsoluble (mkNonCanonical ev)
               -- If we have a ~ [a], it is not canonical, and in particular
               -- we don't want to rewrite existing inerts with it, otherwise
               -- we'd risk divergence in the constraint solver
@@ -1058,26 +948,21 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 co2
                               (ppr xi1 $$ ppr xi2)
                    ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
   where
-    xi1 = mkTyVarTy tv1
-    co1 = mkTcReflCo (eqRelRole eq_rel) xi1
-
-
+    role = eqRelRole eq_rel
+    xi1  = mkTyVarTy tv1
+    co1  = mkTcReflCo role xi1
+    co2  = mkTcReflCo role xi2
 
-canEqTyVarTyVar :: CtEvidence           -- tv1 ~ orhs (or orhs ~ tv1, if swapped)
+canEqTyVarTyVar :: CtEvidence           -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
                 -> EqRel
                 -> SwapFlag
-                -> TcTyVar -> TcTyVar   -- tv2, tv2
-                -> TcCoercion           -- tv2 ~ orhs
+                -> TcTyVar -> TcTyVar   -- tv1, tv2
                 -> TcS (StopOrContinue Ct)
--- Both LHS and RHS rewrote to a type variable,
--- If swapped = NotSwapped, then
---     rw_orhs = tv1, rw_olhs = orhs
---     rw_nlhs = tv2, rw_nrhs = xi1
+-- Both LHS and RHS rewrote to a type variable
 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
-canEqTyVarTyVar ev eq_rel swapped tv1 tv2 co2
+canEqTyVarTyVar ev eq_rel swapped tv1 tv2
   | tv1 == tv2
-  = do { ASSERT( tcCoercionRole co2 == eqRelRole eq_rel )
-         setEvBindIfWanted ev (EvCoercion (maybeSym swapped co2))
+  = do { setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1)
        ; stopWith ev "Equal tyvars" }
 
   | incompat_kind   = incompat
@@ -1087,11 +972,13 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 co2
   | k1_sub_k2       = do_swap   -- Note [Kind orientation for CTyEqCan]
   | otherwise       = no_swap   -- k2_sub_k1
   where
+    role = eqRelRole eq_rel
     xi1 = mkTyVarTy tv1
+    co1 = mkTcReflCo role xi1
     xi2 = mkTyVarTy tv2
+    co2 = mkTcReflCo role xi2
     k1  = tyVarKind tv1
     k2  = tyVarKind tv2
-    co1 = mkTcReflCo (eqRelRole eq_rel) xi1
     k1_sub_k2     = k1 `isSubKind` k2
     k2_sub_k1     = k2 `isSubKind` k1
     same_kind     = k1_sub_k2 && k2_sub_k1
@@ -1101,32 +988,29 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 co2
     do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
 
     canon_eq swapped tv1 xi1 xi2 co1 co2
-        -- ev  : tv1 ~ orhs  (not swapped) or   orhs ~ tv1   (swapped)
-        -- co1 : xi1 ~ tv1
-        -- co2 : xi2 ~ tv2
-      = do { mb <- rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
-           ; let mk_ct ev' = CTyEqCan { cc_ev = ev', cc_tyvar = tv1
-                                      , cc_rhs = xi2 , cc_eq_rel = eq_rel }
-           ; return (fmap mk_ct mb) }
+        -- ev  : tv1 ~ rhs  (not swapped) or   rhs ~ tv1   (swapped)
+      = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2
+        `andWhenContinue` \ new_ev ->
+        continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
+                               , cc_rhs = xi2, cc_eq_rel = eq_rel })
 
     -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten
     do_fmv swapped tv1 xi1 xi2 co1 co2
       | same_kind
       = canon_eq swapped tv1 xi1 xi2 co1 co2
       | otherwise  -- Presumably tv1 `subKind` tv2, which is the wrong way round
-      = ASSERT2( k1_sub_k2, ppr tv1 $$ ppr tv2 )
+      = ASSERT2( tyVarKind tv1 `isSubKind` typeKind xi2,
+                 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
+                 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
         ASSERT2( isWanted ev, ppr ev )  -- Only wanteds have flatten meta-vars
         do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
            ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
                                         (mkTcEqPredRole (eqRelRole eq_rel)
                                                         tv_ty xi2)
            ; emitWorkNC [new_ev]
-           ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev `mkTcTransCo` co2) }
+           ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
 
-    incompat
-      = rewriteEqEvidence ev eq_rel swapped xi1 xi2 (mkTcNomReflCo xi1) co2
-        `andWhenContinue` \ ev' ->
-        incompatibleKind ev' xi1 k1 xi2 k2
+    incompat = incompatibleKind ev xi1 k1 xi2 k2
 
     swap_over
       -- If tv1 is touchable, swap only if tv2 is also
@@ -1333,43 +1217,6 @@ 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_ty1, ps_ty2 argument passed to canEqTyVar.
 
-
-Note [occurCheckExpand]
-~~~~~~~~~~~~~~~~~~~~~~~
-There is a subtle point with type synonyms and the occurs check that
-takes place for equality constraints of the form tv ~ xi.  As an
-example, suppose we have
-
-  type F a = Int
-
-and we come across the equality constraint
-
-  a ~ F a
-
-This should not actually fail the occurs check, since expanding out
-the type synonym results in the legitimate equality constraint a ~
-Int.  We must actually do this expansion, because unifying a with F a
-will lead the type checker into infinite loops later.  Put another
-way, canonical equality constraints should never *syntactically*
-contain the LHS variable in the RHS type.  However, we don't always
-need to expand type synonyms when doing an occurs check; for example,
-the constraint
-
-  a ~ F b
-
-is obviously fine no matter what F expands to. And in this case we
-would rather unify a with F b (rather than F b's expansion) in order
-to get better error messages later.
-
-So, when doing an occurs check with a type synonym application on the
-RHS, we use some heuristics to find an expansion of the RHS which does
-not contain the variable from the LHS.  In particular, given
-
-  a ~ F t1 ... tn
-
-we first try expanding each of the ti to types which no longer contain
-a.  If this turns out to be impossible, we next try expanding F
-itself, and so on.  See Note [Occurs check expansion] in TcType
 -}
 
 {-
@@ -1528,17 +1375,17 @@ rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swap
 --
 -- It's all a form of rewwriteEvidence, specialised for equalities
 rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
+  | NotSwapped <- swapped
+  , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
+  , isTcReflCo rhs_co
+  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
+
   | CtDerived {} <- old_ev
   = do { mb <- newDerived loc' new_pred
        ; case mb of
            Just new_ev -> continueWith new_ev
            Nothing     -> stopWith old_ev "Cached derived" }
 
-  | NotSwapped <- swapped
-  , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
-  , isTcReflCo rhs_co
-  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
-
   | CtGiven { ctev_evtm = old_tm } <- old_ev
   = do { let new_tm = EvCoercion (lhs_co
                                   `mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
@@ -1564,9 +1411,8 @@ rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
 
       -- equality is like a type class. Bumping the depth is necessary because
       -- of recursive newtypes, where "reducing" a newtype can actually make
-      -- it bigger. See Note [Eager reflexivity check] in TcCanonical before
-      -- considering changing this behavior.
-    loc'     = bumpCtLocDepth CountConstraints (ctEvLoc old_ev)
+      -- it bigger. See Note [Newtypes can blow the stack].
+    loc'     = bumpCtLocDepth (ctEvLoc old_ev)
 
 {- Note [unifyWanted and unifyDerived]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 7a61e19892..6b37e80a3d 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1678,21 +1678,23 @@ are created by in RtClosureInspect.zonkRTTIType.
 ************************************************************************
 -}
 
-solverDepthErrorTcS :: SubGoalCounter -> CtEvidence -> TcM a
-solverDepthErrorTcS cnt ev
+solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
+solverDepthErrorTcS loc ty
   = setCtLoc loc $
-    do { pred <- zonkTcType (ctEvPred ev)
+    do { ty <- zonkTcType ty
        ; env0 <- tcInitTidyEnv
-       ; let tidy_env  = tidyFreeTyVars env0 (tyVarsOfType pred)
-             tidy_pred = tidyType tidy_env pred
-       ; failWithTcM (tidy_env, hang (msg cnt) 2 (ppr tidy_pred)) }
+       ; let tidy_env     = tidyFreeTyVars env0 (tyVarsOfType ty)
+             tidy_ty      = tidyType tidy_env ty
+             msg
+               = vcat [ text "Reduction stack overflow; size =" <+> ppr depth
+                      , hang (text "When simplifying the following type:")
+                           2 (ppr tidy_ty)
+                      , note ]
+       ; failWithTcM (tidy_env, msg) }
   where
-    loc   = ctEvLoc ev
     depth = ctLocDepth loc
-    value = subGoalCounterValue cnt depth
-    msg CountConstraints =
-        vcat [ ptext (sLit "Context reduction stack overflow; size =") <+> int value
-             , ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
-    msg CountTyFunApps =
-        vcat [ ptext (sLit "Type function application stack overflow; size =") <+> int value
-             , ptext (sLit "Use -ftype-function-depth=N to increase stack size to N") ]
+    note = vcat
+      [ text "Use -freduction-depth=0 to disable this check"
+      , text "(any upper bound you could choose might fail unpredictably with"
+      , text " minor updates to GHC, so disabling the check is recommended if"
+      , text " you're sure that type checking should terminate)" ]
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index bec2415bb1..9e0b40b7c5 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -1070,7 +1070,7 @@ instance Outputable EvBind where
      = sep [ pp_gw <+> ppr v
            , nest 2 $ equals <+> ppr e ]
      where
-       pp_gw = brackets (if is_given then ptext (sLit "[G]") else ptext (sLit "[W]"))
+       pp_gw = brackets (if is_given then char 'G' else char 'W')
    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
 
 instance Outputable EvTerm where
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index b8ab372ad1..67b60c573f 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -1212,7 +1212,7 @@ tcTagToEnum loc fun_name arg res_ty
         ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar fun))
               rep_ty = mkTyConApp rep_tc rep_args
 
-        ; return (mkHsWrapCoR (mkTcSymCo coi) $ HsApp fun' arg') }
+        ; return (mkHsWrapCoR (mkTcSymCo $ TcCoercion coi) $ HsApp fun' arg') }
                   -- coi is a Representational coercion
   where
     doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature")
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 9e8a392ba6..cd7c3d6c81 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1,8 +1,8 @@
 {-# LANGUAGE CPP #-}
 
 module TcFlatten(
-   FlattenEnv(..), FlattenMode(..), mkFlattenEnv,
-   flatten, flattenManyNom, flattenFamApp, flattenTyVar,
+   FlattenMode(..),
+   flatten, flattenManyNom,
 
    unflatten,
 
@@ -30,10 +30,14 @@ import DynFlags( DynFlags )
 import Util
 import Bag
 import FastString
-import Control.Monad( when, liftM )
+import Control.Monad
 import MonadUtils ( zipWithAndUnzipM )
 import GHC.Exts ( inline )
 
+#if __GLASGOW_HASKELL__ < 709
+import Control.Applicative ( Applicative(..), (<$>) )
+#endif
+
 {-
 Note [The flattening story]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -493,22 +497,24 @@ wanteds, we will
 
 ************************************************************************
 *                                                                      *
-*                     FlattenEnv
-*             The flattening environment 
+*                FlattenEnv & FlatM
+*             The flattening environment & monad
 *                                                                      *
 ************************************************************************
 
 -}
 
+type FlatWorkListRef = TcRef [Ct]  -- See Note [The flattening work list]
+
 data FlattenEnv
   = FE { fe_mode    :: FlattenMode
-       , fe_loc     :: CtLoc
+       , fe_loc     :: CtLoc              -- See Note [Flattener CtLoc]
        , fe_flavour :: CtFlavour
-       , fe_eq_rel  :: EqRel }   -- See Note [Flattener EqRels]
+       , fe_eq_rel  :: EqRel              -- See Note [Flattener EqRels]
+       , fe_work    :: FlatWorkListRef }  -- See Note [The flattening work list]
 
 data FlattenMode  -- Postcondition for all three: inert wrt the type substitution
   = FM_FlattenAll          -- Postcondition: function-free
-
   | FM_SubstOnly           -- See Note [Flattening under a forall]
 
 --  | FM_Avoid TcTyVar Bool  -- See Note [Lazy flattening]
@@ -518,41 +524,209 @@ data FlattenMode  -- Postcondition for all three: inert wrt the type substitutio
 --                           --  * If flat_top is True, top level is not a function application
 --                           --   (but under type constructors is ok e.g. [F a])
 
-mkFlattenEnv :: FlattenMode -> CtEvidence -> FlattenEnv
-mkFlattenEnv fm ctev = FE { fe_mode    = fm
-                          , fe_loc     = ctEvLoc ctev
-                          , fe_flavour = ctEvFlavour ctev
-                          , fe_eq_rel  = ctEvEqRel ctev }
-
-feRole :: FlattenEnv -> Role
-feRole = eqRelRole . fe_eq_rel
-
--- | Change the 'EqRel' in a 'FlattenEnv'. Avoids allocating a
--- new 'FlattenEnv' where possible.
-setFEEqRel :: FlattenEnv -> EqRel -> FlattenEnv
-setFEEqRel fmode@(FE { fe_eq_rel = old_eq_rel }) new_eq_rel
-  | old_eq_rel == new_eq_rel = fmode
-  | otherwise                = fmode { fe_eq_rel = new_eq_rel }
-
--- | Change the 'FlattenMode' in a 'FlattenEnv'. Avoids allocating
--- a new 'FlattenEnv' where possible.
-setFEMode :: FlattenEnv -> FlattenMode -> FlattenEnv
-setFEMode fmode@(FE { fe_mode = old_mode }) new_mode
-  | old_mode `eq` new_mode = fmode
-  | otherwise              = fmode { fe_mode = new_mode }
+mkFlattenEnv :: FlattenMode -> CtEvidence -> FlatWorkListRef -> FlattenEnv
+mkFlattenEnv fm ctev ref = FE { fe_mode    = fm
+                              , fe_loc     = ctEvLoc ctev
+                              , fe_flavour = ctEvFlavour ctev
+                              , fe_eq_rel  = ctEvEqRel ctev
+                              , fe_work    = ref }
+
+-- | The 'FlatM' monad is a wrapper around 'TcS' with the following
+-- extra capabilities: (1) it offers access to a 'FlattenEnv';
+-- and (2) it maintains the flattening worklist.
+-- See Note [The flattening work list].
+newtype FlatM a
+  = FlatM { runFlatM :: FlattenEnv -> TcS a }
+
+instance Monad FlatM where
+  return x = FlatM $ const (return x)
+  m >>= k  = FlatM $ \env ->
+             do { a  <- runFlatM m env
+                ; runFlatM (k a) env }
+
+instance Functor FlatM where
+  fmap = liftM
+
+instance Applicative FlatM where
+  pure  = return
+  (<*>) = ap
+
+liftTcS :: TcS a -> FlatM a
+liftTcS thing_inside
+  = FlatM $ const thing_inside 
+
+emitFlatWork :: Ct -> FlatM ()
+-- See Note [The flattening work list]
+emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :)
+
+runFlatten :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
+-- Run thing_inside (which does flattening), and put all
+-- the work it generates onto the main work list
+-- See Note [The flattening work list]
+-- NB: The returned evidence is always the same as the original, but with
+-- perhaps a new CtLoc
+runFlatten mode ev thing_inside
+  = do { flat_ref <- newTcRef []
+       ; let fmode = mkFlattenEnv mode ev flat_ref
+       ; res <- runFlatM thing_inside fmode
+       ; new_flats <- readTcRef flat_ref
+       ; updWorkListTcS (add_flats new_flats)
+       ; return res }
+  where
+    add_flats new_flats wl
+      = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
+
+    add_funeqs []     wl = wl
+    add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
+      -- add_funeqs fs ws = reverse fs ++ ws
+      -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
+      --        = [f3,f2,f1,w1,w2,w3,w4]
+
+traceFlat :: String -> SDoc -> FlatM ()
+traceFlat herald doc = liftTcS $ traceTcS herald doc
+
+getFlatEnvField :: (FlattenEnv -> a) -> FlatM a
+getFlatEnvField accessor
+  = FlatM $ \env -> return (accessor env)
+
+getEqRel :: FlatM EqRel
+getEqRel = getFlatEnvField fe_eq_rel
+
+getRole :: FlatM Role
+getRole = eqRelRole <$> getEqRel
+
+getFlavour :: FlatM CtFlavour
+getFlavour = getFlatEnvField fe_flavour
+
+getFlavourRole :: FlatM CtFlavourRole
+getFlavourRole
+  = do { flavour <- getFlavour
+       ; eq_rel <- getEqRel
+       ; return (flavour, eq_rel) }
+
+getMode :: FlatM FlattenMode
+getMode = getFlatEnvField fe_mode
+
+getLoc :: FlatM CtLoc
+getLoc = getFlatEnvField fe_loc
+
+checkStackDepth :: Type -> FlatM ()
+checkStackDepth ty
+  = do { loc <- getLoc
+       ; liftTcS $ checkReductionDepth loc ty }
+
+-- | Change the 'EqRel' in a 'FlatM'.
+setEqRel :: EqRel -> FlatM a -> FlatM a
+setEqRel new_eq_rel thing_inside
+  = FlatM $ \env ->
+    if new_eq_rel == fe_eq_rel env
+    then runFlatM thing_inside env
+    else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
+    
+-- | Change the 'FlattenMode' in a 'FlattenEnv'.
+setMode :: FlattenMode -> FlatM a -> FlatM a
+setMode new_mode thing_inside
+  = FlatM $ \env ->
+    if new_mode `eq` fe_mode env
+    then runFlatM thing_inside env
+    else runFlatM thing_inside (env { fe_mode = new_mode })
   where
     FM_FlattenAll   `eq` FM_FlattenAll   = True
     FM_SubstOnly    `eq` FM_SubstOnly    = True
 --  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
     _               `eq` _               = False
 
+bumpDepth :: FlatM a -> FlatM a
+bumpDepth (FlatM thing_inside)
+  = FlatM $ \env -> do { let env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
+                       ; thing_inside env' }
+
+-- Flatten skolems
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+newFlattenSkolemFlatM :: TcType         -- F xis
+                      -> FlatM (CtEvidence, TcTyVar)    -- [W] x:: F xis ~ fsk
+newFlattenSkolemFlatM ty
+  = do { flavour <- getFlavour
+       ; loc <- getLoc
+       ; liftTcS $ newFlattenSkolem flavour loc ty }
+
 {-
+Note [The flattening work list]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The "flattening work list", held in the fe_work field of FlattenEnv,
+is a list of CFunEqCans generated during flattening.  The key idea
+is this.  Consider flattening (Eq (F (G Int) (H Bool)):
+  * The flattener recursively calls itself on sub-terms before building
+    the main term, so it will encounter the terms in order
+              G Int
+              H Bool
+              F (G Int) (H Bool)
+    flattening to sub-goals
+              w1: G Int ~ fuv0
+              w2: H Bool ~ fuv1
+              w3: F fuv0 fuv1 ~ fuv2
+
+  * Processing w3 first is BAD, because we can't reduce i t,so it'll
+    get put into the inert set, and later kicked out when w1, w2 are
+    solved.  In Trac #9872 this led to inert sets containing hundreds
+    of suspended calls.
+
+  * So we want to process w1, w2 first.
+
+  * So you might think that we should just use a FIFO deque for the work-list,
+    so that putting adding goals in order w1,w2,w3 would mean we processed
+    w1 first.
+
+  * BUT suppose we have 'type instance G Int = H Char'.  Then processing
+    w1 leads to a new goal
+                w4: H Char ~ fuv0
+    We do NOT want to put that on the far end of a deque!  Instead we want
+    to put it at the *front* of the work-list so that we continue to work
+    on it.
+
+So the work-list structure is this:
+
+  * The wl_funeqs (in TcS) is a LIFO stack; we push new goals (such as w4) on
+    top (extendWorkListFunEq), and take new work from the top
+    (selectWorkItem).
+
+  * When flattening, emitFlatWork pushes new flattening goals (like
+    w1,w2,w3) onto the flattening work list, fe_work, another
+    push-down stack.
+
+  * When we finish flattening, we *reverse* the fe_work stack
+    onto the wl_funeqs stack (which brings w1 to the top).
+
+The function runFlatten initialises the fe_work stack, and reverses
+it onto wl_fun_eqs at the end.
+
 Note [Flattener EqRels]
 ~~~~~~~~~~~~~~~~~~~~~~~
 When flattening, we need to know which equality relation -- nominal
 or representation -- we should be respecting. The only difference is
 that we rewrite variables by representational equalities when fe_eq_rel
-is ReprEq.
+is ReprEq, and that we unwrap newtypes when flattening w.r.t.
+representational equality.
+
+Note [Flattener CtLoc]
+~~~~~~~~~~~~~~~~~~~~~~
+The flattener does eager type-family reduction.
+Type families might loop, and we
+don't want GHC to do so. A natural solution is to have a bounded depth
+to these processes. A central difficulty is that such a solution isn't
+quite compositional. For example, say it takes F Int 10 steps to get to Bool.
+How many steps does it take to get from F Int -> F Int to Bool -> Bool?
+10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
+know and hard to track. So, we punt, essentially. We store a CtLoc in
+the FlattenEnv and just update the environment when recurring. In the
+TyConApp case, where there may be multiple type families to flatten,
+we just copy the current CtLoc into each branch. If any branch hits the
+stack limit, then the whole thing fails.
+
+A consequence of this is that setting the stack limits appropriately
+will be essentially impossible. So, the official recommendation if a
+stack limit is hit is to disable the check entirely. Otherwise, there
+will be baffling, unpredictable errors.
 
 Note [Lazy flattening]
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -605,11 +779,10 @@ yields a better error message anyway.)
 *                                                                      *
 ********************************************************************* -}
 
-flatten :: FlattenMode -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
+flatten :: FlattenMode -> CtEvidence -> TcType
+        -> TcS (Xi, TcCoercion)
 flatten mode ev ty
-  = runFlatten (flatten_one fmode ty)
-  where
-    fmode = mkFlattenEnv mode ev
+  = runFlatten mode ev (flatten_one ty)
 
 flattenManyNom :: CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
 -- Externally-callable, hence runFlatten
@@ -618,25 +791,7 @@ flattenManyNom :: CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
 --      ctEvFlavour ev = Nominal
 -- and we want to flatten all at nominal role
 flattenManyNom ev tys
-  = runFlatten (flatten_many_nom fmode tys)
-  where
-    fmode = mkFlattenEnv FM_FlattenAll ev
-
-flattenFamApp :: FlattenMode -> CtEvidence
-              -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
--- Externally callable, hence runFlatten
-flattenFamApp mode ev tc tys
-  = runFlatten (flatten_fam_app fmode tc tys)
-  where
-    fmode = mkFlattenEnv mode ev
-
-flattenTyVar :: CtEvidence -> TcTyVar
-             -> TcS (Either TyVar (TcType, TcCoercion))
-flattenTyVar ev tv
-  = runFlatten (flatten_tyvar fmode tv)
-  where
-    fmode = mkFlattenEnv FM_FlattenAll ev
-
+  = runFlatten FM_FlattenAll ev (flatten_many_nom tys)
 
 {- *********************************************************************
 *                                                                      *
@@ -716,33 +871,32 @@ duplicate the flattener code for the nominal case, and make that case
 faster. This doesn't seem quite worth it, yet.
 -}
 
-flatten_many :: FlattenEnv -> [Role] -> [Type] -> TcS ([Xi], [TcCoercion])
+flatten_many :: [Role] -> [Type] -> FlatM ([Xi], [TcCoercion])
 -- Coercions :: Xi ~ Type, at roles given
 -- Returns True iff (no flattening happened)
 -- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
 --     we merely want (a) Given/Solved/Derived/Wanted info
 --                    (b) the GivenLoc/WantedLoc for when we create new evidence
-flatten_many fmode roles tys
+flatten_many roles tys
 -- See Note [flatten_many performance]
   = inline zipWithAndUnzipM go roles tys
   where
-    go Nominal          ty = flatten_one (setFEEqRel fmode NomEq)  ty
-    go Representational ty = flatten_one (setFEEqRel fmode ReprEq) ty
+    go Nominal          ty = setEqRel NomEq  $ flatten_one ty
+    go Representational ty = setEqRel ReprEq $ flatten_one ty
     go Phantom          ty = -- See Note [Phantoms in the flattener]
                              return (ty, mkTcPhantomCo ty ty)
 
 -- | Like 'flatten_many', but assumes that every role is nominal.
-flatten_many_nom :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion])
-flatten_many_nom _     [] = return ([], [])
+flatten_many_nom :: [Type] -> FlatM ([Xi], [TcCoercion])
+flatten_many_nom [] = return ([], [])
 -- See Note [flatten_many performance]
-flatten_many_nom fmode (ty:tys)
-  = ASSERT( fe_eq_rel fmode == NomEq )
-    do { (xi, co) <- flatten_one fmode ty
-       ; (xis, cos) <- flatten_many_nom fmode tys
+flatten_many_nom (ty:tys)
+  = do { (xi, co) <- flatten_one ty
+       ; (xis, cos) <- flatten_many_nom tys
        ; return (xi:xis, co:cos) }
 
 ------------------
-flatten_one :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion)
+flatten_one :: TcType -> FlatM (Xi, TcCoercion)
 -- Flatten a type to get rid of type function applications, returning
 -- the new type-function-free type, and a collection of new equality
 -- constraints.  See Note [Flattening] for more detail.
@@ -750,25 +904,29 @@ flatten_one :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion)
 -- Postcondition: Coercion :: Xi ~ TcType
 -- The role on the result coercion matches the EqRel in the FlattenEnv
 
-flatten_one fmode xi@(LitTy {}) = return (xi, mkTcReflCo (feRole fmode) xi)
+flatten_one xi@(LitTy {})
+  = do { role <- getRole
+       ; return (xi, mkTcReflCo role xi) }
 
-flatten_one fmode (TyVarTy tv)
-  = do { mb_yes <- flatten_tyvar fmode tv
+flatten_one (TyVarTy tv)
+  = do { mb_yes <- flatten_tyvar tv
+       ; role <- getRole
        ; case mb_yes of
            Left tv' -> -- Done
-                       do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
-                          ; return (ty', mkTcReflCo (feRole fmode) ty') }
+                       do { traceFlat "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
+                          ; return (ty', mkTcReflCo role ty') }
                     where
                        ty' = mkTyVarTy tv'
 
            Right (ty1, co1)  -- Recurse
-                    -> do { (ty2, co2) <- flatten_one fmode ty1
-                          ; traceTcS "flattenTyVar2" (ppr tv $$ ppr ty2)
+                    -> do { (ty2, co2) <- flatten_one ty1
+                          ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2 $$ ppr co1)
                           ; return (ty2, co2 `mkTcTransCo` co1) } }
 
-flatten_one fmode (AppTy ty1 ty2)
-  = do { (xi1,co1) <- flatten_one fmode ty1
-       ; case (fe_eq_rel fmode, nextRole xi1) of
+flatten_one (AppTy ty1 ty2)
+  = do { (xi1,co1) <- flatten_one ty1
+       ; eq_rel <- getEqRel
+       ; case (eq_rel, nextRole xi1) of
            (NomEq,  _)                -> flatten_rhs xi1 co1 NomEq
            (ReprEq, Nominal)          -> flatten_rhs xi1 co1 NomEq
            (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
@@ -776,40 +934,41 @@ flatten_one fmode (AppTy ty1 ty2)
              return (mkAppTy xi1 ty2, co1 `mkTcAppCo` mkTcNomReflCo ty2) }
   where
     flatten_rhs xi1 co1 eq_rel2
-      = do { (xi2,co2) <- flatten_one (setFEEqRel fmode eq_rel2) ty2
-           ; traceTcS "flatten/appty"
-                      (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$
-                       ppr co1 $$ ppr xi2 $$ ppr co2)
-           ; let role1 = feRole fmode
-                 role2 = eqRelRole eq_rel2
+      = do { (xi2,co2) <- setEqRel eq_rel2 $ flatten_one ty2
+           ; traceFlat "flatten/appty"
+                       (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$
+                        ppr co1 $$ ppr xi2 $$ ppr co2)
+           ; role1 <- getRole
+           ; let role2 = eqRelRole eq_rel2
            ; return ( mkAppTy xi1 xi2
                     , mkTcTransAppCo role1 co1 xi1 ty1
                                      role2 co2 xi2 ty2
                                      role1 ) }  -- output should match fmode
 
-flatten_one fmode (FunTy ty1 ty2)
-  = do { (xi1,co1) <- flatten_one fmode ty1
-       ; (xi2,co2) <- flatten_one fmode ty2
-       ; return (mkFunTy xi1 xi2, mkTcFunCo (feRole fmode) co1 co2) }
+flatten_one (FunTy ty1 ty2)
+  = do { (xi1,co1) <- flatten_one ty1
+       ; (xi2,co2) <- flatten_one ty2
+       ; role <- getRole
+       ; return (mkFunTy xi1 xi2, mkTcFunCo role co1 co2) }
 
-flatten_one fmode (TyConApp tc tys)
+flatten_one (TyConApp tc tys)
 
   -- Expand type synonyms that mention type families
   -- on the RHS; see Note [Flattening synonyms]
   | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
   , let expanded_ty = mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys'
-  = case fe_mode fmode of
-      FM_FlattenAll | anyNameEnv isTypeFamilyTyCon (tyConsOfType rhs)
-                   -> flatten_one fmode expanded_ty
-                    | otherwise
-                   -> flattenTyConApp fmode tc tys
-      _ -> flattenTyConApp fmode tc tys
+  = do { mode <- getMode
+       ; let used_tcs = tyConsOfType rhs
+       ; case mode of
+           FM_FlattenAll | anyNameEnv isTypeFamilyTyCon used_tcs
+                         -> flatten_one expanded_ty
+           _             -> flatten_ty_con_app tc tys }
 
   -- Otherwise, it's a type function application, and we have to
   -- flatten it away as well, and generate a new given equality constraint
   -- between the application and a newly generated flattening skolem variable.
   | isTypeFamilyTyCon tc
-  = flatten_fam_app fmode tc tys
+  = flatten_fam_app tc tys
 
   -- For * a normal data type application
   --     * data family application
@@ -820,25 +979,25 @@ flatten_one fmode (TyConApp tc tys)
 --                   FE { fe_mode = FM_Avoid tv _ }
 --                     -> fmode { fe_mode = FM_Avoid tv False }
 --                   _ -> fmode
-  = flattenTyConApp fmode tc tys
+  = flatten_ty_con_app tc tys
 
-flatten_one fmode ty@(ForAllTy {})
+flatten_one ty@(ForAllTy {})
 -- We allow for-alls when, but only when, no type function
 -- applications inside the forall involve the bound type variables.
   = do { let (tvs, rho) = splitForAllTys ty
-       ; (rho', co) <- flatten_one (setFEMode fmode FM_SubstOnly) rho
+       ; (rho', co) <- setMode FM_SubstOnly $ flatten_one rho
                          -- Substitute only under a forall
                          -- See Note [Flattening under a forall]
        ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
 
-flattenTyConApp :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
-flattenTyConApp fmode tc tys
-  = do { (xis, cos) <- case fe_eq_rel fmode of
-                         NomEq  -> flatten_many_nom fmode tys
-                         ReprEq -> flatten_many fmode (tyConRolesX role tc) tys
+flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, TcCoercion)
+flatten_ty_con_app tc tys
+  = do { eq_rel <- getEqRel
+       ; let role = eqRelRole eq_rel
+       ; (xis, cos) <- case eq_rel of
+                         NomEq  -> flatten_many_nom tys
+                         ReprEq -> flatten_many (tyConRolesX role tc) tys
        ; return (mkTyConApp tc xis, mkTcTyConAppCo role tc cos) }
-  where
-    role = feRole fmode
 
 {-
 Note [Flattening synonyms]
@@ -884,35 +1043,41 @@ and we have not begun to think about how to make that work!
 -}
 
 flatten_fam_app, flatten_exact_fam_app, flatten_exact_fam_app_fully
-  :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
+  :: TyCon -> [TcType] -> FlatM (Xi, TcCoercion)
   --   flatten_fam_app            can be over-saturated
   --   flatten_exact_fam_app       is exactly saturated
   --   flatten_exact_fam_app_fully lifts out the application to top level
   -- Postcondition: Coercion :: Xi ~ F tys
-flatten_fam_app fmode tc tys  -- Can be over-saturated
+flatten_fam_app tc tys  -- Can be over-saturated
     = ASSERT( tyConArity tc <= length tys )  -- Type functions are saturated
                  -- The type function might be *over* saturated
                  -- in which case the remaining arguments should
                  -- be dealt with by AppTys
       do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
-         ; (xi1, co1) <- flatten_exact_fam_app fmode tc tys1
+         ; (xi1, co1) <- flatten_exact_fam_app tc tys1
                -- co1 :: xi1 ~ F tys1
 
                -- all Nominal roles b/c the tycon is oversaturated
-         ; (xis_rest, cos_rest) <- flatten_many fmode (repeat Nominal) tys_rest
+         ; (xis_rest, cos_rest) <- flatten_many (repeat Nominal) tys_rest
                -- cos_res :: xis_rest ~ tys_rest
          ; return ( mkAppTys xi1 xis_rest   -- NB mkAppTys: rhs_xi might not be a type variable
                                             --    cf Trac #5655
                   , mkTcAppCos co1 cos_rest -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
                   ) }
 
-flatten_exact_fam_app fmode tc tys
-  = case fe_mode fmode of
-       FM_FlattenAll -> flatten_exact_fam_app_fully fmode tc tys
+flatten_exact_fam_app tc tys
+  = do { mode <- getMode
+       ; role <- getRole
+       ; case mode of
+           FM_FlattenAll -> flatten_exact_fam_app_fully tc tys
 
-       FM_SubstOnly -> do { (xis, cos) <- flatten_many fmode roles tys
-                          ; return ( mkTyConApp tc xis
-                                   , mkTcTyConAppCo (feRole fmode) tc cos ) }
+           FM_SubstOnly -> do { (xis, cos) <- flatten_many roles tys
+                              ; return ( mkTyConApp tc xis
+                                       , mkTcTyConAppCo role tc cos ) }
+             where
+               -- These are always going to be Nominal for now,
+               -- but not if #8177 is implemented
+               roles = tyConRolesX role tc }
 
 --       FM_Avoid tv flat_top ->
 --         do { (xis, cos) <- flatten_many fmode roles tys
@@ -920,32 +1085,31 @@ flatten_exact_fam_app fmode tc tys
 --              then flatten_exact_fam_app_fully fmode tc tys
 --              else return ( mkTyConApp tc xis
 --                          , mkTcTyConAppCo (feRole fmode) tc cos ) }
-  where
-    -- These are always going to be Nominal for now,
-    -- but not if #8177 is implemented
-    roles = tyConRolesX (feRole fmode) tc
 
-flatten_exact_fam_app_fully fmode tc tys
+flatten_exact_fam_app_fully tc tys
   -- See Note [Reduce type family applications eagerly]
   = try_to_reduce tc tys False id $
     do { -- First, flatten the arguments
-         (xis, cos) <- flatten_many_nom (setFEEqRel fmode NomEq) tys
-       ; let ret_co = mkTcTyConAppCo (feRole fmode) tc cos
+         (xis, cos) <- setEqRel NomEq $ flatten_many_nom tys
+       ; eq_rel <- getEqRel
+       ; let role   = eqRelRole eq_rel
+             ret_co = mkTcTyConAppCo role tc cos
               -- ret_co :: F xis ~ F tys
 
         -- Now, look in the cache
-       ; mb_ct <- lookupFlatCache tc xis
+       ; mb_ct <- liftTcS $ lookupFlatCache tc xis
+       ; flavour_role <- getFlavourRole
        ; case mb_ct of
            Just (co, rhs_ty, flav)  -- co :: F xis ~ fsk
-             | (flav, NomEq) `canRewriteOrSameFR` (feFlavourRole fmode)
+             | (flav, NomEq) `canRewriteOrSameFR` flavour_role
              ->  -- Usable hit in the flat-cache
                  -- We certainly *can* use a Wanted for a Wanted
-                do { traceTcS "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty $$ ppr co)
-                   ; (fsk_xi, fsk_co) <- flatten_one fmode rhs_ty
+                do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty $$ ppr co)
+                   ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
                           -- The fsk may already have been unified, so flatten it
                           -- fsk_co :: fsk_xi ~ fsk
                    ; return (fsk_xi, fsk_co `mkTcTransCo`
-                                     maybeTcSubCo (fe_eq_rel fmode)
+                                     maybeTcSubCo eq_rel
                                                   (mkTcSymCo co) `mkTcTransCo`
                                      ret_co) }
                                     -- :: fsk_xi ~ F xis
@@ -954,12 +1118,10 @@ flatten_exact_fam_app_fully fmode tc tys
            -- See Note [Reduce type family applications eagerly]
            _ -> try_to_reduce tc xis True (`mkTcTransCo` ret_co) $
                 do { let fam_ty = mkTyConApp tc xis
-                   ; (ev, fsk) <- newFlattenSkolem (fe_flavour fmode)
-                                                   (fe_loc fmode)
-                                                   fam_ty
+                   ; (ev, fsk) <- newFlattenSkolemFlatM fam_ty
                    ; let fsk_ty = mkTyVarTy fsk
                          co     = ctEvCoercion ev
-                   ; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev)
+                   ; liftTcS $ extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev)
 
                    -- The new constraint (F xis ~ fsk) is not necessarily inert
                    -- (e.g. the LHS may be a redex) so we must put it in the work list
@@ -969,8 +1131,8 @@ flatten_exact_fam_app_fully fmode tc tys
                                         , cc_fsk    = fsk }
                    ; emitFlatWork ct
 
-                   ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
-                   ; return (fsk_ty, maybeTcSubCo (fe_eq_rel fmode)
+                   ; traceFlat "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
+                   ; return (fsk_ty, maybeTcSubCo eq_rel
                                                   (mkTcSymCo co)
                                      `mkTcTransCo` ret_co) }
         }
@@ -981,18 +1143,21 @@ flatten_exact_fam_app_fully fmode tc tys
                   -> Bool    -- add to the flat cache?
                   -> (   TcCoercion     -- :: xi ~ F args
                       -> TcCoercion )   -- what to return from outer function
-                  -> TcS (Xi, TcCoercion)  -- continuation upon failure
-                  -> TcS (Xi, TcCoercion)
+                  -> FlatM (Xi, TcCoercion)  -- continuation upon failure
+                  -> FlatM (Xi, TcCoercion)
     try_to_reduce tc tys cache update_co k
-      = do { mb_match <- matchFam tc tys
+      = do { checkStackDepth (mkTyConApp tc tys)
+           ; mb_match <- liftTcS $ matchFam tc tys
            ; case mb_match of
                Just (norm_co, norm_ty)
-                 -> do { traceTcS "Eager T.F. reduction success" $
+                 -> do { traceFlat "Eager T.F. reduction success" $
                          vcat [ppr tc, ppr tys, ppr norm_ty, ppr cache]
-                       ; (xi, final_co) <- flatten_one fmode norm_ty
+                       ; (xi, final_co) <- bumpDepth $ flatten_one norm_ty
                        ; let co = norm_co `mkTcTransCo` mkTcSymCo final_co
+                       ; flavour <- getFlavour
                        ; when cache $
-                         extendFlatCache tc tys (co, xi, fe_flavour fmode)
+                         liftTcS $
+                         extendFlatCache tc tys (co, xi, flavour)
                        ; return (xi, update_co $ mkTcSymCo co) }
                Nothing -> k }
 
@@ -1260,8 +1425,8 @@ subsitution means that the proof in Note [The inert equalities] may need
 to be revisited, but we don't think that the end conclusion is wrong.
 -}
 
-flatten_tyvar :: FlattenEnv -> TcTyVar
-              -> TcS (Either TyVar (TcType, TcCoercion))
+flatten_tyvar :: TcTyVar
+              -> FlatM (Either TyVar (TcType, TcCoercion))
 -- "Flattening" a type variable means to apply the substitution to it
 -- Specifically, look up the tyvar in
 --   * the internal MetaTyVar box
@@ -1269,29 +1434,32 @@ flatten_tyvar :: FlattenEnv -> TcTyVar
 -- Return (Left tv')      if it is not found, tv' has a properly zonked kind
 --        (Right (ty, co) if found, with co :: ty ~ tv;
 
-flatten_tyvar fmode tv
+flatten_tyvar tv
   | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
-  = Left `liftM` flattenTyVarFinal fmode tv
+  = Left `liftM` flattenTyVarFinal tv
           -- So ty contains refernces to the non-TcTyVar a
 
   | otherwise
-  = do { mb_ty <- isFilledMetaTyVar_maybe tv
+  = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
+       ; role <- getRole
        ; case mb_ty of {
-           Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
-                         ; return (Right (ty, mkTcReflCo (feRole fmode) ty)) } ;
+           Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
+                         ; return (Right (ty, mkTcReflCo role ty)) } ;
            Nothing ->
 
     -- Try in the inert equalities
     -- See Definition [Applying a generalised substitution]
-    do { ieqs <- getInertEqs
+    do { ieqs <- liftTcS $ getInertEqs
+       ; flavour_role <- getFlavourRole
+       ; eq_rel <- getEqRel
        ; case lookupVarEnv ieqs tv of
            Just (ct:_)   -- If the first doesn't work,
                          -- the subsequent ones won't either
              | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
-             , ctEvFlavourRole ctev `eqCanRewriteFR` feFlavourRole fmode
-             ->  do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
+             , ctEvFlavourRole ctev `eqCanRewriteFR` flavour_role
+             ->  do { traceFlat "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
                     ; let rewrite_co1 = mkTcSymCo (ctEvCoercion ctev)
-                          rewrite_co = case (ctEvEqRel ctev, fe_eq_rel fmode) of
+                          rewrite_co = case (ctEvEqRel ctev, eq_rel) of
                             (ReprEq, _rel)  -> ASSERT( _rel == ReprEq )
                                     -- if this ASSERT fails, then
                                     -- eqCanRewriteFR answered incorrectly
@@ -1304,15 +1472,14 @@ flatten_tyvar fmode tv
                     -- we are not going to touch the returned coercion
                     -- so ctEvCoercion is fine.
 
-           _other -> Left `liftM` flattenTyVarFinal fmode tv
+           _other -> Left `liftM` flattenTyVarFinal tv
     } } }
 
-flattenTyVarFinal :: FlattenEnv -> TcTyVar -> TcS TyVar
-flattenTyVarFinal fmode tv
+flattenTyVarFinal :: TcTyVar -> FlatM TyVar
+flattenTyVarFinal tv
   = -- Done, but make sure the kind is zonked
     do { let kind       = tyVarKind tv
-             kind_fmode = setFEMode fmode FM_SubstOnly
-       ; (new_knd, _kind_co) <- flatten_one kind_fmode kind
+       ; (new_knd, _kind_co) <- setMode FM_SubstOnly $ flatten_one kind
        ; return (setVarType tv new_knd) }
 
 {-
@@ -1400,11 +1567,6 @@ ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
 ctFlavourRole :: Ct -> CtFlavourRole
 ctFlavourRole = ctEvFlavourRole . cc_ev
 
--- | Extract the flavour and role from a 'FlattenEnv'
-feFlavourRole :: FlattenEnv -> CtFlavourRole
-feFlavourRole (FE { fe_flavour = flav, fe_eq_rel = eq_rel })
-  = (flav, eq_rel)
-
 eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
 -- Very important function!
 -- See Note [eqCanRewrite]
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index e83709cb5f..ce34d1fa3c 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -171,20 +171,20 @@ solveSimples :: Cts -> TcS ()
 
 solveSimples cts
   = {-# SCC "solveSimples" #-}
-    do { dyn_flags <- getDynFlags
-       ; updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
-       ; solve_loop (maxSubGoalDepth dyn_flags) }
+    do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
+       ; solve_loop }
   where
-    solve_loop max_depth
+    solve_loop
       = {-# SCC "solve_loop" #-}
-        do { sel <- selectNextWorkItem max_depth
+        do { sel <- selectNextWorkItem
            ; case sel of
               NoWorkRemaining     -- Done, successfuly (modulo frozen)
                 -> return ()
-              MaxDepthExceeded cnt ct -- Failure, depth exceeded
-                -> wrapErrTcS $ solverDepthErrorTcS cnt (ctEvidence ct)
+              MaxDepthExceeded ct -- Failure, depth exceeded
+                -> wrapErrTcS $ solverDepthErrorTcS (ctLoc ct) (ctPred ct)
               NextWorkItem ct     -- More work, loop around!
-                -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
+                -> do { runSolverPipeline thePipeline ct
+                      ; solve_loop } }
 
 
 -- | Extract the (inert) givens and invoke the plugins on them.
@@ -312,26 +312,26 @@ type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
 
 data SelectWorkItem
        = NoWorkRemaining      -- No more work left (effectively we're done!)
-       | MaxDepthExceeded SubGoalCounter Ct
+       | MaxDepthExceeded Ct
                               -- More work left to do but this constraint has exceeded
-                              -- the maximum depth for one of the subgoal counters and we
-                              -- must stop
+                              -- the maximum depth and we must stop
        | NextWorkItem Ct      -- More work left, here's the next item to look at
 
-selectNextWorkItem :: SubGoalDepth -- Max depth allowed
-                   -> TcS SelectWorkItem
-selectNextWorkItem max_depth
-  = updWorkListTcS_return pick_next
+selectNextWorkItem :: TcS SelectWorkItem
+selectNextWorkItem
+  = do { dflags <- getDynFlags
+       ; updWorkListTcS_return (pick_next dflags) }
   where
-    pick_next :: WorkList -> (SelectWorkItem, WorkList)
-    pick_next wl
+    pick_next :: DynFlags -> WorkList -> (SelectWorkItem, WorkList)
+    pick_next dflags wl
       = case selectWorkItem wl of
           (Nothing,_)
               -> (NoWorkRemaining,wl)           -- No more work
           (Just ct, new_wl)
-              | Just cnt <- subGoalDepthExceeded max_depth (ctLocDepth (ctLoc ct)) -- Depth exceeded
-              -> (MaxDepthExceeded cnt ct,new_wl)
-          (Just ct, new_wl)
+              | subGoalDepthExceeded dflags (ctLocDepth (ctLoc ct)) 
+              -> (MaxDepthExceeded ct,new_wl)   -- Depth exceeded
+
+              | otherwise
               -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
 
 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
@@ -616,7 +616,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
   , isWanted ev_w
   , Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls ty
   = do let ev_cs =
-             case lookupInertDict inerts (ctEvLoc ev_w) cls tys of
+             case lookupInertDict inerts cls tys of
                Just ev | isGiven ev -> mkEvCs (ctEvTerm ev)
                _ -> mkEvCs (EvCallStack EvCsEmpty)
 
@@ -629,7 +629,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
        setWantedEvBind (ctEvId ev_w) ev_tm
        stopWith ev_w "Wanted CallStack IP"
 
-  | Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
+  | Just ctev_i <- lookupInertDict inerts cls tys
   = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
        ; case inert_effect of
            IRKeep    -> return ()
@@ -1272,7 +1272,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
   | not (isWanted fl)   -- Never use instances for Given or Derived constraints
   = try_fundeps_and_return
 
-  | Just ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
+  | Just ev <- lookupSolvedDict inerts cls xis   -- Cached
   = do { setWantedEvBind dict_id (ctEvTerm ev);
        ; stopWith fl "Dict/Top (cached)" }
 
@@ -1287,7 +1287,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
      dict_pred = mkClassPred cls xis
      dict_loc = ctEvLoc fl
      dict_origin = ctLocOrigin dict_loc
-     deeper_loc = bumpCtLocDepth CountConstraints dict_loc
+     deeper_loc = bumpCtLocDepth dict_loc
 
      solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
@@ -1298,7 +1298,8 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
              ; setWantedEvBind dict_id ev_term
              ; stopWith fl "Dict/Top (solved, no new work)" }
         | otherwise
-        = do { traceTcS "doTopReact/found non-nullary instance for" $
+        = do { checkReductionDepth deeper_loc dict_pred
+             ; traceTcS "doTopReact/found non-nullary instance for" $
                ppr dict_id
              ; setWantedEvBind dict_id ev_term
              ; let mk_new_wanted ev
@@ -1382,7 +1383,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
           ; stopWith old_ev "Fun/Top (wanted)" } } }
   where
     loc = ctEvLoc old_ev
-    deeper_loc = bumpCtLocDepth CountTyFunApps loc
+    deeper_loc = bumpCtLocDepth loc
 
     try_improvement
       | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
@@ -1400,7 +1401,6 @@ shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
 shortCutReduction old_ev fsk ax_co fam_tc tc_args
   | isGiven old_ev
   = ASSERT( ctEvEqRel old_ev == NomEq )
-    runFlatten $
     do { (xis, cos) <- flattenManyNom old_ev tc_args
                -- ax_co :: F args ~ G tc_args
                -- cos   :: xis ~ tc_args
@@ -1414,7 +1414,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                                         `mkTcTransCo` ctEvCoercion old_ev) )
 
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; emitFlatWork new_ct
+       ; emitWorkCt new_ct
        ; stopWith old_ev "Fun/Top (given, shortcut)" }
 
   | otherwise
@@ -1434,11 +1434,11 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                                       `mkTcTransCo` ctEvCoercion new_ev))
 
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; emitFlatWork new_ct
+       ; emitWorkCt new_ct
        ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
   where
     loc = ctEvLoc old_ev
-    deeper_loc = bumpCtLocDepth CountTyFunApps loc
+    deeper_loc = bumpCtLocDepth loc
 
 dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 -- (dischargeFmv x fmv co ty)
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 59a4e0ddfb..cce1705b04 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -16,7 +16,7 @@ For state that is global and should be returned at the end (e.g not part
 of the stack mechanism), you should use an TcRef (= IORef) to store them.
 -}
 
-{-# LANGUAGE CPP, ExistentialQuantification #-}
+{-# LANGUAGE CPP, ExistentialQuantification, GeneralizedNewtypeDeriving #-}
 
 module TcRnTypes(
         TcRnIf, TcRn, TcM, RnM, IfM, IfL, IfG, -- The monad is opaque outside this module
@@ -57,16 +57,15 @@ module TcRnTypes(
         ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel,
         mkNonCanonical, mkNonCanonicalCt,
         ctEvPred, ctEvLoc, ctEvEqRel,
-        ctEvTerm, ctEvCoercion, ctEvId, ctEvCheckDepth,
+        ctEvTerm, ctEvCoercion, ctEvId,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
         dropDerivedWC, insolubleImplic, trulyInsoluble,
 
         Implication(..), ImplicStatus(..), isInsolubleStatus,
-        SubGoalCounter(..),
-        SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
-        bumpSubGoalDepth, subGoalCounterValue, subGoalDepthExceeded,
+        SubGoalDepth, initialSubGoalDepth,
+        bumpSubGoalDepth, subGoalDepthExceeded,
         CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin, setCtLocEnv, setCtLocSpan,
@@ -109,7 +108,6 @@ import TyCon    ( TyCon )
 import ConLike  ( ConLike(..) )
 import DataCon  ( DataCon, dataConUserType, dataConOrigArgTys )
 import PatSyn   ( PatSyn, patSynType )
-import TysWiredIn ( coercibleClass )
 import TcType
 import Annotations
 import InstEnv
@@ -1747,31 +1745,30 @@ ctEvFlavour (CtDerived {}) = Derived
 
 Note [SubGoalDepth]
 ~~~~~~~~~~~~~~~~~~~
-The 'SubGoalCounter' takes care of stopping the constraint solver from looping.
-Because of the different use-cases of regular constaints and type function
-applications, there are two independent counters. Therefore, this datatype is
-abstract. See Note [WorkList]
+The 'SubGoalDepth' takes care of stopping the constraint solver from looping.
 
-Each counter starts at zero and increases.
+The counter starts at zero and increases. It includes dictionary constraints,
+equality simplification, and type family reduction. (Why combine these? Because
+it's actually quite easy to mistake one for another, in sufficiently involved
+scenarios, like ConstraintKinds.)
 
-* The "dictionary constraint counter" counts the depth of type class
-  instance declarations.  Example:
+The flag -fcontext-stack=n (not very well named!) fixes the maximium
+level.
+
+* The counter includes the depth of type class instance declarations.  Example:
      [W] d{7} : Eq [Int]
   That is d's dictionary-constraint depth is 7.  If we use the instance
      $dfEqList :: Eq a => Eq [a]
   to simplify it, we get
      d{7} = $dfEqList d'{8}
-  where d'{8} : Eq Int, and d' has dictionary-constraint depth 8.
+  where d'{8} : Eq Int, and d' has depth 8.
 
   For civilised (decidable) instance declarations, each increase of
   depth removes a type constructor from the type, so the depth never
   gets big; i.e. is bounded by the structural depth of the type.
 
-  The flag -fcontext-stack=n (not very well named!) fixes the maximium
-  level.
-
-* The "type function reduction counter" does the same thing when resolving
-* qualities involving type functions. Example:
+* The counter also increments when resolving
+equalities involving type functions. Example:
   Assume we have a wanted at depth 7:
     [W] d{7} : F () ~ a
   If thre is an type function equation "F () = Int", this would be rewritten to
@@ -1779,79 +1776,37 @@ Each counter starts at zero and increases.
   and remembered as having depth 8.
 
   Again, without UndecidableInstances, this counter is bounded, but without it
-  can resolve things ad infinitum. Hence there is a maximum level. But we use a
-  different maximum, as we expect possibly many more type function reductions
-  in sensible programs than type class constraints.
+  can resolve things ad infinitum. Hence there is a maximum level.
 
-  The flag -ftype-function-depth=n fixes the maximium level.
--}
+* Lastly, every time an equality is rewritten, the counter increases. Again,
+  rewriting an equality constraint normally makes progress, but it's possible
+  the "progress" is just the reduction of an infinitely-reducing type family.
+  Hence we need to track the rewrites.
 
-data SubGoalCounter = CountConstraints | CountTyFunApps
+When compiling a program requires a greater depth, then GHC recommends turning
+off this check entirely by setting -freduction-depth=0. This is because the
+exact number that works is highly variable, and is likely to change even between
+minor releases. Because this check is solely to prevent infinite compilation
+times, it seems safe to disable it when a user has ascertained that their program
+doesn't loop at the type level.
 
-data SubGoalDepth  -- See Note [SubGoalDepth]
-   = SubGoalDepth
-         {-# UNPACK #-} !Int      -- Dictionary constraints
-         {-# UNPACK #-} !Int      -- Type function reductions
-  deriving (Eq, Ord)
+-}
 
-instance Outputable SubGoalDepth where
- ppr (SubGoalDepth c f) =  angleBrackets $
-        char 'C' <> colon <> int c <> comma <>
-        char 'F' <> colon <> int f
+-- | See Note [SubGoalDepth]
+newtype SubGoalDepth = SubGoalDepth Int
+  deriving (Eq, Ord, Outputable)
 
 initialSubGoalDepth :: SubGoalDepth
-initialSubGoalDepth = SubGoalDepth 0 0
-
-maxSubGoalDepth :: DynFlags -> SubGoalDepth
-maxSubGoalDepth dflags = SubGoalDepth (ctxtStkDepth dflags) (tyFunStkDepth dflags)
-
-bumpSubGoalDepth :: SubGoalCounter -> SubGoalDepth -> SubGoalDepth
-bumpSubGoalDepth CountConstraints (SubGoalDepth c f) = SubGoalDepth (c+1) f
-bumpSubGoalDepth CountTyFunApps   (SubGoalDepth c f) = SubGoalDepth c (f+1)
-
-subGoalCounterValue :: SubGoalCounter -> SubGoalDepth -> Int
-subGoalCounterValue CountConstraints (SubGoalDepth c _) = c
-subGoalCounterValue CountTyFunApps   (SubGoalDepth _ f) = f
-
-subGoalDepthExceeded :: SubGoalDepth -> SubGoalDepth -> Maybe SubGoalCounter
-subGoalDepthExceeded (SubGoalDepth mc mf) (SubGoalDepth c f)
-  | c > mc    = Just CountConstraints
-  | f > mf    = Just CountTyFunApps
-  | otherwise = Nothing
-
--- | Checks whether the evidence can be used to solve a goal with the given minimum depth
--- See Note [Preventing recursive dictionaries]
-ctEvCheckDepth :: Class -> CtLoc -> CtEvidence -> Bool
-ctEvCheckDepth cls target ev
-  | isWanted ev
-  , cls == coercibleClass  -- The restriction applies only to Coercible
-  = ctLocDepth target <= ctLocDepth (ctEvLoc ev)
-  | otherwise = True
+initialSubGoalDepth = SubGoalDepth 0
 
-{-
-Note [Preventing recursive dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-NB: this will go away when we start treating Coercible as an equality.
-
-We have some classes where it is not very useful to build recursive
-dictionaries (Coercible, at the moment). So we need the constraint solver to
-prevent that. We conservatively ensure this property using the subgoal depth of
-the constraints: When solving a Coercible constraint at depth d, we do not
-consider evidence from a depth <= d as suitable.
-
-Therefore we need to record the minimum depth allowed to solve a CtWanted. This
-is done in the SubGoalDepth field of CtWanted. Most code now uses mkCtWanted,
-which initializes it to initialSubGoalDepth (i.e. 0); but when requesting a
-Coercible instance (requestCoercible in TcInteract), we bump the current depth
-by one and use that.
-
-There are two spots where wanted contraints attempted to be solved
-using existing constraints: lookupInertDict and lookupSolvedDict in
-TcSMonad.  Both use ctEvCheckDepth to make the check. That function
-ensures that a Given constraint can always be used to solve a goal
-(i.e. they are at depth infinity, for our purposes)
+bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
+bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
 
+subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
+subGoalDepthExceeded dflags (SubGoalDepth d)
+  = mkIntWithInf d > reductionDepth dflags
 
+{-
 ************************************************************************
 *                                                                      *
             CtLoc
@@ -1897,8 +1852,8 @@ ctLocSpan (CtLoc { ctl_env = lcl}) = tcl_loc lcl
 setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
 setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (lcl { tcl_loc = loc })
 
-bumpCtLocDepth :: SubGoalCounter -> CtLoc -> CtLoc
-bumpCtLocDepth cnt loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth cnt d }
+bumpCtLocDepth :: CtLoc -> CtLoc
+bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d }
 
 setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
 setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 16ac1141a8..5000fd5a64 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -9,7 +9,6 @@ module TcSMonad (
     extendWorkListCts, appendWorkList, selectWorkItem,
     workListSize,
     updWorkListTcS, updWorkListTcS_return,
-    runFlatten, emitFlatWork,
 
     -- The TcS monad
     TcS, runTcS, runTcSWithEvBinds,
@@ -29,7 +28,7 @@ module TcSMonad (
     setWantedTyBind, reportUnifications,
     setEvBind, setWantedEvBind, setEvBindIfWanted,
     newEvVar, newGivenEvVar, newGivenEvVars,
-    newDerived, emitNewDerived,
+    newDerived, emitNewDerived, checkReductionDepth,
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
@@ -44,7 +43,7 @@ module TcSMonad (
     splitInertCans, removeInertCts,
     prepareInertsForImplications,
     addInertCan, insertInertItemTcS, insertFunEq,
-    emitInsoluble, emitWorkNC,
+    emitInsoluble, emitWorkNC, emitWorkCt,
     EqualCtList,
 
     -- Inert CDictCans
@@ -108,6 +107,7 @@ import Type
 import TcEvidence
 import Class
 import TyCon
+import TcErrors   ( solverDepthErrorTcS )
 
 import Name
 import RdrName (RdrName, GlobalRdrEnv)
@@ -160,55 +160,6 @@ so that it's easier to deal with them first, but the separation
 is not strictly necessary. Notice that non-canonical constraints
 are also parts of the worklist.
 
-Note [The flattening work list]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The "flattening work list", held in the tcs_flat_work field of TcSEnv,
-is a list of CFunEqCans generated during flattening.  The key idea
-is this.  Consider flattening (Eq (F (G Int) (H Bool)):
-  * The flattener recursively calls itself on sub-terms before building
-    the main term, so it will encounter the terms in order
-              G Int
-              H Bool
-              F (G Int) (H Bool)
-    flattening to sub-goals
-              w1: G Int ~ fuv0
-              w2: H Bool ~ fuv1
-              w3: F fuv0 fuv1 ~ fuv2
-
-  * Processing w3 first is BAD, because we can't reduce i t,so it'll
-    get put into the inert set, and later kicked out when w1, w2 are
-    solved.  In Trac #9872 this led to inert sets containing hundreds
-    of suspended calls.
-
-  * So we want to process w1, w2 first.
-
-  * So you might think that we should just use a FIFO deque for the work-list,
-    so that putting adding goals in order w1,w2,w3 would mean we processed
-    w1 first.
-
-  * BUT suppose we have 'type instance G Int = H Char'.  Then processing
-    w1 leads to a new goal
-                w4: H Char ~ fuv0
-    We do NOT want to put that on the far end of a deque!  Instead we want
-    to put it at the *front* of the work-list so that we continue to work
-    on it.
-
-So the work-list structure is this:
-
-  * The wl_funeqs is a LIFO stack; we push new goals (such as w4) on
-    top (extendWorkListFunEq), and take new work from the top
-    (selectWorkItem).
-
-  * When flattening, emitFlatWork pushes new flattening goals (like
-    w1,w2,w3) onto the flattening work list, tcs_flat_work, another
-    push-down stack.
-
-  * When we finish flattening, we *reverse* the tcs_flat_work stack
-    onto the wl_funeqs stack (which brings w1 to the top).
-
-The function runFlatten initialised the tcs_flat_work stack, and reverses
-it onto wl_fun_eqs at the end.
-
 -}
 
 -- See Note [WorkList priorities]
@@ -299,35 +250,6 @@ instance Outputable WorkList where
             ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
           ])
 
-emitFlatWork :: Ct -> TcS ()
--- See Note [The flattening work list]
-emitFlatWork ct
-  = TcS $ \env ->
-    do { let flat_ref = tcs_flat_work env
-       ; TcM.updTcRef flat_ref (ct :) }
-
-runFlatten :: TcS a -> TcS a
--- Run thing_inside (which does flattening), and put all
--- the work it generates onto the main work list
--- See Note [The flattening work list]
-runFlatten (TcS thing_inside)
-  = TcS $ \env ->
-    do { let flat_ref = tcs_flat_work env
-       ; old_flats <- TcM.updTcRefX flat_ref (\_ -> [])
-       ; res <- thing_inside env
-       ; new_flats <- TcM.updTcRefX flat_ref (\_ -> old_flats)
-       ; TcM.updTcRef (tcs_worklist env) (add_flats new_flats)
-       ; return res }
-  where
-    add_flats new_flats wl
-      = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
-
-    add_funeqs []     wl = wl
-    add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
-      -- add_funeqs fs ws = reverse fs ++ ws
-      -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
-      --        = [f3,f2,f1,w1,w2,w3,w4]
-
 {-
 ************************************************************************
 *                                                                      *
@@ -975,30 +897,28 @@ lookupFlatCache fam_tc tys
     lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
 
 
-lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
+lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
-lookupInInerts loc pty
+lookupInInerts pty
   | ClassPred cls tys <- classifyPredType pty
   = do { inerts <- getTcSInerts
-       ; return (lookupSolvedDict inerts loc cls tys `mplus`
-                 lookupInertDict (inert_cans inerts) loc cls tys) }
+       ; return (lookupSolvedDict inerts cls tys `mplus`
+                 lookupInertDict (inert_cans inerts) cls tys) }
   | otherwise -- NB: No caching for equalities, IPs, holes, or errors
   = return Nothing
 
-lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
+lookupInertDict :: InertCans -> Class -> [Type] -> Maybe CtEvidence
+lookupInertDict (IC { inert_dicts = dicts }) cls tys
   = case findDict dicts cls tys of
-      Just ct | let ev = ctEvidence ct
-              , ctEvCheckDepth cls loc ev
-              -> Just ev
+      Just ct -> Just (ctEvidence ct)
       _       -> Nothing
 
-lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
+lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
 -- Returns just if exactly this predicate type exists in the solved.
-lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
+lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
   = case findDict solved cls tys of
-      Just ev | ctEvCheckDepth cls loc ev -> Just ev
-      _                                   -> Nothing
+      Just ev -> Just ev
+      _       -> Nothing
 
 {-
 ************************************************************************
@@ -1214,9 +1134,7 @@ data TcSEnv
 
       -- The main work-list and the flattening worklist
       -- See Note [Work list priorities] and
-      --     Note [The flattening work list]
-      tcs_worklist  :: IORef WorkList, -- Current worklist
-      tcs_flat_work :: IORef [Ct]      -- Flattening worklist
+      tcs_worklist  :: IORef WorkList -- Current worklist
     }
 
 ---------------
@@ -1316,14 +1234,12 @@ runTcSWithEvBinds ev_binds_var tcs
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef is
        ; wl_var <- TcM.newTcRef emptyWorkList
-       ; fw_var <- TcM.newTcRef (panic "Flat work list")
 
        ; let env = TcSEnv { tcs_ev_binds  = ev_binds_var
                           , tcs_unified   = unified_var
                           , tcs_count     = step_count
                           , tcs_inerts    = inert_var
-                          , tcs_worklist  = wl_var
-                          , tcs_flat_work = fw_var }
+                          , tcs_worklist  = wl_var }
 
              -- Run the computation
        ; res <- unTcS tcs env
@@ -1372,13 +1288,11 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
                                    -- See Note [Do not inherit the flat cache]
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
-       ; new_fw_var    <- TcM.newTcRef (panic "Flat work list")
        ; let nest_env = TcSEnv { tcs_ev_binds    = ref
                                , tcs_unified     = unified_var
                                , tcs_count       = count
                                , tcs_inerts      = new_inert_var
-                               , tcs_worklist    = new_wl_var
-                               , tcs_flat_work   = new_fw_var }
+                               , tcs_worklist    = new_wl_var }
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
@@ -1494,6 +1408,11 @@ emitWorkNC evs
   = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
        ; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
 
+emitWorkCt :: Ct -> TcS ()
+emitWorkCt ct
+  = do { traceTcS "Emitting fresh (canonical) work" (ppr ct)
+       ; updWorkListTcS (extendWorkListCt ct) }
+
 emitInsoluble :: Ct -> TcS ()
 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
 emitInsoluble ct
@@ -1680,7 +1599,8 @@ newFlattenSkolem :: CtFlavour -> CtLoc
                  -> TcType         -- F xis
                  -> TcS (CtEvidence, TcTyVar)    -- [W] x:: F xis ~ fsk
 newFlattenSkolem Given loc fam_ty
-  =  do { fsk <- wrapTcS $
+  =  do { checkReductionDepth loc fam_ty
+        ; fsk <- wrapTcS $
                  do { uniq <- TcM.newUnique
                     ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
                     ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
@@ -1690,7 +1610,8 @@ newFlattenSkolem Given loc fam_ty
         ; return (ev, fsk) }
 
 newFlattenSkolem _ loc fam_ty  -- Make a wanted
-  = do { fuv <- wrapTcS $
+  = do { checkReductionDepth loc fam_ty
+       ; fuv <- wrapTcS $
                  do { uniq <- TcM.newUnique
                     ; ref  <- TcM.newMutVar Flexi
                     ; let details = MetaTv { mtv_info  = FlatMetaTv
@@ -1789,7 +1710,8 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 --               See Note [Do not create Given kind equalities]
 newGivenEvVar loc (pred, rhs)
   = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
-    do { new_ev <- newEvVar pred
+    do { checkReductionDepth loc pred
+       ; new_ev <- newEvVar pred
        ; setEvBind (mkGivenEvBind new_ev rhs)
        ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
 
@@ -1842,13 +1764,14 @@ TcCanonical), and will do no harm.
 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
 -- Don't look up in the solved/inerts; we know it's not there
 newWantedEvVarNC loc pty
-  = do { new_ev <- newEvVar pty
+  = do { checkReductionDepth loc pty
+       ; new_ev <- newEvVar pty
        ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
 
 newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
 -- For anything except ClassPred, this is the same as newWantedEvVarNC
 newWantedEvVar loc pty
-  = do { mb_ct <- lookupInInerts loc pty
+  = do { mb_ct <- lookupInInerts pty
        ; case mb_ct of
             Just ctev | not (isDerived ctev)
                       -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
@@ -1870,11 +1793,21 @@ newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
 -- Returns Nothing    if cached,
 --         Just pred  if not cached
 newDerived loc pred
-  = do { mb_ct <- lookupInInerts loc pred
+  = do { checkReductionDepth loc pred
+       ; mb_ct <- lookupInInerts pred
        ; return (case mb_ct of
                     Just {} -> Nothing
                     Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
 
+-- | Checks if the depth of the given location is too much. Fails if
+-- it's too big, with an appropriate error message.
+checkReductionDepth :: CtLoc -> TcType   -- ^ type being reduced
+                    -> TcS ()
+checkReductionDepth loc ty
+  = do { dflags <- getDynFlags
+       ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
+         wrapErrTcS $
+         solverDepthErrorTcS loc ty }
 
 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 293f7cf56b..d3000a651a 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -44,6 +44,7 @@ import Util
 import ListSetOps
 import SrcLoc
 import Outputable
+import BasicTypes       ( IntWithInf, infinity )
 import FastString
 
 import Control.Monad
@@ -1315,37 +1316,15 @@ sizePred on them), or we might get an infinite loop if that PredType
 is irreducible. See Trac #5581.
 -}
 
-data TypeSize = TS Int | TSBig   -- TSBig behaves like positive infinity
-                                 -- Used when we encounter a type function
-
-instance Num TypeSize where
-  fromInteger n = TS (fromInteger n)
-  TS a + TS b = TS (a+b)
-  _    + _    = TSBig
-  negate = panic "TypeSize:negate"
-  abs    = panic "TypeSize:abs"
-  signum = panic "TypeSize:signum"
-  (*)    = panic "TypeSize:*"
-  (-)    = panic "TypeSize:-"
-
-instance Eq TypeSize where
-  TS a  == TS b  = a==b
-  TSBig == TSBig = True
-  _     == _     = False
-
-instance Ord TypeSize where
-  TS a  `compare` TS b  = a `compare` b
-  TS _  `compare` TSBig = LT
-  TSBig `compare` TS _  = GT
-  TSBig `compare` TSBig = EQ
+type TypeSize = IntWithInf
 
 sizeType :: Type -> TypeSize
 -- Size of a type: the number of variables and constructors
 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
 sizeType (TyVarTy {})      = 1
 sizeType (TyConApp tc tys)
-  | isTypeFamilyTyCon tc   = TSBig  -- Type-family applications can
-                                    -- expand to any arbitrary size
+  | isTypeFamilyTyCon tc   = infinity  -- Type-family applications can
+                                       -- expand to any arbitrary size
   | otherwise              = sizeTypes tys + 1
 sizeType (LitTy {})        = 1
 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml
index bdb783d0a6..1385acb7a5 100644
--- a/docs/users_guide/flags.xml
+++ b/docs/users_guide/flags.xml
@@ -706,8 +706,14 @@
         </thead>
         <tbody>
           <row>
+            <entry><option>-freduction-depth=</option><replaceable>n</replaceable></entry>
+	    <entry>set the <link linkend="undecidable-instances">limit for type simplification</link>. Default is 200.</entry>
+	    <entry>dynamic</entry>
+	    <entry></entry>
+	  </row>
+	  <row>
             <entry><option>-fcontext-stack=</option><replaceable>n</replaceable></entry>
-            <entry>set the <link linkend="undecidable-instances">limit for type-class context reduction</link>. Default is 100.</entry>
+            <entry>Deprecated. Use <option>-freduction-depth=</option><replaceable>n</replaceable> instead.</entry>
             <entry>dynamic</entry>
             <entry></entry>
           </row>
@@ -731,7 +737,7 @@
           </row>
           <row>
             <entry><option>-ftype-function-depth=</option><replaceable>n</replaceable></entry>
-            <entry>set the <link linkend="type-families">limit for type function reductions</link>. Default is 200.</entry>
+            <entry>Deprecated. Use <option>-freduction-depth=</option><replaceable>n</replaceable> instead.</entry>
             <entry>dynamic</entry>
             <entry></entry>
           </row>
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index e8337dd559..832b02fff3 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -5080,7 +5080,13 @@ both the Paterson Conditions and the Coverage Condition
 Termination is still ensured by having a
 fixed-depth recursion stack.  If you exceed the stack depth you get a
 sort of backtrace, and the opportunity to increase the stack depth
-with <option>-fcontext-stack=</option><emphasis>N</emphasis>.
+with <option>-freduction-depth=</option><emphasis>N</emphasis>.
+However, if you should exceed the default reduction depth limit,
+it is probably best just to disable depth checking, with
+<option>-freduction-depth=0</option>. The exact depth your program
+requires depends on minutiae of your code, and it may change between
+minor GHC releases. The safest bet for released code -- if you're sure
+that it should compile in finite time -- is just to disable the check.
 </para>
 
 <para>
diff --git a/testsuite/tests/deriving/should_fail/T4846.stderr b/testsuite/tests/deriving/should_fail/T4846.stderr
index ab24af374e..33b125f2bc 100644
--- a/testsuite/tests/deriving/should_fail/T4846.stderr
+++ b/testsuite/tests/deriving/should_fail/T4846.stderr
@@ -1,6 +1,6 @@
 
 T4846.hs:29:1:
-    Couldn't match type ‘BOOL’ with ‘Bool’
+    Couldn't match type ‘Bool’ with ‘BOOL’
     arising from trying to show that the representations of
       ‘Expr Bool’ and
       ‘Expr BOOL’ are the same
@@ -9,7 +9,7 @@ T4846.hs:29:1:
         GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL
     In an equation for ‘mkExpr’:
         mkExpr = GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL
-    When typechecking the code for  ‘mkExpr’
+    When typechecking the code for ‘mkExpr’
       in a derived instance for ‘B BOOL’:
       To see the code I am typechecking, use -ddump-deriv
     In the instance declaration for ‘B BOOL’
diff --git a/testsuite/tests/indexed-types/should_compile/T10139.hs b/testsuite/tests/indexed-types/should_compile/T10139.hs
new file mode 100644
index 0000000000..8963b7cb1c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T10139.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances,
+             MultiParamTypeClasses, FunctionalDependencies #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+module T10139 where
+
+import GHC.Exts
+import Data.Monoid
+
+class Monoid v => Measured v a | a -> v where
+  _measure :: v -> a
+data FingerTree v a = Dummy v a
+singleton :: Measured v a => a -> FingerTree v a
+singleton = undefined
+
+class DOps a where
+  plus :: a -> D a -> a
+
+type family D a :: *
+type instance D (FingerTree (Size Int, v) (Sized a)) = [Diff (Normal a)]
+
+type family Normal a :: *
+
+data Diff a = Add Int a
+
+newtype Sized a = Sized a
+newtype Size a = Size a
+
+-- This works:
+{-
+instance (Measured (Size Int, v) (Sized a), Coercible (Normal a) (Sized a)) => DOps (FingerTree (Size Int, v) (Sized a)) where
+  plus = foldr (\(Add index val) seq -> singleton ((coerce) val))
+-}
+
+-- This hangs:
+instance (Measured (Size Int, v) (Sized a), Coercible (Normal a) (Sized a)) => DOps (FingerTree (Size Int, v) (Sized a)) where
+  plus = foldr (flip f)
+    where f _seq x = case x of
+            Add _index val -> singleton ((coerce) val)
diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.stderr b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
index b5014d0049..282aa2f886 100644
--- a/testsuite/tests/indexed-types/should_compile/T3208b.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
@@ -1,6 +1,6 @@
 
 T3208b.hs:15:10:
-    Could not deduce: STerm o0 ~ OTerm o0
+    Could not deduce: OTerm o0 ~ STerm o0
     from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
       bound by the type signature for:
                fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
@@ -10,15 +10,12 @@ T3208b.hs:15:10:
     In an equation for ‘fce'’: fce' f = fce (apply f)
 
 T3208b.hs:15:15:
-    Could not deduce: OTerm o0 ~ OTerm a
+    Could not deduce: OTerm o0 ~ STerm a
     from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
       bound by the type signature for:
                fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
       at T3208b.hs:14:9-56
-    NB: ‘OTerm’ is a type function, and may not be injective
     The type variable ‘o0’ is ambiguous
-    Expected type: STerm a
-      Actual type: OTerm o0
     Relevant bindings include
       f :: a (bound at T3208b.hs:15:6)
       fce' :: a -> c (bound at T3208b.hs:15:1)
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index f4df93324a..c6dde35f79 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -252,3 +252,5 @@ test('T9582', normal, compile, [''])
 test('T9090', normal, compile, [''])
 test('T10020', normal, compile, [''])
 test('T10079', normal, compile, [''])
+test('T10139', normal, compile, [''])
+
diff --git a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
index 6a566f4f63..5a0443bfa1 100644
--- a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
+++ b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
@@ -1,11 +1,11 @@
-

-NoMatchErr.hs:19:7:

-    Couldn't match type ‘Memo d’ with ‘Memo d0’

-    NB: ‘Memo’ is a type function, and may not be injective

-    The type variable ‘d0’ is ambiguous

-    Expected type: Memo d a -> Memo d a

-      Actual type: Memo d0 a -> Memo d0 a

-    In the ambiguity check for the type signature for ‘f’:

-      f :: forall d a. Fun d => Memo d a -> Memo d a

-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

-    In the type signature for ‘f’: f :: (Fun d) => Memo d a -> Memo d a

+
+NoMatchErr.hs:19:7:
+    Couldn't match type ‘Memo d0’ with ‘Memo d’
+    NB: ‘Memo’ is a type function, and may not be injective
+    The type variable ‘d0’ is ambiguous
+    Expected type: Memo d a -> Memo d a
+      Actual type: Memo d0 a -> Memo d0 a
+    In the ambiguity check for the type signature for ‘f’:
+      f :: forall d a. Fun d => Memo d a -> Memo d a
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In the type signature for ‘f’: f :: (Fun d) => Memo d a -> Memo d a
diff --git a/testsuite/tests/indexed-types/should_fail/T1897b.stderr b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
index c6d318f047..936aa26924 100644
--- a/testsuite/tests/indexed-types/should_fail/T1897b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
@@ -1,6 +1,6 @@
 
 T1897b.hs:16:1:
-    Couldn't match type ‘Depend a0’ with ‘Depend a’
+    Couldn't match type ‘Depend a’ with ‘Depend a0’
     NB: ‘Depend’ is a type function, and may not be injective
     The type variable ‘a0’ is ambiguous
     Expected type: t (Depend a) -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
index 43a38de87b..fb28764c80 100644
--- a/testsuite/tests/indexed-types/should_fail/T2664.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -1,15 +1,15 @@
 
 T2664.hs:31:52:
-    Could not deduce: a ~ b
+    Could not deduce: b ~ a
     from the context: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b))
       bound by the type signature for:
                newPChan :: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
                            IO (PChan (a :*: b), PChan c)
       at T2664.hs:23:5-12
-      ‘a’ is a rigid type variable bound by
-          the instance declaration at T2664.hs:22:10
       ‘b’ is a rigid type variable bound by
           the instance declaration at T2664.hs:22:10
+      ‘a’ is a rigid type variable bound by
+          the instance declaration at T2664.hs:22:10
     Expected type: Dual (Dual a)
       Actual type: b
     Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index d2d62439f3..7069de90d8 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -1,8 +1,8 @@
 
 T4179.hs:26:16:
-    Couldn't match type ‘A3 (x (A2 (FCon x) -> A3 (FCon x)))’
-                  with ‘A3 (FCon x)’
-    NB: ‘A3’ is a type function, and may not be injective
+    Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
+                   with ‘A2 (FCon x)’
+    NB: ‘A2’ is a type function, and may not be injective
     Expected type: x (A2 (FCon x) -> A3 (FCon x))
                    -> A2 (FCon x) -> A3 (FCon x)
       Actual type: x (A2 (FCon x) -> A3 (FCon x))
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index 3bffb4fc6c..a68e8c2226 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -1,25 +1,25 @@
-

-T5439.hs:82:28:

-    Couldn't match type ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’

-                  with ‘Attempt (WaitOpResult (WaitOps rs))’

-    Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))

-      Actual type: f (Attempt (WaitOpResult (WaitOps rs)))

-    Relevant bindings include

-      register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool

-        (bound at T5439.hs:64:9)

-      ev :: f (Attempt (WaitOpResult (WaitOps rs)))

-        (bound at T5439.hs:61:22)

-      ops :: WaitOps rs (bound at T5439.hs:61:18)

-      registerWaitOp :: WaitOps rs

-                        -> f (Attempt (WaitOpResult (WaitOps rs))) -> IO Bool

-        (bound at T5439.hs:61:3)

-    In the first argument of ‘complete’, namely ‘ev’

-    In the expression: complete ev

-

-T5439.hs:82:39:

-    Couldn't match expected type ‘Peano n0’

-                with actual type ‘Attempt α0’

-    In the second argument of ‘($)’, namely

-      ‘Failure (e :: SomeException)’

-    In the second argument of ‘($)’, namely

-      ‘inj $ Failure (e :: SomeException)’

+
+T5439.hs:82:28:
+    Couldn't match type ‘Attempt (HElemOf rs)’
+                   with ‘Attempt (HHead (HDrop n0 l0)) -> Attempt (HElemOf l0)’
+    Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
+      Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
+    Relevant bindings include
+      register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
+        (bound at T5439.hs:64:9)
+      ev :: f (Attempt (WaitOpResult (WaitOps rs)))
+        (bound at T5439.hs:61:22)
+      ops :: WaitOps rs (bound at T5439.hs:61:18)
+      registerWaitOp :: WaitOps rs
+                        -> f (Attempt (WaitOpResult (WaitOps rs))) -> IO Bool
+        (bound at T5439.hs:61:3)
+    In the first argument of ‘complete’, namely ‘ev’
+    In the expression: complete ev
+
+T5439.hs:82:39:
+    Couldn't match expected type ‘Peano n0’
+                with actual type ‘Attempt α0’
+    In the second argument of ‘($)’, namely
+      ‘Failure (e :: SomeException)’
+    In the second argument of ‘($)’, namely
+      ‘inj $ Failure (e :: SomeException)’
diff --git a/testsuite/tests/indexed-types/should_fail/T7010.stderr b/testsuite/tests/indexed-types/should_fail/T7010.stderr
index 4ff0597a1b..9441b3857e 100644
--- a/testsuite/tests/indexed-types/should_fail/T7010.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7010.stderr
@@ -1,7 +1,7 @@
-

-T7010.hs:53:27:

-    Couldn't match type ‘Serial (IO Float)’ with ‘IO Float’

-    Expected type: (Float, ValueTuple Vector)

-      Actual type: (Float, ValueTuple Float)

-    In the first argument of ‘withArgs’, namely ‘plug’

-    In the expression: withArgs plug

+
+T7010.hs:53:27:
+    Couldn't match type ‘IO Float’ with ‘Serial (IO Float)’
+    Expected type: (Float, ValueTuple Vector)
+      Actual type: (Float, ValueTuple Float)
+    In the first argument of ‘withArgs’, namely ‘plug’
+    In the expression: withArgs plug
diff --git a/testsuite/tests/indexed-types/should_fail/T7729.stderr b/testsuite/tests/indexed-types/should_fail/T7729.stderr
index 1f3d19d426..053d54e264 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729.stderr
@@ -1,6 +1,6 @@
 
 T7729.hs:36:14:
-    Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
+    Couldn't match type ‘t0 (BasePrimMonad m)’ with ‘BasePrimMonad m’
     The type variable ‘t0’ is ambiguous
     Expected type: t0 (BasePrimMonad m) a -> Rand m a
       Actual type: BasePrimMonad (Rand m) a -> Rand m a
diff --git a/testsuite/tests/indexed-types/should_fail/T7788.hs b/testsuite/tests/indexed-types/should_fail/T7788.hs
new file mode 100644
index 0000000000..56f378d202
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7788.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T7788 where
+
+data Proxy a = Proxy
+
+foo :: Proxy (F (Fix Id)) -> ()
+foo = undefined
+
+newtype Fix a = Fix (a (Fix a))
+newtype Id a = Id a
+
+type family F a
+type instance F (Fix a) = F (a (Fix a))
+type instance F (Id a) = F a
+
+main :: IO ()
+main = print $ foo Proxy
diff --git a/testsuite/tests/indexed-types/should_fail/T7788.stderr b/testsuite/tests/indexed-types/should_fail/T7788.stderr
new file mode 100644
index 0000000000..31e23cd3fd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7788.stderr
@@ -0,0 +1,10 @@
+
+T7788.hs:9:7:
+    Reduction stack overflow; size = 201
+    When simplifying the following type: F (Id (Fix Id))
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
+    In the expression: undefined
+    In an equation for ‘foo’: foo = undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T7967.stderr b/testsuite/tests/indexed-types/should_fail/T7967.stderr
index a7269451fe..44fb064594 100644
--- a/testsuite/tests/indexed-types/should_fail/T7967.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7967.stderr
@@ -1,6 +1,6 @@
 
 T7967.hs:31:26:
-    Couldn't match type ‘'[]’ with ‘h0 : t0’
+    Couldn't match type ‘h0 : t0’ with ‘'[]’
     Expected type: Index n l
       Actual type: Index 'Zero (h0 : t0)
     In the expression: IZero
diff --git a/testsuite/tests/indexed-types/should_fail/T8550.hs b/testsuite/tests/indexed-types/should_fail/T8550.hs
new file mode 100644
index 0000000000..d3639a4a9d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T8550.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances #-}
+
+module T8550 where
+
+type family F a
+type instance F () = F ()
+data A where
+  A :: F () ~ () => A
+x :: A
+x = A
+
+main :: IO ()
+main = seq A (return ())
+
+-- Note: This worked in GHC 7.8, but I (Richard E) think this regression
+-- is acceptable.
diff --git a/testsuite/tests/indexed-types/should_fail/T8550.stderr b/testsuite/tests/indexed-types/should_fail/T8550.stderr
new file mode 100644
index 0000000000..1092ed247d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T8550.stderr
@@ -0,0 +1,11 @@
+
+T8550.hs:13:12:
+    Reduction stack overflow; size = 201
+    When simplifying the following type: F ()
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
+    In the expression: A
+    In the expression: seq A (return ())
+    In an equation for ‘main’: main = seq A (return ())
diff --git a/testsuite/tests/indexed-types/should_fail/T9036.stderr b/testsuite/tests/indexed-types/should_fail/T9036.stderr
index 9a9486ea45..2fdf9c6557 100644
--- a/testsuite/tests/indexed-types/should_fail/T9036.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9036.stderr
@@ -1,13 +1,13 @@
-

-T9036.hs:17:17:

-    Couldn't match type ‘Curried t [t]’ with ‘Curried t0 [t0]’

-    NB: ‘Curried’ is a type function, and may not be injective

-    The type variable ‘t0’ is ambiguous

-    Expected type: Maybe (GetMonad t after) -> Curried t [t]

-      Actual type: Maybe (GetMonad t0 after) -> Curried t0 [t0]

-    In the ambiguity check for the type signature for ‘simpleLogger’:

-      simpleLogger :: forall t after.

-                      Maybe (GetMonad t after) -> Curried t [t]

-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

-    In the type signature for ‘simpleLogger’:

-      simpleLogger :: Maybe (GetMonad t after) -> t `Curried` [t]

+
+T9036.hs:17:17:
+    Couldn't match type ‘Curried t0 [t0]’ with ‘Curried t [t]’
+    NB: ‘Curried’ is a type function, and may not be injective
+    The type variable ‘t0’ is ambiguous
+    Expected type: Maybe (GetMonad t after) -> Curried t [t]
+      Actual type: Maybe (GetMonad t0 after) -> Curried t0 [t0]
+    In the ambiguity check for the type signature for ‘simpleLogger’:
+      simpleLogger :: forall t after.
+                      Maybe (GetMonad t after) -> Curried t [t]
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In the type signature for ‘simpleLogger’:
+      simpleLogger :: Maybe (GetMonad t after) -> t `Curried` [t]
diff --git a/testsuite/tests/indexed-types/should_fail/T9554.hs b/testsuite/tests/indexed-types/should_fail/T9554.hs
new file mode 100644
index 0000000000..99c27e24f4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T9554.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
+
+module T9554 where
+
+import Data.Proxy
+
+type family F a where
+  F a = F (F a)
+
+foo :: Proxy (F Bool) -> Proxy (F Int)
+foo x = x
+
+main = case foo Proxy of Proxy -> putStrLn "Made it!"
diff --git a/testsuite/tests/indexed-types/should_fail/T9554.stderr b/testsuite/tests/indexed-types/should_fail/T9554.stderr
new file mode 100644
index 0000000000..0baf5d78ff
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T9554.stderr
@@ -0,0 +1,22 @@
+
+T9554.hs:11:9:
+    Reduction stack overflow; size = 201
+    When simplifying the following type:
+      F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
+    In the expression: x
+    In an equation for ‘foo’: foo x = x
+
+T9554.hs:13:17:
+    Reduction stack overflow; size = 201
+    When simplifying the following type:
+      F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
+    In the first argument of ‘foo’, namely ‘Proxy’
+    In the expression: foo Proxy
diff --git a/testsuite/tests/indexed-types/should_fail/T9580.stderr b/testsuite/tests/indexed-types/should_fail/T9580.stderr
index fdb457ae31..2ed480fb7b 100644
--- a/testsuite/tests/indexed-types/should_fail/T9580.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9580.stderr
@@ -2,8 +2,8 @@
 [2 of 2] Compiling T9580            ( T9580.hs, T9580.o )
 
 T9580.hs:7:9:
-    Couldn't match representation of type ‘Double’
-                             with that of ‘Dimensional Int Double’
+    Couldn't match representation of type ‘Dimensional Int Double’
+                             with that of ‘Double’
     Relevant role signatures: type role Dimensional nominal nominal
     The data constructor ‘T9580a.Quantity'’
       of newtype ‘Dimensional Int v’ is not in scope
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 5f65a7a4fd..2e1a8761c5 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -133,4 +133,6 @@ test('T9662', normal, compile_fail, [''])
 test('T7862', normal, compile, [''])
 test('T9896', normal, compile_fail, [''])
 test('T6088', normal, compile_fail, [''])
-
+test('T7788', normal, compile_fail, [''])
+test('T8550', normal, compile_fail, [''])
+test('T9554', normal, compile_fail, [''])
diff --git a/testsuite/tests/perf/compiler/T5321FD.hs b/testsuite/tests/perf/compiler/T5321FD.hs
index 004f487098..308ff348b9 100644
--- a/testsuite/tests/perf/compiler/T5321FD.hs
+++ b/testsuite/tests/perf/compiler/T5321FD.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -fcontext-stack=1000 #-} 
+{-# OPTIONS_GHC -freduction-depth=1000 #-} 
 {-# LANGUAGE 
      FlexibleContexts, FlexibleInstances, FunctionalDependencies, 
      MultiParamTypeClasses, TypeSynonymInstances, 
diff --git a/testsuite/tests/perf/compiler/T5321Fun.hs b/testsuite/tests/perf/compiler/T5321Fun.hs
index bf70ce5221..6c38d2c0c3 100644
--- a/testsuite/tests/perf/compiler/T5321Fun.hs
+++ b/testsuite/tests/perf/compiler/T5321Fun.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -fcontext-stack=1000 #-} 
+{-# OPTIONS_GHC -freduction-depth=1000 #-} 
 {-# LANGUAGE 
      FlexibleContexts, FlexibleInstances, FunctionalDependencies, 
      MultiParamTypeClasses, TypeSynonymInstances, 
diff --git a/testsuite/tests/perf/compiler/T5837.stderr b/testsuite/tests/perf/compiler/T5837.stderr
index df4fbefb77..7add7e39bc 100644
--- a/testsuite/tests/perf/compiler/T5837.stderr
+++ b/testsuite/tests/perf/compiler/T5837.stderr
@@ -1,7 +1,7 @@
 
 T5837.hs:8:6:
-    Type function application stack overflow; size = 51
-    Use -ftype-function-depth=N to increase stack size to N
+    Reduction stack overflow; size = 51
+    When simplifying the following type:
       TF
         (TF
            (TF
@@ -27,33 +27,7 @@ T5837.hs:8:6:
                                                                        (TF
                                                                           (TF
                                                                              (TF
-                                                                                (TF
-                                                                                   (TF
-                                                                                      (TF
-                                                                                         (TF
-                                                                                            (TF
-                                                                                               (TF
-                                                                                                  (TF
-                                                                                                     (TF
-                                                                                                        (TF
-                                                                                                           (TF
-                                                                                                              (TF
-                                                                                                                 (TF
-                                                                                                                    (TF
-                                                                                                                       (TF
-                                                                                                                          (TF
-                                                                                                                             (TF
-                                                                                                                                (TF
-                                                                                                                                   (TF
-                                                                                                                                      (TF
-                                                                                                                                         (TF
-                                                                                                                                            (TF
-                                                                                                                                               (TF
-                                                                                                                                                  (TF
-                                                                                                                                                     (TF
-                                                                                                                                                        (TF
-                                                                                                                                                           (TF
-                                                                                                                                                              a))))))))))))))))))))))))))))))))))))))))))))))))))
+                                                                                a))))))))))))))))))))))))
       ~ (TF
            (TF
               (TF
@@ -80,33 +54,7 @@ T5837.hs:8:6:
                                                                              (TF
                                                                                 (TF
                                                                                    (TF
-                                                                                      (TF
-                                                                                         (TF
-                                                                                            (TF
-                                                                                               (TF
-                                                                                                  (TF
-                                                                                                     (TF
-                                                                                                        (TF
-                                                                                                           (TF
-                                                                                                              (TF
-                                                                                                                 (TF
-                                                                                                                    (TF
-                                                                                                                       (TF
-                                                                                                                          (TF
-                                                                                                                             (TF
-                                                                                                                                (TF
-                                                                                                                                   (TF
-                                                                                                                                      (TF
-                                                                                                                                         (TF
-                                                                                                                                            (TF
-                                                                                                                                               (TF
-                                                                                                                                                  (TF
-                                                                                                                                                     (TF
-                                                                                                                                                        (TF
-                                                                                                                                                           (TF
-                                                                                                                                                              (TF
-                                                                                                                                                                 (TF
-                                                                                                                                                                    a))))))))))))))))))))))))))))))))))))))))))))))))))),
+                                                                                      a))))))))))))))))))))))))),
          TF
            (TF
               (TF
@@ -133,33 +81,11 @@ T5837.hs:8:6:
                                                                              (TF
                                                                                 (TF
                                                                                    (TF
-                                                                                      (TF
-                                                                                         (TF
-                                                                                            (TF
-                                                                                               (TF
-                                                                                                  (TF
-                                                                                                     (TF
-                                                                                                        (TF
-                                                                                                           (TF
-                                                                                                              (TF
-                                                                                                                 (TF
-                                                                                                                    (TF
-                                                                                                                       (TF
-                                                                                                                          (TF
-                                                                                                                             (TF
-                                                                                                                                (TF
-                                                                                                                                   (TF
-                                                                                                                                      (TF
-                                                                                                                                         (TF
-                                                                                                                                            (TF
-                                                                                                                                               (TF
-                                                                                                                                                  (TF
-                                                                                                                                                     (TF
-                                                                                                                                                        (TF
-                                                                                                                                                           (TF
-                                                                                                                                                              (TF
-                                                                                                                                                                 (TF
-                                                                                                                                                                    Int))))))))))))))))))))))))))))))))))))))))))))))))))))
+                                                                                      Int))))))))))))))))))))))))))
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
     In the ambiguity check for the type signature for ‘t’:
       t :: forall a. (a ~ TF (a, Int)) => Int
     In the type signature for ‘t’: t :: (a ~ TF (a, Int)) => Int
diff --git a/testsuite/tests/perf/compiler/T9872a.hs b/testsuite/tests/perf/compiler/T9872a.hs
index 16a0adcb44..7ceba4ee66 100644
--- a/testsuite/tests/perf/compiler/T9872a.hs
+++ b/testsuite/tests/perf/compiler/T9872a.hs
@@ -4,7 +4,7 @@
  - See:  The Monad Read, Issue #8 - http://www.haskell.org/wikiupload/d/dd/TMR-Issue8.pdf
  -}
 
-{-# OPTIONS_GHC -ftype-function-depth=400 #-}
+{-# OPTIONS_GHC -freduction-depth=400 #-}
 
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -164,4 +164,4 @@ type instance Solutions (Cons c cs) = AllowedCombinations (Orientations c) (Solu
 {-
  - solutions [] = [ [] ]
  - solutions (c:cs) = [ (o:sol) | sol <- solutions cs, o <- orientations c, allowed o 
--}
\ No newline at end of file
+-}
diff --git a/testsuite/tests/perf/compiler/T9872b.hs b/testsuite/tests/perf/compiler/T9872b.hs
index 77c204e097..eaa6afb142 100644
--- a/testsuite/tests/perf/compiler/T9872b.hs
+++ b/testsuite/tests/perf/compiler/T9872b.hs
@@ -4,7 +4,7 @@
  - See:  http://stackoverflow.com/questions/26538595
  -}
 
-{-# OPTIONS_GHC -ftype-function-depth=400 #-}
+{-# OPTIONS_GHC -freduction-depth=400 #-}
 
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeFamilies #-}
diff --git a/testsuite/tests/perf/compiler/T9872c.hs b/testsuite/tests/perf/compiler/T9872c.hs
index b6a0f0d40f..b925c9f791 100644
--- a/testsuite/tests/perf/compiler/T9872c.hs
+++ b/testsuite/tests/perf/compiler/T9872c.hs
@@ -4,7 +4,7 @@
  - See:  http://stackoverflow.com/questions/26538595
  -}
 
-{-# OPTIONS_GHC -ftype-function-depth=400 #-}
+{-# OPTIONS_GHC -freduction-depth=400 #-}
 
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeFamilies #-}
diff --git a/testsuite/tests/perf/compiler/T9872d.hs b/testsuite/tests/perf/compiler/T9872d.hs
index a247336500..4930ffecfe 100644
--- a/testsuite/tests/perf/compiler/T9872d.hs
+++ b/testsuite/tests/perf/compiler/T9872d.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -freduction-depth=0 #-}   -- this should terminate!
 
 module T9872d where
 -- Code from Jan Stolarek, labelled "exp-tyfams.hs" on Trac #9872,
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index a874866949..4a6ab3e49f 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -191,7 +191,7 @@ test('T4801',
 #            # 2014-10-13: 48 stricter seqDmdType
 
       compiler_stats_num_field('bytes allocated',
-          [(platform('x86_64-apple-darwin'), 464872776, 5),
+          [(platform('x86_64-apple-darwin'), 434058304, 5),
                            # expected value: 510938976 (amd64/OS X):
 
            (wordsize(32), 203962148, 10),
@@ -329,7 +329,7 @@ test('T5030',
            # 2014-12-10:  227205560 constraint solver got worse again; more agressive solving
            #                        of family-applications leads to less sharing, I think
 
-           (wordsize(64), 449042120, 10)]),
+           (wordsize(64), 403932600, 10)]),
              # Previously 530000000 (+/- 10%)
              # 17/1/13:   602993184  (x86_64/Linux)
              #            (new demand analyser)
@@ -345,11 +345,12 @@ test('T5030',
              # 2014-12-08 340969128  constraint solver perf improvements (esp kick-out)
              # 2014-12-10 449042120  constraint solver got worse again; more agressive solving
              #                          of family-applications leads to less sharing, I think
+             # 2015-03-17 403932600  tweak to solver algorithm
 
        only_ways(['normal'])
       ],
      compile,
-     ['-fcontext-stack=300'])
+     ['-freduction-depth=300'])
 
 test('T5631',
      [compiler_stats_num_field('bytes allocated',
@@ -490,7 +491,7 @@ test('T5837',
              # 2014-12-01: 135914136 (Windows laptop, regression see below)
              # 2014-12-08  115905208  Constraint solver perf improvements (esp kick-out)
  
-           (wordsize(64), 231155640, 10)])
+           (wordsize(64), 53424304, 10)])
              # sample: 3926235424 (amd64/Linux, 15/2/2012)
              # 2012-10-02 81879216
              # 2012-09-20 87254264 amd64/Linux
@@ -504,8 +505,9 @@ test('T5837',
              # 2014-12-08 234790312 Constraint solver perf improvements (esp kick-out)
              # 2014-12-16 231155640 Mac  Flattener parameterized over roles;
              #                           some optimization
+             # 2015-03-17 53424304  Mac  Better depth checking; fails earlier
       ],
-      compile_fail,['-ftype-function-depth=50'])
+      compile_fail,['-freduction-depth=50'])
 
 test('T6048',
      [ only_ways(['optasm']),
@@ -611,10 +613,11 @@ test('T9872c',
 test('T9872d',
      [ only_ways(['normal']),
        compiler_stats_num_field('bytes allocated',
-          [(wordsize(64), 687562440, 5),
+          [(wordsize(64), 726679784, 5),
           # 2014-12-18    796071864   Initally created
           # 2014-12-18    739189056   Reduce type families even more eagerly
           # 2015-01-07    687562440   TrieMap leaf compression
+          # 2015-03-17    726679784   tweak to solver; probably flattens more
            (wordsize(32), 328810212, 5)
           ]),
       ],
diff --git a/testsuite/tests/roles/should_fail/Roles10.stderr b/testsuite/tests/roles/should_fail/Roles10.stderr
index 4275385081..4434352652 100644
--- a/testsuite/tests/roles/should_fail/Roles10.stderr
+++ b/testsuite/tests/roles/should_fail/Roles10.stderr
@@ -1,6 +1,6 @@
 
 Roles10.hs:16:12:
-    Couldn't match representation of type ‘Char’ with that of ‘Bool’
+    Couldn't match representation of type ‘Bool’ with that of ‘Char’
     arising from the coercion of the method ‘meth’
       from type ‘Int -> F Int’ to type ‘Age -> F Age’
     Relevant role signatures: type role F nominal
diff --git a/testsuite/tests/typecheck/should_compile/T10184.hs b/testsuite/tests/typecheck/should_compile/T10184.hs
new file mode 100644
index 0000000000..0369ebd992
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T10184.hs
@@ -0,0 +1,9 @@
+module T10184 where
+
+import Data.Coerce
+
+newtype Bar a = Bar (Either a (Bar a))
+newtype Age = MkAge Int
+
+x :: Bar Age
+x = coerce (Bar (Left (5 :: Int)))
diff --git a/testsuite/tests/typecheck/should_compile/T10185.hs b/testsuite/tests/typecheck/should_compile/T10185.hs
new file mode 100644
index 0000000000..5185d10550
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T10185.hs
@@ -0,0 +1,7 @@
+module T10185 where
+
+import Data.Coerce
+import Data.Proxy
+
+foo :: (Coercible (a b) (c d), Coercible (c d) (e f)) => Proxy (c d) -> a b -> e f
+foo _ = coerce
diff --git a/testsuite/tests/typecheck/should_compile/TcCoercibleCompile.hs b/testsuite/tests/typecheck/should_compile/TcCoercibleCompile.hs
index cedf01326c..96220897e0 100644
--- a/testsuite/tests/typecheck/should_compile/TcCoercibleCompile.hs
+++ b/testsuite/tests/typecheck/should_compile/TcCoercibleCompile.hs
@@ -1,8 +1,49 @@
+{-# LANGUAGE RoleAnnotations #-}
 {-# OPTIONS_GHC -fwarn-unused-imports  #-}
 
-import GHC.Prim (coerce)
+import Data.Coerce
+import Data.Proxy
 import Data.Monoid (First(First)) -- check whether the implicit use of First is noted
 
+-- see https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver/V2
+
+foo1 :: f a -> f a
+foo1 = coerce
+
+newtype X = MkX (Int -> X)
+foo2 :: X -> X
+foo2 = coerce
+
+newtype X2 a = MkX2 Char
+type role X2 nominal
+
+foo3 :: X2 Int -> X2 Bool
+foo3 = coerce
+
+newtype Age = MkAge Int
+newtype Y a = MkY a
+type role Y nominal
+
+foo4 :: Y Age -> Y Int
+foo4 = coerce
+
+newtype Z a = MkZ ()
+type role Z representational
+
+foo5 :: Z Int -> Z Bool
+foo5 = coerce
+
+newtype App f a = MkApp (f a)
+
+foo6 :: f a -> App f a
+foo6 = coerce
+
+foo7 :: Coercible a b => b -> a
+foo7 = coerce
+
+foo8 :: (Coercible a b, Coercible b c) => Proxy b -> a -> c
+foo8 _ = coerce
+
 main = print (coerce $ Just (1::Int)  :: First Int)
 
 
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d4e71c709e..f01e720552 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -287,7 +287,7 @@ test('T2497', normal, compile, [''])
      
 
 # Omitting temporarily
-test('syn-perf', normal, compile, ['-fcontext-stack=30'])
+test('syn-perf', normal, compile, ['-freduction-depth=30'])
 test('syn-perf2', normal, compile, [''])
 
 test('LoopOfTheDay1', normal, compile, [''])
@@ -441,7 +441,9 @@ test('T9939', normal, compile, [''])
 test('T9973', normal, compile, [''])
 test('T9971', normal, compile, [''])
 test('T10031', normal, compile, [''])
+test('T10184', expect_broken(10184), compile, [''])
 test('T10072', normal, compile_fail, [''])
 test('T10100', normal, compile, [''])
 test('T10156', normal, compile, [''])
 test('T10177', normal, compile, [''])
+test('T10185', expect_broken(10185), compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack1.stderr b/testsuite/tests/typecheck/should_fail/ContextStack1.stderr
index d11a6255ed..db57e5a5e7 100644
--- a/testsuite/tests/typecheck/should_fail/ContextStack1.stderr
+++ b/testsuite/tests/typecheck/should_fail/ContextStack1.stderr
@@ -1,7 +1,10 @@
 
 ContextStack1.hs:10:5:
-    Context reduction stack overflow; size = 11
-    Use -fcontext-stack=N to increase stack size to N
-      Cls [[[[[[[[[[[()]]]]]]]]]]]
+    Reduction stack overflow; size = 11
+    When simplifying the following type: Cls [[[[[[[[[[()]]]]]]]]]]
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
     In the expression: meth
     In an equation for ‘t’: t = meth
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr b/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
index 8da1c39cfb..1a6d1d26aa 100644
--- a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
+++ b/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
@@ -1,10 +1,13 @@
 
 ContextStack2.hs:8:6:
-    Type function application stack overflow; size = 11
-    Use -ftype-function-depth=N to increase stack size to N
-      TF (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF a))))))))))
-      ~ (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF a))))))))))),
-         TF (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF Int))))))))))))
+    Reduction stack overflow; size = 11
+    When simplifying the following type:
+      TF (TF (TF (TF (TF a))))
+      ~ (TF (TF (TF (TF (TF (TF a))))), TF (TF (TF (TF (TF (TF Int))))))
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
     In the ambiguity check for the type signature for ‘t’:
       t :: forall a. (a ~ TF (a, Int)) => Int
     In the type signature for ‘t’: t :: (a ~ TF (a, Int)) => Int
diff --git a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
index ff39e7e6ef..932ba108d4 100644
--- a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
+++ b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
@@ -1,52 +1,52 @@
-

-FrozenErrorTests.hs:12:12:

-    Couldn't match type ‘Int’ with ‘Bool’

-    Inaccessible code in

-      a pattern with constructor: MkT3 :: forall a. (a ~ Bool) => T a,

-      in a case alternative

-    In the pattern: MkT3

-    In a case alternative: MkT3 -> ()

-    In the expression: case x of { MkT3 -> () }

-

-FrozenErrorTests.hs:26:9:

-    Occurs check: cannot construct the infinite type: a ~ [a]

-    Expected type: [a]

-      Actual type: F a Bool

-    Relevant bindings include

-      test1 :: a (bound at FrozenErrorTests.hs:26:1)

-    In the expression: goo1 False undefined

-    In an equation for ‘test1’: test1 = goo1 False undefined

-

-FrozenErrorTests.hs:29:15:

-    Couldn't match type ‘[Int]’ with ‘Int’

-    Expected type: [[Int]]

-      Actual type: F [Int] Bool

-    In the first argument of ‘goo2’, namely ‘(goo1 False undefined)’

-    In the expression: goo2 (goo1 False undefined)

-    In an equation for ‘test2’: test2 = goo2 (goo1 False undefined)

-

-FrozenErrorTests.hs:30:9:

-    Couldn't match type ‘[Int]’ with ‘Int’

-    Expected type: [[Int]]

-      Actual type: F [Int] Bool

-    In the expression: goo1 False (goo2 undefined)

-    In an equation for ‘test3’: test3 = goo1 False (goo2 undefined)

-

-FrozenErrorTests.hs:45:15:

-    Couldn't match type ‘T2 c c’ with ‘M (T2 (T2 c c) c)’

-    Expected type: T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)

-      Actual type: F (T2 (T2 c c) c) Bool

-    Relevant bindings include

-      test4 :: T2 (T2 c c) c (bound at FrozenErrorTests.hs:45:1)

-    In the first argument of ‘goo4’, namely ‘(goo3 False undefined)’

-    In the expression: goo4 (goo3 False undefined)

-    In an equation for ‘test4’: test4 = goo4 (goo3 False undefined)

-

-FrozenErrorTests.hs:46:9:

-    Couldn't match type ‘T2 c c’ with ‘M (T2 (T2 c c) c)’

-    Expected type: T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)

-      Actual type: F (T2 (T2 c c) c) Bool

-    Relevant bindings include

-      test5 :: T2 (T2 c c) c (bound at FrozenErrorTests.hs:46:1)

-    In the expression: goo3 False (goo4 undefined)

-    In an equation for ‘test5’: test5 = goo3 False (goo4 undefined)

+
+FrozenErrorTests.hs:12:12:
+    Couldn't match type ‘Int’ with ‘Bool’
+    Inaccessible code in
+      a pattern with constructor: MkT3 :: forall a. (a ~ Bool) => T a,
+      in a case alternative
+    In the pattern: MkT3
+    In a case alternative: MkT3 -> ()
+    In the expression: case x of { MkT3 -> () }
+
+FrozenErrorTests.hs:26:9:
+    Occurs check: cannot construct the infinite type: a ~ [a]
+    Expected type: [a]
+      Actual type: F a Bool
+    Relevant bindings include
+      test1 :: a (bound at FrozenErrorTests.hs:26:1)
+    In the expression: goo1 False undefined
+    In an equation for ‘test1’: test1 = goo1 False undefined
+
+FrozenErrorTests.hs:29:15:
+    Couldn't match type ‘Int’ with ‘[Int]’
+    Expected type: [[Int]]
+      Actual type: F [Int] Bool
+    In the first argument of ‘goo2’, namely ‘(goo1 False undefined)’
+    In the expression: goo2 (goo1 False undefined)
+    In an equation for ‘test2’: test2 = goo2 (goo1 False undefined)
+
+FrozenErrorTests.hs:30:9:
+    Couldn't match type ‘Int’ with ‘[Int]’
+    Expected type: [[Int]]
+      Actual type: F [Int] Bool
+    In the expression: goo1 False (goo2 undefined)
+    In an equation for ‘test3’: test3 = goo1 False (goo2 undefined)
+
+FrozenErrorTests.hs:45:15:
+    Couldn't match type ‘T2 c c’ with ‘M (T2 (T2 c c) c)’
+    Expected type: T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)
+      Actual type: F (T2 (T2 c c) c) Bool
+    Relevant bindings include
+      test4 :: T2 (T2 c c) c (bound at FrozenErrorTests.hs:45:1)
+    In the first argument of ‘goo4’, namely ‘(goo3 False undefined)’
+    In the expression: goo4 (goo3 False undefined)
+    In an equation for ‘test4’: test4 = goo4 (goo3 False undefined)
+
+FrozenErrorTests.hs:46:9:
+    Couldn't match type ‘T2 c c’ with ‘M (T2 (T2 c c) c)’
+    Expected type: T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)
+      Actual type: F (T2 (T2 c c) c) Bool
+    Relevant bindings include
+      test5 :: T2 (T2 c c) c (bound at FrozenErrorTests.hs:46:1)
+    In the expression: goo3 False (goo4 undefined)
+    In an equation for ‘test5’: test5 = goo3 False (goo4 undefined)
diff --git a/testsuite/tests/typecheck/should_fail/T9318.stderr b/testsuite/tests/typecheck/should_fail/T9318.stderr
index 963d73e1fe..218ae97b77 100644
--- a/testsuite/tests/typecheck/should_fail/T9318.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9318.stderr
@@ -1,6 +1,6 @@
 
 T9318.hs:12:5:
-    Couldn't match type ‘Bool’ with ‘Char’
+    Couldn't match type ‘Char’ with ‘Bool’
     Expected type: F Int
       Actual type: Char
     In the pattern: 'x'
diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
index 52d2c25e97..41cc7cc47d 100644
--- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
@@ -1,12 +1,12 @@
 
 TcCoercibleFail.hs:11:8:
-    Couldn't match representation of type ‘()’ with that of ‘Int’
+    Couldn't match representation of type ‘Int’ with that of ‘()’
     In the expression: coerce
     In the expression: coerce $ one :: ()
     In an equation for ‘foo1’: foo1 = coerce $ one :: ()
 
 TcCoercibleFail.hs:14:8:
-    Couldn't match representation of type ‘m Age’ with that of ‘m Int’
+    Couldn't match representation of type ‘m Int’ with that of ‘m Age’
     NB: We cannot know what roles the parameters to ‘m’ have;
       we must assume that the role is nominal
     Relevant bindings include
@@ -26,7 +26,7 @@ TcCoercibleFail.hs:16:8:
     In an equation for ‘foo3’: foo3 = coerce $ Map one () :: Map Age ()
 
 TcCoercibleFail.hs:18:8:
-    Couldn't match representation of type ‘Down Int’ with that of ‘Int’
+    Couldn't match representation of type ‘Int’ with that of ‘Down Int’
     Relevant role signatures: type role Down representational
     The data constructor ‘Data.Ord.Down’
       of newtype ‘Down’ is not in scope
@@ -35,28 +35,33 @@ TcCoercibleFail.hs:18:8:
     In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int
 
 TcCoercibleFail.hs:21:8:
-    Couldn't match representation of type ‘()’ with that of ‘Void’
+    Couldn't match representation of type ‘Void’ with that of ‘()’
     In the expression: coerce :: Void -> ()
     In an equation for ‘foo5’: foo5 = coerce :: Void -> ()
 
 TcCoercibleFail.hs:24:9:
-    Couldn't match representation of type ‘()’
-                             with that of ‘VoidBad ()’
+    Couldn't match representation of type ‘VoidBad ()’
+                             with that of ‘()’
     Relevant role signatures: type role VoidBad phantom
     In the expression: coerce :: (VoidBad ()) -> ()
     In an equation for ‘foo5'’: foo5' = coerce :: (VoidBad ()) -> ()
 
 TcCoercibleFail.hs:28:8:
-    Context reduction stack overflow; size = 101
-    Use -fcontext-stack=N to increase stack size to N
-      Coercible (Fix (Either Int)) (Fix (Either Age))
+    Reduction stack overflow; size = 201
+    When simplifying the following type:
+      Coercible (Either Int (Fix (Either Int))) (Fix (Either Age))
+    Use -freduction-depth=0 to disable this check
+    (any upper bound you could choose might fail unpredictably with
+     minor updates to GHC, so disabling the check is recommended if
+     you're sure that type checking should terminate)
     In the expression: coerce :: Fix (Either Int) -> Fix (Either Age)
     In an equation for ‘foo6’:
         foo6 = coerce :: Fix (Either Int) -> Fix (Either Age)
 
 TcCoercibleFail.hs:29:8:
-    Couldn't match representation of type ‘()’
-                             with that of ‘Either Int (Fix (Either Int))’
+    Couldn't match representation of type ‘Either
+                                             Int (Fix (Either Int))’
+                             with that of ‘()’
     arising from trying to show that the representations of
       ‘Fix (Either Int)’ and
       ‘()’ are the same
diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr
index 797451d3bf..f4ebe40bb1 100644
--- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr
@@ -1,6 +1,6 @@
 
 TcCoercibleFail3.hs:12:7:
-    Couldn't match representation of type ‘NT2’ with that of ‘NT1’
+    Couldn't match representation of type ‘NT1’ with that of ‘NT2’
     arising from trying to show that the representations of
       ‘T NT1’ and
       ‘T NT2’ are the same
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 1ebb0a718f..7efbb70ce1 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -323,8 +323,8 @@ test('T8392a', normal, compile_fail, [''])
 test('T8428', normal, compile_fail, [''])
 test('T8450', normal, compile_fail, [''])
 test('T8514', normal, compile_fail, [''])
-test('ContextStack1', normal, compile_fail, ['-fcontext-stack=10'])
-test('ContextStack2', normal, compile_fail, ['-ftype-function-depth=10'])
+test('ContextStack1', normal, compile_fail, ['-freduction-depth=10'])
+test('ContextStack2', normal, compile_fail, ['-freduction-depth=10'])
 test('T8570', extra_clean(['T85570a.o', 'T8570a.hi','T85570b.o', 'T8570b.hi']),
      multimod_compile_fail, ['T8570', '-v0'])
 test('T8603', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.hs b/testsuite/tests/typecheck/should_fail/tcfail201.hs
index f9d3188682..ac59cb0b55 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.hs
@@ -15,7 +15,7 @@ data HsDoc id
 gfoldl' :: (forall a b . c (a -> b) -> a -> c b) -> (forall g . g -> c g) -> a -> c a
 gfoldl' k z hsDoc = case hsDoc of
 			  DocEmpty                  -> z DocEmpty
-			  (DocParagraph hsDoc)      -> z DocParagraph `k` hsDoc
+--			  (DocParagraph hsDoc)      -> z DocParagraph `k` hsDoc
 
 
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index 1414ceabb3..a69906452c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,20 +1,15 @@
 
-tcfail201.hs:18:28:
-    Couldn't match expected type ‘a’ with actual type ‘HsDoc id1’
+tcfail201.hs:17:58:
+    Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’
       ‘a’ is a rigid type variable bound by
           the type signature for:
-            gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
-                       -> (forall g. g -> c g) -> a -> c a
+          gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
+                     -> (forall g. g -> c g) -> a -> c a
           at tcfail201.hs:15:12
     Relevant bindings include
       hsDoc :: a (bound at tcfail201.hs:16:13)
       gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
                  -> (forall g. g -> c g) -> a -> c a
         (bound at tcfail201.hs:16:1)
-    In the pattern: DocParagraph hsDoc
-    In a case alternative:
-        (DocParagraph hsDoc) -> z DocParagraph `k` hsDoc
-    In the expression:
-      case hsDoc of {
-        DocEmpty -> z DocEmpty
-        (DocParagraph hsDoc) -> z DocParagraph `k` hsDoc }
+    In the first argument of ‘z’, namely ‘DocEmpty’
+    In the expression: z DocEmpty