Fixing the constraint solverwip/spj-solver-branch

This is in-flight work on fixing the constraint solver.
In particular I'm working on situations where the
constraint solver loops, which should never happen

  #12386 (only loosely related)
  #12522
  #12526
  #12444
  #12538

This is NOT DONE and not ready for review.  I'm
just committing it so I don't lose it.

Current status

Unexpected failures:
   hsc2hs/T12504.run                    T12504 [bad stdout] (normal)
   indexed-types/should_fail/T4179.run  T4179 [stderr mismatch] (normal)
   perf/compiler/T5837.run              T5837 [stderr mismatch] (normal)

20 files changed, 291 insertions, 240 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index b6a76c762b..f280f13bc8 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1394,7 +1394,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
              -- canonical, and we might loop if we were to use it in rewriting.
          else do { traceTcS "Occurs-check in representational equality"
                            (ppr xi1 $$ ppr xi2)
-                      ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
+                 ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
   where
     role = eqRelRole eq_rel
     xi1  = mkTyVarTy tv1
@@ -1410,19 +1410,9 @@ canEqTyVarTyVar :: CtEvidence           -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
 -- 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 kco2
-  | tv1 == tv2
-  = do { let mk_coh = case swapped of IsSwapped  -> mkTcCoherenceLeftCo
-                                      NotSwapped -> mkTcCoherenceRightCo
-       ; setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1 `mk_coh` kco2)
-       ; stopWith ev "Equal tyvars" }
-
--- We don't do this any more
--- See Note [Orientation of equalities with fmvs] in TcFlatten
---  | isFmvTyVar tv1  = do_fmv swapped            tv1 xi1 xi2 co1 co2
---  | isFmvTyVar tv2  = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
-
-  | swap_over       = do_swap
-  | otherwise       = no_swap
+  | tv1 == tv2 = do_same
+  | swap_over  = do_swap
+  | otherwise  = no_swap
   where
     role = eqRelRole eq_rel
     xi1 = mkTyVarTy tv1
@@ -1432,6 +1422,11 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
 
     no_swap = canon_eq swapped            tv1 xi1 xi2 co1 co2
     do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
+    do_same = do { let mk_coh = case swapped of
+                                   IsSwapped  -> mkTcCoherenceLeftCo
+                                   NotSwapped -> mkTcCoherenceRightCo
+                 ; setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1 `mk_coh` kco2)
+                 ; stopWith ev "Equal tyvars" }
 
     canon_eq swapped tv1 ty1 ty2 co1 co2
         -- ev  : tv1 ~ orhs  (not swapped) or   orhs ~ tv1   (swapped)
@@ -1450,33 +1445,10 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
              CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
                       , cc_rhs = ty2', cc_eq_rel = eq_rel } }
 
-{- We don't do this any more
-   See Note [Orientation of equalities with fmvs] in TcFlatten
-    -- tv1 is the flatten meta-var
-    do_fmv swapped tv1 xi1 xi2 co1 co2
-      | same_kind
-      = canon_eq swapped tv1 xi1 xi2 co1 co2
-      | otherwise  -- Presumably tv1 :: *, since it is a flatten meta-var,
-                   -- at a kind that has some interesting sub-kind structure.
-                   -- Since the two kinds are not the same, we must have
-                   -- tv1 `subKind` tv2, which is the wrong way round
-                   --   e.g.  (fmv::*) ~ (a::OpenKind)
-                   -- So make a new meta-var and use that:
-                   --         fmv ~ (beta::*)
-                   --         (a::OpenKind) ~ (beta::*)
-      = ASSERT2( k1_sub_k2,
-                 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)
-                                        (mkPrimEqPredRole (eqRelRole eq_rel)
-                                           g           tv_ty xi2)
-           ; emitWorkNC [new_ev]
-           ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
--}
-
     swap_over
+      | isFmvTyVar tv1 = False
+      | isFmvTyVar tv2 = True
+      
       -- If tv1 is touchable, swap only if tv2 is also
       -- touchable and it's strictly better to update the latter
       -- But see Note [Avoid unnecessary swaps]
@@ -1491,13 +1463,15 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
       -- If only one is a meta tyvar, put it on the left
       -- This is not because it'll be solved; but because
       -- the floating step looks for meta tyvars on the left
-      | isMetaTyVar tv2 = True
+      | isMetaTyVar tv2
+      = True
 
       -- So neither is a meta tyvar (including FlatMetaTv)
 
       -- If only one is a flatten skolem, put it on the left
       -- See Note [Eliminate flat-skols]
-      | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
+      | not (isFlattenTyVar tv1), isFlattenTyVar tv2
+      = True
 
       | otherwise = False
 
@@ -1971,6 +1945,11 @@ unify_derived loc role    orig_ty1 orig_ty2
       | tc1 == tc2, tys1 `equalLength` tys2
       , isInjectiveTyCon tc1 role
       = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
+
+    go (TyVarTy tv1) (TyVarTy tv2)
+      | tv1 == tv2
+      = return ()
+
     go (TyVarTy tv) ty2
       = do { mb_ty <- isFilledMetaTyVar_maybe tv
            ; case mb_ty of
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 4e02e99299..44d7dc715d 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -144,7 +144,7 @@ But since fsk = F alpha Int, this is really an occurs check error.  If
 that is all we know about alpha, we will succeed in constraint
 solving, producing a program with an infinite type.
 
-Even if we did finally get (g : fsk ~ Boo)l by solving (F alpha Int ~ fsk)
+Even if we did finally get (g : fsk ~ Bool) by solving (F alpha Int ~ fsk)
 using axiom, zonking would not see it, so (x::alpha) sitting in the
 tree will get zonked to an infinite type.  (Zonking always only does
 refl stuff.)
@@ -161,8 +161,9 @@ Look at Simple13, with unification-fmvs only
   [W] x : F a ~ fmv
 
 --> subst a in x
-       x = F g' ; x2
-   [W] x2 : F [fmv] ~ fmv
+  g' = g;[x]
+  x = F g' ; x2
+  [W] x2 : F [fmv] ~ fmv
 
 And now we have an evidence cycle between g' and x!
 
@@ -232,6 +233,7 @@ Old solution: always put fmvs on the left, so we get
       [W] fmv ~ alpha, F alpha ~ fmv, alpha ~ a
 
 BUT this works badly for Trac #10340:
+     type family Any :: *   -- No instances
      get :: MonadState s m => m s
      instance MonadState s (State s) where ...
 
@@ -510,6 +512,16 @@ 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])
 
+instance Outputable FlattenMode where
+  ppr FM_FlattenAll = text "FM_FlattenAll"
+  ppr FM_SubstOnly  = text "FM_SubstOnly"
+
+eqFlattenMode :: FlattenMode -> FlattenMode -> Bool
+eqFlattenMode FM_FlattenAll FM_FlattenAll = True
+eqFlattenMode FM_SubstOnly  FM_SubstOnly  = True
+--  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
+eqFlattenMode _  _ = False
+
 mkFlattenEnv :: FlattenMode -> CtEvidence -> FlatWorkListRef -> FlattenEnv
 mkFlattenEnv fm ctev ref = FE { fe_mode    = fm
                               , fe_loc     = ctEvLoc ctev
@@ -612,14 +624,9 @@ setEqRel new_eq_rel thing_inside
 setMode :: FlattenMode -> FlatM a -> FlatM a
 setMode new_mode thing_inside
   = FlatM $ \env ->
-    if new_mode `eq` fe_mode env
+    if new_mode `eqFlattenMode` 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
 
 -- | Use when flattening kinds/kind coercions. See
 -- Note [No derived kind equalities] in TcCanonical
@@ -789,6 +796,7 @@ flattenManyNom :: CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
 flattenManyNom ev tys
   = runFlatten FM_FlattenAll ev (flatten_many_nom tys)
 
+
 {- *********************************************************************
 *                                                                      *
 *           The main flattening functions
@@ -1105,15 +1113,14 @@ 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 roles tys
+               -- These roles are always going to be Nominal for now,
+               -- but not if #8177 is implemented
+           FM_SubstOnly -> do { let roles = tyConRolesX role tc
+                              ; (xis, cos) <- flatten_many roles tys
                               ; return ( mkTyConApp tc xis
                                        , mkTyConAppCo role tc cos ) }
-             where
-               -- These are always going to be Nominal for now,
-               -- but not if #8177 is implemented
-               roles = tyConRolesX role tc }
+
+           FM_FlattenAll -> flatten_exact_fam_app_fully tc tys }
 
 --       FM_Avoid tv flat_top ->
 --         do { (xis, cos) <- flatten_many fmode roles tys
@@ -1126,7 +1133,8 @@ 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) <- setEqRel NomEq $ flatten_many_nom tys
+       ; (xis, cos) <- setEqRel NomEq    $
+                       flatten_many_nom tys
        ; eq_rel <- getEqRel
        ; let role   = eqRelRole eq_rel
              ret_co = mkTyConAppCo role tc cos
@@ -1314,9 +1322,10 @@ flatten_tyvar1 tv
                          ; return (FTRFollowed ty (mkReflCo role ty)) } ;
            Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
                          ; fr <- getFlavourRole
-                         ; flatten_tyvar2  tv fr } }
+                         ; flatten_tyvar2 tv fr } }
 
 flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
+-- The tyvar is not filled-in meta-tyvar
 -- Try in the inert equalities
 -- See Definition [Applying a generalised substitution] in TcSMonad
 -- See Note [Stability of flattening] in TcSMonad
@@ -1332,12 +1341,14 @@ flatten_tyvar2 tv fr@(flavour, eq_rel)
 
   | otherwise   -- For non-derived equalities, consult the inert_eqs (only)
   = do { ieqs <- liftTcS $ getInertEqs
+       ; mode <- getMode
        ; case lookupDVarEnv 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` fr
-             ->  do { traceFlat "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
+             , let ct_fr = ctEvFlavourRole ctev
+             , ct_fr `eqCanRewriteFR` fr
+             ->  do { traceFlat "Following inert tyvar" (ppr mode <+> ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
                     ; let rewrite_co1 = mkSymCo $ ctEvCoercion ctev
                           rewrite_co  = case (ctEvEqRel ctev, eq_rel) of
                             (ReprEq, _rel)  -> ASSERT( _rel == ReprEq )
@@ -1485,8 +1496,7 @@ unflatten tv_eqs funeqs
              rhs' <- zonkTcType (mkTyConApp tc xis)
            ; case occurCheckExpand dflags fmv rhs' of
                OC_OK rhs''    -- Normal case: fill the tyvar
-                 -> do { setEvBindIfWanted ev
-                               (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
+                 -> do { setReflEvidence ev NomEq rhs''
                        ; unflattenFmv fmv rhs''
                        ; return rest }
 
@@ -1505,17 +1515,21 @@ unflatten tv_eqs funeqs
 
     ----------------
     unflatten_eq ::  DynFlags -> TcLevel -> Ct -> Cts -> TcS Cts
-    unflatten_eq dflags tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
+    unflatten_eq dflags tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv
+                                           , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
       | isFmvTyVar tv   -- Previously these fmvs were untouchable,
                         -- but now they are touchable
                         -- NB: unlike unflattenFmv, filling a fmv here does
                         --     bump the unification count; it is "improvement"
                         -- Note [Unflattening can force the solver to iterate]
-      = do { lhs_elim <- tryFill dflags tv rhs ev
-           ; if lhs_elim then return rest else
-        do { rhs_elim <- try_fill dflags tclvl ev rhs (mkTyVarTy tv)
-           ; if rhs_elim then return rest else
-             return (ct `consCts` rest) } }
+      , tyVarKind tv `eqType` typeKind rhs
+      = do { is_filled <- isFilledMetaTyVar tv
+           ; elim <- case (is_filled, tcGetTyVar_maybe rhs) of
+               (False, _)          -> tryFill      dflags eq_rel       tv rhs    ev
+               (True, Just rhs_tv) -> try_fill_rhs dflags eq_rel tclvl tv rhs_tv ev
+               (True, Nothing)     -> return False
+           ; if elim then return rest
+                     else return (ct `consCts` rest) }
 
       | otherwise
       = return (ct `consCts` rest)
@@ -1523,51 +1537,68 @@ unflatten tv_eqs funeqs
     unflatten_eq _ _ ct _ = pprPanic "unflatten_irred" (ppr ct)
 
     ----------------
+    try_fill_rhs dflags eq_rel tclvl lhs_tv rhs_tv ev
+         -- Constraint is lhs_tv ~ rhs_tv,
+         -- and lhs_tv is filled, so try RHS
+             
+      | isFmvTyVar rhs_tv
+      = do { is_filled <- isFilledMetaTyVar rhs_tv
+           ; if is_filled then return False
+             else tryFill dflags eq_rel rhs_tv (mkTyVarTy lhs_tv) ev }
+
+      | isTouchableMetaTyVar tclvl rhs_tv
+      , not (isSigTyVar rhs_tv)  -- LHS is a filled fmv, and so is a type
+                                 -- family appliaction, which a SigTv should
+                                 -- not unify with
+      = do { is_filled <- isFilledMetaTyVar rhs_tv
+           ; if is_filled then return False
+             else tryFill dflags eq_rel rhs_tv (mkTyVarTy lhs_tv) ev }
+             
+      | otherwise
+      = return False
+
+    ----------------
     finalise_eq :: Ct -> Cts -> TcS Cts
     finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv
                           , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
       | isFmvTyVar tv
       = do { ty1 <- zonkTcTyVar tv
-           ; ty2 <- zonkTcType rhs
-           ; let is_refl = ty1 `tcEqType` ty2
-           ; if is_refl then do { setEvBindIfWanted ev
-                                            (EvCoercion $
-                                             mkTcReflCo (eqRelRole eq_rel) rhs)
-                                ; return rest }
-                        else return (mkNonCanonical ev `consCts` rest) }
+           ; rhs' <- zonkTcType rhs
+           ; if ty1 `tcEqType` rhs'
+             then do { setReflEvidence ev eq_rel rhs'
+                     ; return rest }
+             else return (mkNonCanonical ev `consCts` rest) }
       | otherwise
       = return (mkNonCanonical ev `consCts` rest)
 
     finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
 
-    ----------------
-    try_fill dflags tclvl ev ty1 ty2
-      | Just tv1 <- tcGetTyVar_maybe ty1
-      , isTouchableOrFmv tclvl tv1
-      , typeKind ty1 `eqType` tyVarKind tv1
-      = tryFill dflags tv1 ty2 ev
-      | otherwise
-      = return False
-
-tryFill :: DynFlags -> TcTyVar -> TcType -> CtEvidence -> TcS Bool
--- (tryFill tv rhs ev) sees if 'tv' is an un-filled MetaTv
--- If so, and if tv does not appear in 'rhs', set tv := rhs
--- bind the evidence (which should be a CtWanted) to Refl<rhs>
--- and return True.  Otherwise return False
-tryFill dflags tv rhs ev
+tryFill :: DynFlags -> EqRel -> TcTyVar -> TcType -> CtEvidence -> TcS Bool
+-- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv
+-- If tv does not appear in 'rhs', it set tv := rhs,
+-- binds the evidence (which should be a CtWanted) to Refl<rhs>
+-- and return True.  Otherwise returns False
+tryFill dflags eq_rel tv rhs ev
   = ASSERT2( not (isGiven ev), ppr ev )
-    do { is_filled <- isFilledMetaTyVar tv
-       ; if is_filled then return False else
     do { rhs' <- zonkTcType rhs
-       ; case occurCheckExpand dflags tv rhs' of
-           OC_OK rhs''    -- Normal case: fill the tyvar
-             -> do { setEvBindIfWanted ev
-                               (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
-                   ; unifyTyVar tv rhs''
-                   ; return True }
-
-           _ ->  -- Occurs check
-                 return False } }
+       ; case tcGetTyVar_maybe rhs' of {
+            Just tv' | tv == tv' -> do { setReflEvidence ev eq_rel rhs
+                                       ; return True } ;
+            _other -> 
+    case occurCheckExpand dflags tv rhs' of
+      OC_OK rhs''    -- Normal case: fill the tyvar
+        -> do { setReflEvidence ev eq_rel rhs''
+              ; unifyTyVar tv rhs''
+              ; return True }
+
+      _ ->  -- Occurs check
+            return False } }
+
+setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS ()
+setReflEvidence ev eq_rel rhs
+  = setEvBindIfWanted ev (EvCoercion refl_co)
+  where
+    refl_co = mkTcReflCo (eqRelRole eq_rel) rhs
 
 {-
 Note [Unflatten using funeqs first]
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 298bbb2dc9..3ad4aa8e0f 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -182,7 +182,8 @@ solveSimpleWanteds simples
 
           ; if unif_count == 0 && not rerun_plugin
             then return (n, wc2)             -- Done
-            else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
+            else do { traceTcS "solveSimple going round again:" $
+                      ppr unif_count $$ ppr rerun_plugin
                     ; go (n+1) limit wc2 } }      -- Loop
 
 
@@ -385,19 +386,19 @@ runSolverPipeline pipeline workItem
 
        ; bumpStepCountTcS    -- One step for each constraint processed
        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
-
-       ; final_is <- getTcSInerts
        ; case final_res of
            Stop ev s       -> do { traceFireTcS ev s
+                                 ; final_is <- getTcSInerts
                                  ; traceTcS "End solver pipeline (discharged) }"
                                        (text "inerts =" <+> ppr final_is)
                                  ; return () }
            ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (text "Kept as inert")
+                                 ; addInertCan ct
+                                 ; final_is <- getTcSInerts
                                  ; traceTcS "End solver pipeline (kept as inert) }" $
                                        vcat [ text "final_item =" <+> ppr ct
                                             , pprTvBndrs $ tyCoVarsOfCtList ct
-                                            , text "inerts     =" <+> ppr final_is]
-                                 ; addInertCan ct }
+                                            , text "inerts     =" <+> ppr final_is] }
        }
   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
                      -> TcS (StopOrContinue Ct)
@@ -1389,26 +1390,31 @@ doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
                                      , cc_tyargs = args, cc_fsk = fsk })
+  | fsk `elemVarSet` tyCoVarsOfTypes args
+  = no_reduction
+  | otherwise
   = do { match_res <- matchFam fam_tc args
                            -- Look up in top-level instances, or built-in axiom
                            -- See Note [MATCHING-SYNONYMS]
        ; case match_res of
-           Nothing -> do { improveTopFunEqs (ctEvLoc old_ev) fam_tc args fsk
-                         ; continueWith work_item }
-           Just (ax_co, rhs_ty)
-             -> reduce_top_fun_eq old_ev fsk ax_co rhs_ty }
+           Nothing         -> no_reduction
+           Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
+  where
+    no_reduction = do { improveTopFunEqs (ctEvLoc old_ev) fam_tc args fsk
+                      ; continueWith work_item }
 
 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
 
-reduce_top_fun_eq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType
+reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
                   -> TcS (StopOrContinue Ct)
--- Found an applicable top-level axiom: use it to reduce
-reduce_top_fun_eq old_ev fsk ax_co rhs_ty
+-- We have found an applicable top-level axiom: use it to reduce
+reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
   | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
   , isTypeFamilyTyCon tc
   , tc_args `lengthIs` tyConArity tc    -- Short-cut
-  = shortCutReduction old_ev fsk ax_co tc tc_args
-       -- Try shortcut; see Note [Short cut for top-level reaction]
+  = -- RHS is another type-family application
+    -- Try shortcut; see Note [Short cut for top-level reaction]
+    shortCutReduction old_ev fsk ax_co tc tc_args
 
   | isGiven old_ev  -- Not shortcut
   = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
@@ -1419,39 +1425,51 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
        ; stopWith old_ev "Fun/Top (given)" }
 
   -- So old_ev is Wanted or Derived
-  | not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
+--  | not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
+  | otherwise
   = do { dischargeFmv old_ev fsk ax_co rhs_ty
        ; traceTcS "doTopReactFunEq" $
          vcat [ text "old_ev:" <+> ppr old_ev
               , nest 2 (text ":=") <+> ppr ax_co ]
        ; stopWith old_ev "Fun/Top (wanted)" }
 
-  | otherwise -- We must not assign ufsk := ...ufsk...!
+{-
+  | otherwise -- We must not assign fuv := ...fuv...!
+              -- We have fuv ~ rhs_ty, but 'fuv' occurs in rhs_ty
+              -- So we do  fuv := alpha, and emit the
   = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
+
        ; new_ev <- case old_ev of
            CtWanted {}  -> do { (ev, _) <- newWantedEq loc Nominal alpha_ty rhs_ty
-                              ; updWorkListTcS $
-                                  extendWorkListEq (mkNonCanonical ev)
+--                              ; updWorkListTcS $
+--                                extendWorkListEq (mkNonCanonical ev)
                               ; return ev }
-           CtDerived {} -> do { ev <- newDerivedNC loc pred
-                              ; updWorkListTcS (extendWorkListDerived loc ev)
+           CtDerived {} -> do { let pred = mkPrimEqPred alpha_ty rhs_ty
+	                      ; ev <- newDerivedNC loc pred
+--                              ; updWorkListTcS (extendWorkListDerived loc ev)
                               ; return ev }
-             where pred = mkPrimEqPred alpha_ty rhs_ty
            _ -> pprPanic "reduce_top_fun_eq" (ppr old_ev)
 
+       ; updInertIrreds (mkNonCanonical new_ev `consCts`)
+
             -- By emitting this as non-canonical, we deal with all
             -- flattening, occurs-check, and ufsk := ufsk issues
        ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
+            --   old_ev :: fam_tc args ~ fmv
             --    ax_co :: fam_tc args ~ rhs_ty
-            --       ev :: alpha ~ rhs_ty
-            --     ufsk := alpha
+            --   new_ev :: alpha ~ rhs_ty
             -- final_co :: fam_tc args ~ alpha
+            --
+            --     fmv := alpha
        ; dischargeFmv old_ev fsk final_co alpha_ty
        ; traceTcS "doTopReactFunEq (occurs)" $
          vcat [ text "old_ev:" <+> ppr old_ev
-              , nest 2 (text ":=") <+> ppr final_co
+              , ppUnless (isDerived old_ev) $
+                   -- No evidence for derived constraints
+                nest 2 (text ":=") <+> ppr final_co
               , text "new_ev:" <+> ppr new_ev ]
        ; stopWith old_ev "Fun/Top (wanted)" }
+-}
   where
     loc = ctEvLoc old_ev
     deeper_loc = bumpCtLocDepth loc
@@ -1570,10 +1588,10 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 -- (dischargeFmv x fmv co ty)
 --     [W] ev :: F tys ~ fmv
 --         co :: F tys ~ xi
--- Precondition: fmv is not filled, and fuv `notElem` xi
+-- Precondition: fmv is not filled, and fmv `notElem` xi
 --
 -- Then set fmv := xi,
---      set ev := co
+--      set ev  := co
 --      kick out any inert things that are now rewritable
 --
 -- Does not evaluate 'co' if 'ev' is Derived
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 61b00f3727..7ed18a0acd 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1455,7 +1455,8 @@ data Ct
       cc_tyvar  :: TcTyVar,
       cc_rhs    :: TcType,     -- Not necessarily function-free (hence not Xi)
                                -- See invariants above
-      cc_eq_rel :: EqRel
+
+      cc_eq_rel :: EqRel       -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev
     }
 
   | CFunEqCan {  -- F xis ~ fsk
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 687168bfa1..fafd556d04 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -1113,7 +1113,7 @@ Note [Adding an inert canonical constraint the InertCans]
         (respecting flavours) by the new constraint. This is done
         by kickOutRewritable.
 
-    (B) Applies only to nominal equalities: a ~ ty.  Four cases:
+    (B) Applies only to Nominal equalities: a ~ ty.  Four cases:
 
         [Representational]   [G/W/D] a ~R ty:
           Just add it to inert_eqs
@@ -1131,6 +1131,11 @@ Note [Adding an inert canonical constraint the InertCans]
                Reason for (b) if the model can rewrite c, then we have already
                generated a shadow copy
 
+              Reason for doing this at all: class or fun-eq constraints may be
+	      rewritten and fundeps may then give rise to new equalities.
+	      An Irred constraint might be rewritten to a class constraint
+	      that has superclasses or fundeps
+
        [Given/Wanted Nominal]  [G/W] a ~N ty:
           1. Add it to inert_eqs
           2. Emit [D] a~ty
@@ -1237,28 +1242,23 @@ add_inert_eq ics@(IC { inert_count = n
 add_inert_eq _ ct = pprPanic "addInertEq" (ppr ct)
 
 emitDerivedShadows :: InertCans -> TcTyVar -> TcS ()
-emitDerivedShadows IC { inert_eqs      = tv_eqs
-                      , inert_dicts    = dicts
+emitDerivedShadows IC { inert_dicts    = dicts
+                      -- , inert_eqs      = tv_eqs
                       , inert_safehask = safehask
                       , inert_funeqs   = funeqs
                       , inert_irreds   = irreds
                       , inert_model    = model } new_tv
-  | null shadows
-  = return ()
-  | otherwise
-  = do { traceTcS "Emit derived shadows:" $
-         vcat [ text "tyvar =" <+> ppr new_tv
-              , text "shadows =" <+> vcat (map ppr shadows) ]
-       ; emitWork shadows }
+  = emitShadows shadows
   where
     shadows = foldDicts  get_ct dicts    $
               foldDicts  get_ct safehask $
               foldFunEqs get_ct funeqs   $
               foldIrreds get_ct irreds   $
-              foldTyEqs  get_ct tv_eqs []
+              []   -- For tyvar eqs we always have a shadow already
+--              foldTyEqs  get_ct tv_eqs []
       -- Ignore insolubles
 
-    get_ct ct cts | want_shadow ct = mkShadowCt ct : cts
+    get_ct ct cts | want_shadow ct = ct : cts
                   | otherwise      = cts
 
     want_shadow ct
@@ -1270,15 +1270,43 @@ emitDerivedShadows IC { inert_eqs      = tv_eqs
       where
         rw_tvs = rewritableTyCoVars ct
 
-mkShadowCt :: Ct -> Ct
+emitShadows :: [Ct] -> TcS ()
+emitShadows cts
+  | null cts
+  = return ()
+  | otherwise
+  = do { shadows <- concatMapM mkShadowCt cts
+       ; traceTcS "Emitting shadows:" (vcat (map ppr shadows))
+       ; updWorkListTcS (extendWorkListCts shadows) }
+
+mkShadowCt :: Ct -> TcS [Ct]
 -- Produce a Derived shadow constraint from the input
 -- If it is a CFunEqCan, make it NonCanonical, to avoid
 --   duplicating the flatten-skolems
 -- Otherwise keep the canonical shape.  This just saves work, but
 -- is sometimes important; see Note [Keep CDictCan shadows as CDictCan]
+mkShadowCt ct@(CFunEqCan { cc_ev = ev, cc_fun = tc
+                         , cc_tyargs = xis, cc_fsk = old_fmv })
+  = do { let fam_ty = mkTyConApp tc xis
+             loc    = ctEvLoc ev
+       ; new_fmv <- newFmv fam_ty
+       ; let old_fmv_ty = mkTyVarTy old_fmv
+             new_fmv_ty = mkTyVarTy new_fmv
+             eq_pred = mkPrimEqPred fam_ty     new_fmv_ty
+             tv_eq   = mkPrimEqPred new_fmv_ty old_fmv_ty
+             der_fun_eq_ev = CtDerived { ctev_pred = eq_pred, ctev_loc = loc }
+             der_tv_eq_ev  = CtDerived { ctev_pred = tv_eq,   ctev_loc = loc }
+
+       ; return [ CTyEqCan { cc_ev     = der_tv_eq_ev
+                           , cc_tyvar  = old_fmv
+                           , cc_rhs    = new_fmv_ty
+                           , cc_eq_rel = NomEq }
+
+                , ct { cc_ev  = der_fun_eq_ev
+                     , cc_fsk = new_fmv } ] }
+
 mkShadowCt ct
-  | CFunEqCan {} <- ct = CNonCanonical { cc_ev = derived_ev }
-  | otherwise          = ct { cc_ev = derived_ev }
+  = return [ct { cc_ev = derived_ev }]
   where
     ev = ctEvidence ct
     derived_ev = CtDerived { ctev_pred = ctEvPred ev
@@ -1326,7 +1354,7 @@ rewritableTyCoVars ct                              = tyCoVarsOfType (ctPred ct)
 addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
 addInertCan ct
   = do { traceTcS "insertInertCan {" $
-         text "Trying to insert new inert item:" <+> ppr ct
+         text "Trying to insert new non-eq inert item:" <+> ppr ct
 
        ; ics <- getInertCans
        ; setInertCans (add_item ics ct)
@@ -1335,7 +1363,7 @@ addInertCan ct
        -- See Note [Emitting shadow constraints]
        ; let rw_tvs = rewritableTyCoVars ct
        ; when (not (isDerivedCt ct) && modelCanRewrite (inert_model ics) rw_tvs)
-              (emitWork [mkShadowCt ct])
+              (emitShadows [ct])
 
        ; traceTcS "addInertCan }" $ empty }
 
diff --git a/testsuite/tests/indexed-types/should_fail/T1897b.stderr b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
index b83c7ffe78..53d4a49d53 100644
--- a/testsuite/tests/indexed-types/should_fail/T1897b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
@@ -9,5 +9,5 @@ T1897b.hs:16:1: error:
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
         isValid :: forall a (t :: * -> *).
-                   (Bug a, Foldable t) =>
+                   (Foldable t, Bug a) =>
                    t (Depend a) -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 6375c8f79e..8154a301c0 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,24 +1,12 @@
 
-T2544.hs:17:18: error:
-    • Couldn't match type ‘IxMap i0’ with ‘IxMap l’
-      Expected type: IxMap l [Int]
-        Actual type: IxMap i0 [Int]
+T2544.hs:17:12: error:
+    • Couldn't match type ‘IxMap r’ with ‘IxMap i0’
+      Expected type: IxMap (l :|: r) [Int]
+        Actual type: BiApp (IxMap i1) (IxMap i0) [Int]
       NB: ‘IxMap’ is a type function, and may not be injective
       The type variable ‘i0’ is ambiguous
-    • In the first argument of ‘BiApp’, namely ‘empty’
-      In the expression: BiApp empty empty
-      In an equation for ‘empty’: empty = BiApp empty empty
-    • Relevant bindings include
-        empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
-
-T2544.hs:17:24: error:
-    • Couldn't match type ‘IxMap i1’ with ‘IxMap r’
-      Expected type: IxMap r [Int]
-        Actual type: IxMap i1 [Int]
-      NB: ‘IxMap’ is a type function, and may not be injective
-      The type variable ‘i1’ is ambiguous
-    • In the second argument of ‘BiApp’, namely ‘empty’
-      In the expression: BiApp empty empty
+    • In the expression: BiApp empty empty
       In an equation for ‘empty’: empty = BiApp empty empty
+      In the instance declaration for ‘Ix (l :|: r)’
     • Relevant bindings include
         empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.stderr b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
index 11e1b8e8fd..63f11b97f1 100644
--- a/testsuite/tests/indexed-types/should_fail/T2627b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
@@ -1,9 +1,9 @@
 
 T2627b.hs:20:24: error:
     • Occurs check: cannot construct the infinite type:
-        t0 ~ Dual (Dual t0)
+        b0 ~ Dual (Dual b0)
         arising from a use of ‘conn’
-      The type variable ‘t0’ is ambiguous
+      The type variable ‘b0’ is ambiguous
     • In the expression: conn undefined undefined
       In an equation for ‘conn’:
           conn (Rd k) (Wr a r) = conn undefined undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
index 8526c17f5e..829bca1400 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -3,14 +3,14 @@ T3330c.hs:23:43: error:
     • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
         f1 :: * -> *
-        Der f1 x :: *
-      Expected type: Der ((->) x) (Der f1 x)
+        f1 x :: *
+      Expected type: Der ((->) x) (f1 x)
         Actual type: R f1
     • In the first argument of ‘plug’, namely ‘rf’
       In the first argument of ‘Inl’, namely ‘(plug rf df x)’
       In the expression: Inl (plug rf df x)
     • Relevant bindings include
         x :: x (bound at T3330c.hs:23:29)
-        df :: Der f1 x (bound at T3330c.hs:23:25)
+        df :: f1 x (bound at T3330c.hs:23:25)
         rf :: R f1 (bound at T3330c.hs:23:13)
         plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:23:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T6123.stderr b/testsuite/tests/indexed-types/should_fail/T6123.stderr
index 3c77040f95..0ae1a5e3c1 100644
--- a/testsuite/tests/indexed-types/should_fail/T6123.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T6123.stderr
@@ -1,9 +1,9 @@
 
 T6123.hs:10:14: error:
-    • Occurs check: cannot construct the infinite type: t0 ~ Id t0
+    • Occurs check: cannot construct the infinite type: a0 ~ Id a0
         arising from a use of ‘cid’
-      The type variable ‘t0’ is ambiguous
+      The type variable ‘a0’ is ambiguous
     • In the expression: cid undefined
       In an equation for ‘cundefined’: cundefined = cid undefined
     • Relevant bindings include
-        cundefined :: t0 (bound at T6123.hs:10:1)
+        cundefined :: a0 (bound at T6123.hs:10:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T7786.hs b/testsuite/tests/indexed-types/should_fail/T7786.hs
index 839a1fb83d..08961b2a68 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.hs
+++ b/testsuite/tests/indexed-types/should_fail/T7786.hs
@@ -82,9 +82,23 @@ foo :: Database inv
 foo db k sub = buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db
 -}
 
+foogle :: Database inv
+       -> Sing post
+       -> Database sub
+       -> Maybe (Sing (Intersect (BuriedUnder sub post 'Empty) inv))
+
+foogle db k sub = return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+
+
+addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
+addSub db k sub = do Nil :: Sing xxx <- foogle db k sub
+                     return $ Sub db k sub
+
+{-
 addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
-addSub db k sub = do Nil :: Sing xxx <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+addSub db k sub = do Nil :: Sing xxx <- foogle db sub k
                      -- Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
                      -- Nil :: Sing Empty <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
                      -- Nil <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
                      return $ Sub db k sub
+-}
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T7786.stderr b/testsuite/tests/indexed-types/should_fail/T7786.stderr
index ca3e9ecbda..8fdb49bd8e 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7786.stderr
@@ -1,29 +1,29 @@
 
-T7786.hs:86:49: error:
+T7786.hs:94:41: error:
     • Couldn't match type ‘xxx’
                      with ‘Intersect (BuriedUnder sub k 'Empty) inv’
-      Expected type: Sing xxx
-        Actual type: Sing (Intersect (BuriedUnder sub k 'Empty) inv)
-    • In the first argument of ‘return’, namely
-        ‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’
-      In a stmt of a 'do' block:
-        Nil :: Sing xxx <- return
-                             (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+      Expected type: Maybe (Sing xxx)
+        Actual type: Maybe
+                       (Sing (Intersect (BuriedUnder sub k 'Empty) inv))
+    • In a stmt of a 'do' block: Nil :: Sing xxx <- foogle db k sub
       In the expression:
-        do { Nil :: Sing xxx <- return
-                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
+        do { Nil :: Sing xxx <- foogle db k sub;
              return $ Sub db k sub }
+      In an equation for ‘addSub’:
+          addSub db k sub
+            = do { Nil :: Sing xxx <- foogle db k sub;
+                   return $ Sub db k sub }
     • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:86:13)
-        k :: Sing k (bound at T7786.hs:86:11)
-        db :: Database inv (bound at T7786.hs:86:8)
+        sub :: Database sub (bound at T7786.hs:94:13)
+        k :: Sing k (bound at T7786.hs:94:11)
+        db :: Database inv (bound at T7786.hs:94:8)
         addSub :: Database inv
                   -> Sing k
                   -> Database sub
                   -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:86:1)
+          (bound at T7786.hs:94:1)
 
-T7786.hs:90:31: error:
+T7786.hs:95:31: error:
     • Could not deduce: Intersect (BuriedUnder sub k 'Empty) inv
                         ~
                         'Empty
@@ -32,19 +32,18 @@ T7786.hs:90:31: error:
         bound by a pattern with constructor: Nil :: forall a. Sing 'Empty,
                  in a pattern binding in
                       'do' block
-        at T7786.hs:86:22-24
+        at T7786.hs:94:22-24
     • In the second argument of ‘($)’, namely ‘Sub db k sub’
       In a stmt of a 'do' block: return $ Sub db k sub
       In the expression:
-        do { Nil :: Sing xxx <- return
-                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
+        do { Nil :: Sing xxx <- foogle db k sub;
              return $ Sub db k sub }
     • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:86:13)
-        k :: Sing k (bound at T7786.hs:86:11)
-        db :: Database inv (bound at T7786.hs:86:8)
+        sub :: Database sub (bound at T7786.hs:94:13)
+        k :: Sing k (bound at T7786.hs:94:11)
+        db :: Database inv (bound at T7786.hs:94:8)
         addSub :: Database inv
                   -> Sing k
                   -> Database sub
                   -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:86:1)
+          (bound at T7786.hs:94:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr
index 6dec5d0191..697c9c3231 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -1,10 +1,9 @@
 
-T8227.hs:16:44: error:
-    • Couldn't match expected type ‘Scalar (V (Scalar (V a)))’
-                  with actual type ‘Scalar (V a)’
-      NB: ‘Scalar’ is a type function, and may not be injective
-    • In the first argument of ‘arcLengthToParam’, namely ‘eps’
-      In the expression: arcLengthToParam eps eps
+T8227.hs:16:27: error:
+    • Couldn't match expected type ‘Scalar (V a)’
+                  with actual type ‘Scalar (V (Scalar (V a)))
+                                    -> Scalar (V (Scalar (V a)))’
+    • In the expression: arcLengthToParam eps eps
       In an equation for ‘absoluteToParam’:
           absoluteToParam eps seg = arcLengthToParam eps eps
     • Relevant bindings include
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 3c8cbdabf9..0a237d8270 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -583,7 +583,7 @@ test('T5837',
              # 2014-12-08: 115905208  Constraint solver perf improvements (esp kick-out)
              # 2016-04-06: 24199320  (x86/Linux, 64-bit machine) TypeInType
 
-           (wordsize(64), 48507272, 10)])
+           (wordsize(64), 61640208, 10)])
              # sample: 3926235424 (amd64/Linux, 15/2/2012)
              # 2012-10-02 81879216
              # 2012-09-20 87254264 amd64/Linux
@@ -602,8 +602,11 @@ test('T5837',
              # 2015-12-11 43877520  amd64/Linux, TypeInType (see #11196)
              # 2016-03-18 48507272  Mac, accept small regression in exchange
              #                           for other optimisations
+             # 2016-08-29 61640208 New constraint solver /succeeds/ on this code
+             #                           so program goes through whole pipeline
+             #                           so allocation legitimately increases
       ],
-      compile_fail,['-freduction-depth=50'])
+      compile,['-freduction-depth=50'])
 
 test('T6048',
      [ only_ways(['optasm']),
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.hs b/testsuite/tests/typecheck/should_fail/ContextStack2.hs
index f3f93eb912..d66103c880 100644
--- a/testsuite/tests/typecheck/should_fail/ContextStack2.hs
+++ b/testsuite/tests/typecheck/should_fail/ContextStack2.hs
@@ -5,6 +5,8 @@ module ContextStack2 where
 type family TF a :: *
 type instance TF (a,b) = (TF a, TF b)
 
+-- Succeeds with new approach to fuvs
+-- Aug 2016
 t :: (a ~ TF (a,Int)) => Int
 t = undefined
 
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr b/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
deleted file mode 100644
index f76d1f486c..0000000000
--- a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
+++ /dev/null
@@ -1,13 +0,0 @@
-
-ContextStack2.hs:8:6: error:
-    • 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 ‘t’
-      In the type signature:
-        t :: (a ~ TF (a, Int)) => Int
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index 62385ea1df..ed02c075e3 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,22 +1,23 @@
 
 T5853.hs:15:46: error:
-    • Could not deduce: Subst (Subst t2 t) t1 ~ Subst t2 t1
+    • Could not deduce: Subst fa (Elem fb) ~ fb
         arising from a use of ‘<$>’
-      from the context: (F t2,
-                         Elem t2 ~ Elem t2,
-                         Elem (Subst t2 t1) ~ t1,
-                         Subst t2 t1 ~ Subst t2 t1,
-                         Subst (Subst t2 t1) (Elem t2) ~ t2,
-                         F (Subst t2 t),
-                         Elem (Subst t2 t) ~ t,
-                         Elem t2 ~ Elem t2,
-                         Subst (Subst t2 t) (Elem t2) ~ t2,
-                         Subst t2 t ~ Subst t2 t)
+      from the context: (F (Subst fb a),
+                         Elem (Subst fb a) ~ a,
+                         Elem fb ~ Elem fb,
+                         Subst (Subst fb a) (Elem fb) ~ fb,
+                         Subst fb a ~ Subst fb a,
+                         F fa,
+                         Elem fa ~ Elem fa,
+                         Elem (Subst fb a) ~ a,
+                         Subst fa a ~ Subst fb a,
+                         Subst (Subst fb a) (Elem fa) ~ fa)
         bound by the RULE "map/map" at T5853.hs:15:2-57
-      NB: ‘Subst’ is a type function, and may not be injective
+      ‘fb’ is a rigid type variable bound by
+        the RULE "map/map" at T5853.hs:15:2-57
     • In the expression: (f . g) <$> xs
       When checking the transformation rule "map/map"
     • Relevant bindings include
-        f :: Elem t2 -> t1 (bound at T5853.hs:15:19)
-        g :: t -> Elem t2 (bound at T5853.hs:15:21)
-        xs :: Subst t2 t (bound at T5853.hs:15:23)
+        f :: a -> Elem fb (bound at T5853.hs:15:19)
+        g :: Elem fa -> a (bound at T5853.hs:15:21)
+        xs :: fa (bound at T5853.hs:15:23)
diff --git a/testsuite/tests/typecheck/should_fail/T8883.stderr b/testsuite/tests/typecheck/should_fail/T8883.stderr
index 25fd7c06a0..22856e29cf 100644
--- a/testsuite/tests/typecheck/should_fail/T8883.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8883.stderr
@@ -4,5 +4,5 @@ T8883.hs:20:1: error:
       (Use FlexibleContexts to permit this)
     • When checking the inferred type
         fold :: forall b a.
-                (Regular a, Functor (PF a)) =>
+                (Functor (PF a), Regular a) =>
                 (PF a b -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_fail/T9260.stderr b/testsuite/tests/typecheck/should_fail/T9260.stderr
index 0773da2bf5..f55f474904 100644
--- a/testsuite/tests/typecheck/should_fail/T9260.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9260.stderr
@@ -1,7 +1,8 @@
 
-T9260.hs:12:8: error:
-    • Couldn't match type ‘2’ with ‘1’
-      Expected type: Fin 1
-        Actual type: Fin (1 + 1)
-    • In the expression: Fsucc Fzero
+T9260.hs:12:14: error:
+    • Couldn't match type ‘1’ with ‘0’
+      Expected type: Fin 0
+        Actual type: Fin (0 + 1)
+    • In the first argument of ‘Fsucc’, namely ‘Fzero’
+      In the expression: Fsucc Fzero
       In an equation for ‘test’: test = Fsucc Fzero
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index dda2a7d1c8..80409dda60 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -340,7 +340,7 @@ test('T8428', normal, compile_fail, [''])
 test('T8450', normal, compile_fail, [''])
 test('T8514', normal, compile_fail, [''])
 test('ContextStack1', normal, compile_fail, ['-freduction-depth=10'])
-test('ContextStack2', normal, compile_fail, ['-freduction-depth=10'])
+test('ContextStack2', normal, compile, [''])
 test('T8570', extra_clean(['T85570a.o', 'T8570a.hi','T85570b.o', 'T8570b.hi']),
      multimod_compile_fail, ['T8570', '-v0'])
 test('T8603', normal, compile_fail, [''])