Another major constraint-solver refactoring

This patch takes further my refactoring of the constraint
solver, which I've been doing over the last couple of months
in consultation with Richard.

It fixes a number of tricky bugs that made the constraint
solver actually go into a loop, including

  Trac #12526
  Trac #12444
  Trac #12538

The main changes are these

* Flatten unification variables (fmvs/fuvs) appear on the LHS
  of a tvar/tyvar equality; thus
           fmv ~ alpha
  and not
           alpha ~ fmv

  See Note [Put flatten unification variables on the left]
  in TcUnify.  This is implemented by TcUnify.swapOverTyVars.

* Don't reduce a "loopy" CFunEqCan where the fsk appears on
  the LHS:
      F t1 .. tn ~ fsk
  where 'fsk' is free in t1..tn.
  See Note [FunEq occurs-check principle] in TcInteract

  This neatly stops some infinite loops that people reported;
  and it allows us to delete some crufty code in reduce_top_fun_eq.
  And it appears to be no loss whatsoever.

  As well as fixing loops, ContextStack2 and T5837 both terminate
  when they didn't before.

* Previously we generated "derived shadow" constraints from
  Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
  generate a derived shadow from the same Wanted.

  A big change in this patch is to have two kinds of Wanteds:
     [WD] behaves like a pair of a Wanted and a Derived
     [W]  behaves like a Wanted only
  See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
  field of a Wanted.

  This turned out to be a lot simpler.  A [WD] gets split into a
  [W] and a [D] in TcSMonad.maybeEmitShaodow.

  See TcSMonad Note [The improvement story and derived shadows]

* Rather than have a separate inert_model in the InertCans, I've
  put the derived equalities back into inert_eqs.  We weren't
  gaining anything from a separate field.

* Previously we had a mode for the constraint solver in which it
  would more aggressively solve Derived constraints; it was used
  for simplifying the context of a 'deriving' clause, or a 'default'
  delcaration, for example.

  But the complexity wasn't worth it; now I just make proper Wanted
  constraints.  See TcMType.cloneWC

* Don't generate injectivity improvement for Givens; see
  Note [No FunEq improvement for Givens] in TcInteract

* solveSimpleWanteds leaves the insolubles in-place rather than
  returning them.  Simpler.

I also did lots of work on comments, including fixing Trac #12821.

35 files changed, 500 insertions, 228 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T10226.hs b/testsuite/tests/indexed-types/should_compile/T10226.hs
index 14d3a3eb31..77ce29a69d 100644
--- a/testsuite/tests/indexed-types/should_compile/T10226.hs
+++ b/testsuite/tests/indexed-types/should_compile/T10226.hs
@@ -42,6 +42,30 @@ showFromF fa = undefined
 showFromF' :: (Show (FInv b), F (FInv b) ~ b) => b -> String
 showFromF' = showFromF
 
+{- [G] F (FInv b) ~ b
+   [W] FInv (F alpha) ~ alpha
+   [W] F alpha ~ b
+-->
+   [G] g1: FInv b ~ fsk1
+   [G] g2: F fsk1 ~ fsk2
+   [G} g3: fsk2 ~ b
+
+   [W] F alpha ~ fmv1
+   [W] FInv fmv1 ~ fmv2
+   [W] fmv2 ~ alpha
+   [W] fmv1 ~ b
+
+   [D] d1: F alpha ~ fmv1
+   [D] d2: FInv fmv1 ~ fmv2
+   [D] d3: fmv2 ~ alpha
+   [D] d4: fmv1 ~ b
+
+--> d2 + d4: [D] FInv b ~ fmv2
+       + g1: [D] fmv2 ~ b
+--> d3: b ~ alpha, and we are done
+
+-}
+
 {-------------------------------------------------------------------------------
   In 7.10 the definition of showFromF' is not accepted, but it gets stranger.
   In 7.10 we cannot _call_ showFromF at all, even at a concrete type. Below
@@ -57,3 +81,36 @@ type instance FInv Int = Int
 
 test :: String
 test = showFromF (0 :: Int)
+
+{-
+
+  [WD] FInv (F alpha) ~ alpha
+  [WD] F alpha ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+* [WD] FInv fuv0 ~ fuv1
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+  [W] FInv fuv0 ~ fuv1
+*  [D] FInv Int ~ fuv1
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+  [W] FInv fuv0 ~ fuv1
+* [D] fuv1 ~ Int
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+
+-->
+  [WD] F alpha ~ fuv0
+  [W] FInv fuv0 ~ fuv1
+  [D] alpha := Int
+  [WD] fuv1 ~ alpha
+  [WD] fuv0 ~ Int
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/T10634.hs b/testsuite/tests/indexed-types/should_compile/T10634.hs
index f02cf810da..0b52ef534a 100644
--- a/testsuite/tests/indexed-types/should_compile/T10634.hs
+++ b/testsuite/tests/indexed-types/should_compile/T10634.hs
@@ -21,3 +21,18 @@ instance Convert Int32 where
 
 x :: Int8
 x = down 8
+
+{- From x = down 8
+
+[WD] Num alpha
+[WD] Convert alpha
+[WD] Down alpha ~ Int8
+
+--> superclasses
+[D] Up (Down alpha) ~ alpha
+
+--> substitute (Down alpha ~ Int8)
+[D] Up Int8 ~ alpha
+
+--> alpha := Int16
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/T12526.hs b/testsuite/tests/indexed-types/should_compile/T12526.hs
new file mode 100644
index 0000000000..35a653a544
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T12526.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE TypeFamilies, MonoLocalBinds #-}
+module T12526 where
+
+type family P (s :: * -> *) :: * -> * -> *
+type instance P Signal = Causal
+
+type family S (p :: * -> * -> *) :: * -> *
+type instance S Causal = Signal
+
+class (P (S p) ~ p) => CP p
+instance CP Causal
+
+data Signal a = Signal
+data Causal a b = Causal
+
+shapeModOsci :: CP p => p Float Float
+shapeModOsci = undefined
+
+f :: Causal Float Float -> Bool
+f = undefined
+
+-- This fails
+ping :: Bool
+ping = let osci = shapeModOsci in  f osci
+
+
+-- This works
+-- ping :: Bool
+-- ping = f shapeModOsci
+
+
+{-
+
+    osci :: p Float Float
+    [W] CP p, [D] P (S p) ~ p
+-->
+    [W] CP p, [D] P fuv1 ~ fuv2, S p ~ fuv1, fuv2 ~ p
+-->
+    p := fuv2
+    [W] CP fuv2, [D] P fuv1 ~ fuv2, S fuv2 ~ fuv1
+
+-}
+
+-- P (S p) ~ p
+-- p Float Float ~ Causal Float Float
+
+
+{-
+  P (S p) ~ p
+  p Float Float ~ Causal Float Float
+
+--->
+  S p ~ fuv1    (FunEq)
+  P fuv1 ~ fuv2 (FunEq)
+  fuv2 ~ p
+  p F F ~ Causal F F
+
+--->
+  p := fuv2
+
+  fuv2 ~ Causal
+  S fuv2 ~ fuv1 (FunEq)
+  P fuv1 ~ fuv2 (FunEq)
+
+---> unflatten
+  fuv1 := S fuv2
+  fuv2 := Causal
+
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/T12538.hs b/testsuite/tests/indexed-types/should_compile/T12538.hs
new file mode 100644
index 0000000000..9aff36e47d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T12538.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T12538 where
+
+data Tagged t a = Tagged a
+
+type family Tag a where
+  Tag (Tagged t a) = Tagged t a
+  Tag a = Tagged Int a
+
+class (r ~ Tag a) => TagImpl a r | a -> r where
+  tag :: a -> r
+
+instance {-# OVERLAPPING #-} (r ~ Tag (Tagged t a)) => TagImpl (Tagged t a) r where
+  tag = id
+
+#ifdef WRONG
+instance {-# OVERLAPPING #-} (r ~ Tagged t a, r ~ Tag a) => TagImpl a r where
+#else
+instance {-# OVERLAPPING #-} (r ~ Tagged Int a, r ~ Tag a) => TagImpl a r where
+#endif
+  tag = Tagged @Int
+
+data family   DF x
+data instance DF (Tagged t a) = DF (Tagged t a)
+
+class ToDF a b | a -> b where
+  df :: a -> b
+
+instance (TagImpl a a', b ~ DF a') => ToDF a b where
+  df = DF . tag
+
+main :: IO ()
+main = pure ()
diff --git a/testsuite/tests/indexed-types/should_compile/T12538.stderr b/testsuite/tests/indexed-types/should_compile/T12538.stderr
new file mode 100644
index 0000000000..ca106246e7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T12538.stderr
@@ -0,0 +1,13 @@
+
+T12538.hs:37:8: error:
+    • Could not deduce: a' ~ Tagged Int a
+      from the context: (TagImpl a a', b ~ DF a')
+        bound by the instance declaration at T12538.hs:36:10-46
+      ‘a'’ is a rigid type variable bound by
+        the instance declaration at T12538.hs:36:10-46
+      Expected type: a -> b
+        Actual type: a -> DF (Tagged Int a)
+    • In the expression: DF . tag
+      In an equation for ‘df’: df = DF . tag
+      In the instance declaration for ‘ToDF a b’
+    • Relevant bindings include df :: a -> b (bound at T12538.hs:37:3)
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
index 29877bf2aa..b11c95eb6c 100644
--- a/testsuite/tests/indexed-types/should_compile/T3017.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   insert :: forall c. Coll c => Elem c -> c -> c
   test2 ::
-    forall a b c. (Elem c ~ (a, b), Coll c, Num a, Num b) => c -> c
+    forall a b c. (Elem c ~ (a, b), Num b, Num a, Coll c) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c :: * open
diff --git a/testsuite/tests/indexed-types/should_compile/T4338.hs b/testsuite/tests/indexed-types/should_compile/T4338.hs
index 6fa2ae85ac..64e224e11d 100644
--- a/testsuite/tests/indexed-types/should_compile/T4338.hs
+++ b/testsuite/tests/indexed-types/should_compile/T4338.hs
@@ -17,7 +17,40 @@ instance Foo Char Int where
      tickle = (+1)
 
 test :: (Foo a b) => a -> a
-test = back . tickle . there
+test x = back (tickle (there x))
 
 main :: IO ()
 main = print $ test 'F'
+
+{-
+
+[G] Foo a b
+[G] There a ~ b
+[G] Back b ~ a
+
+[W] Foo a beta      -- from 'there'
+[W] Foo alpha beta  -- from tickle
+[W] Foo a beta      -- from back
+
+[D] There a ~ beta
+[D] Back beta ~ a
+
+[D] There alpha ~ beta
+[D] Back beta ~ alpha
+
+
+-- Hence beta = b
+--       alpha = a
+
+
+
+[W] Foo a (There t_a1jL)
+[W] Foo t_a1jL (There t_a1jL)
+[W] Back (There t_a1jL) ~ t_a1jL
+
+[D] There a ~ There t_a1jL
+     hence There t_a1jL ~ b
+[D] Back (There t_a1jL) ~ a
+[D] There t_a1jL ~ There t_a1jL
+[D] Back (There t_a1jL) ~ t_a1jL
+-}
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index b093128a41..eb71a2866e 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -278,3 +278,5 @@ test('T12175', normal, compile, [''])
 test('T12522', normal, compile, [''])
 test('T12522b', normal, compile, [''])
 test('T12676', normal, compile, [''])
+test('T12526', normal, compile, [''])
+test('T12538', normal, compile_fail, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 6375c8f79e..b943db2087 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,4 +1,16 @@
 
+T2544.hs:17:12: error:
+    • Couldn't match type ‘IxMap r’ with ‘IxMap i1’
+      Expected type: IxMap (l :|: r) [Int]
+        Actual type: BiApp (IxMap l) (IxMap i1) [Int]
+      NB: ‘IxMap’ is a type function, and may not be injective
+      The type variable ‘i1’ is ambiguous
+    • 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)
+
 T2544.hs:17:18: error:
     • Couldn't match type ‘IxMap i0’ with ‘IxMap l’
       Expected type: IxMap l [Int]
@@ -10,15 +22,3 @@ T2544.hs:17:18: error:
       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 an equation for ‘empty’: empty = BiApp empty empty
-    • 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/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index 91244c4ce7..516bdf3802 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -1,13 +1,13 @@
 
 T4179.hs:26:16: error:
-    • Couldn't match type ‘A3 (x (A2 (FCon x) -> A3 (FCon x)))’
-                     with ‘A3 (FCon x)’
+    • Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
+                     with ‘A2 (FCon x)’
       Expected type: x (A2 (FCon x) -> A3 (FCon x))
                      -> A2 (FCon x) -> A3 (FCon x)
         Actual type: x (A2 (FCon x) -> A3 (FCon x))
                      -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
                      -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
-      NB: ‘A3’ is a type function, and may not be injective
+      NB: ‘A2’ is a type function, and may not be injective
     • In the first argument of ‘foldDoC’, namely ‘op’
       In the expression: foldDoC op
       In an equation for ‘fCon’: fCon = foldDoC op
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..2a5c7f5983 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.hs
+++ b/testsuite/tests/indexed-types/should_fail/T7786.hs
@@ -55,17 +55,17 @@ type family Intersect (l :: Inventory a) (r :: Inventory a) :: Inventory a where
   Intersect l Empty = Empty
   Intersect (More ls l) r = InterAppend (Intersect ls r) r l
 
-type family InterAppend (l :: Inventory a) 
-                        (r :: Inventory a) 
-                        (one :: a) 
+type family InterAppend (l :: Inventory a)
+                        (r :: Inventory a)
+                        (one :: a)
             :: Inventory a where
   InterAppend acc Empty one = acc
   InterAppend acc (More rs one) one = More acc one
   InterAppend acc (More rs r) one = InterAppend acc rs one
 
-type family BuriedUnder (sub :: Inventory [KeySegment]) 
-                        (post :: [KeySegment]) 
-                        (inv :: Inventory [KeySegment]) 
+type family BuriedUnder (sub :: Inventory [KeySegment])
+                        (post :: [KeySegment])
+                        (inv :: Inventory [KeySegment])
             :: Inventory [KeySegment] where
   BuriedUnder Empty post inv = inv
   BuriedUnder (More ps p) post inv = More ((ps `BuriedUnder` post) inv) (p `Under` post)
@@ -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 <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+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 <- 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
+-}
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..88f4732df1 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -1,10 +1,11 @@
 
-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 type ‘Scalar (V a)’
+                     with ‘Scalar (V a) -> Scalar (V a)’
+      Expected type: Scalar (V a)
+        Actual type: Scalar (V (Scalar (V a) -> Scalar (V a)))
+                     -> Scalar (V (Scalar (V a) -> 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/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 23c059e720..0588c1b5bc 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -60,18 +60,3 @@ T10403.hs:28:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘app2’: app2 = h2 (H . I) (B ())
     • Relevant bindings include
         app2 :: H (B t) (bound at T10403.hs:28:1)
-
-T10403.hs:28:20: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘f0’ with ‘B t’
-        because type variable ‘t’ would escape its scope
-      This (rigid, skolem) type variable is bound by
-        the type signature for:
-          app2 :: H (B t)
-        at T10403.hs:27:1-15
-      Expected type: f0 ()
-        Actual type: B t ()
-    • In the second argument of ‘h2’, namely ‘(B ())’
-      In the expression: h2 (H . I) (B ())
-      In an equation for ‘app2’: app2 = h2 (H . I) (B ())
-    • Relevant bindings include
-        app2 :: H (B t) (bound at T10403.hs:28:1)
diff --git a/testsuite/tests/perf/compiler/T5837.hs b/testsuite/tests/perf/compiler/T5837.hs
index 6ebbd65bd5..0a500fb826 100644
--- a/testsuite/tests/perf/compiler/T5837.hs
+++ b/testsuite/tests/perf/compiler/T5837.hs
@@ -13,26 +13,35 @@ t = undefined
          [G] a ~ TF (a,Int)               -- a = a_am1
 -->
          [G] TF (a,Int) ~ fsk             -- fsk = fsk_am8
+
 inert    [G] fsk ~ a
 
---->
-    [G] fsk ~ (TF a, TF Int)
+---> reduce
+         [G] fsk ~ (TF a, TF Int)
+
 inert    [G] fsk ~ a
 
---->
-    a ~ (TF a, TF Int)
+---> substitute for fsk and flatten
+         [G] TF a ~ fsk1
+         [G] TF Int ~ fsk2
+
 inert    [G] fsk ~ a
+         [G] a ~ (fsk1, fsk2)
 
----> (attempting to flatten (TF a) so that it does not mention a
-         TF a ~ fsk2
-inert    a ~ (fsk2, TF Int)
-inert    fsk ~ (fsk2, TF Int)
+---> (substitute for a in first constraint)
+         TF (fsk1, fsk2) ~ fsk1     (C1)
+         TF Int ~ fsk2
 
----> (substitute for a)
-         TF (fsk2, TF Int) ~ fsk2
 inert    a ~ (fsk2, TF Int)
 inert    fsk ~ (fsk2, TF Int)
 
+
+------- At this point we are stuck because of
+--      the recursion in the first constraint C1
+--      Hooray
+
+-- Before, we reduced C1, which led to a loop
+
 ---> (top-level reduction, re-orient)
          fsk2 ~ (TF fsk2, TF Int)
 inert    a ~ (fsk2, TF Int)
@@ -50,4 +59,4 @@ inert    fsk2 ~ (fsk3, TF Int)
 inert    a   ~ ((fsk3, TF Int), TF Int)
 inert    fsk ~ ((fsk3, TF Int), TF Int)
 
--}
\ No newline at end of file
+-}
diff --git a/testsuite/tests/perf/compiler/T5837.stderr b/testsuite/tests/perf/compiler/T5837.stderr
deleted file mode 100644
index 324e817947..0000000000
--- a/testsuite/tests/perf/compiler/T5837.stderr
+++ /dev/null
@@ -1,91 +0,0 @@
-
-T5837.hs:8:6: error:
-    Reduction stack overflow; size = 51
-    When simplifying the following type:
-      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))))))))))))))))))))))))
-      ~ (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))))))))))))))))))))))))),
-         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))))))))))))))))))))))))))
-    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/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 72c58c7592..7c8f55ab24 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -594,7 +594,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), 41832056, 10)])
+           (wordsize(64), 52597024, 10)])
              # sample: 3926235424 (amd64/Linux, 15/2/2012)
              # 2012-10-02 81879216
              # 2012-09-20 87254264 amd64/Linux
@@ -615,8 +615,11 @@ test('T5837',
              #                           for other optimisations
              # 2016-09-15 42445672  Linux; fixing #12422
              # 2016-09-25 41832056  amd64/Linux, Rework handling of names (D2469)
+             # 2016-10-25 52597024  amd64/Linux, the test now passes (hooray), and so
+             #                          allocates more because it goes right down the
+             #                          compilation pipeline
       ],
-      compile_fail,['-freduction-depth=50'])
+      compile, ['-freduction-depth=50'])
 
 test('T6048',
      [ only_ways(['optasm']),
diff --git a/testsuite/tests/polykinds/T12444.hs b/testsuite/tests/polykinds/T12444.hs
new file mode 100644
index 0000000000..746c6448ef
--- /dev/null
+++ b/testsuite/tests/polykinds/T12444.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T12444 where
+
+data Nat = Zero | Succ Nat
+
+data SNat (n :: Nat) where
+  SZero :: SNat Zero
+  SSucc :: SNat n -> SNat (Succ n)
+
+type family (:+:) (a :: Nat) (b :: Nat) :: Nat where
+  m :+: Zero = m
+  m :+: (Succ n) = Succ (m :+: n)
+
+foo :: SNat (Succ c) -> SNat b -> SNat (Succ (c :+: b))
+foo _ x = x
+
+
+{-
+sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m)
+     => SNat m -> SNat n -> SNat (m :+: n)
+sadd SZero n = n
+-}
+
+{- [G]  a ~ Succ c
+        Succ c + b ~ Succ (c+b)
+        a ~ Zero
+
+-->
+        Zero ~ Succ c            TyEq
+        fsk1 ~ Succ fsk2         TyEq
+        fsk1 ~ (Succ c) + b      FunEq
+        fsk2 ~ c+b               FunEq
+----
+[W] b ~ a+b  --->   b ~ Succ (c+b)
+
+
+Derived
+       a ~ Succ c
+       fsk1 ~ Succ fsk2
+       b ~ Succ fsk2
+
+work   (Succ c) + b ~ fsk1
+       c+b ~ fsk2
+
+
+-}
+
+{-
+
+[G] a ~ [b]
+--> Derived shadow [D] a ~ [b]
+    When adding this to the model
+    don't kick out a derived shadow again!
+
+[G] (a ~ b)  --> sc   a ~~ b, a ~# b
+  Silly to then kick out (a~b) and (a~~b)
+  and rewrite them to (a~a) and (a~~a)
+
+Insoluble constraint does not halt solving;
+indeed derived version stays. somehow
+-}
diff --git a/testsuite/tests/polykinds/T12444.stderr b/testsuite/tests/polykinds/T12444.stderr
new file mode 100644
index 0000000000..0ebd2986cf
--- /dev/null
+++ b/testsuite/tests/polykinds/T12444.stderr
@@ -0,0 +1,16 @@
+
+T12444.hs:19:11: error:
+    • Couldn't match type ‘b’ with ‘'Succ (c :+: b)’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall (c :: Nat) (b :: Nat).
+                 SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
+        at T12444.hs:18:1-55
+      Expected type: SNat ('Succ (c :+: b))
+        Actual type: SNat b
+    • In the expression: x
+      In an equation for ‘foo’: foo _ x = x
+    • Relevant bindings include
+        x :: SNat b (bound at T12444.hs:19:7)
+        foo :: SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
+          (bound at T12444.hs:19:1)
diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr
index df97578029..dc1b92c202 100644
--- a/testsuite/tests/polykinds/T9222.stderr
+++ b/testsuite/tests/polykinds/T9222.stderr
@@ -1,12 +1,12 @@
 
 T9222.hs:13:3: error:
-    • Couldn't match type ‘b0’ with ‘b’
-        ‘b0’ is untouchable
+    • Couldn't match type ‘c0’ with ‘c’
+        ‘c0’ is untouchable
           inside the constraints: a ~ '(b0, c0)
           bound by the type of the constructor ‘Want’:
                      a ~ '(b0, c0) => Proxy b0
           at T9222.hs:13:3
-      ‘b’ is a rigid type variable bound by
+      ‘c’ is a rigid type variable bound by
         the type of the constructor ‘Want’:
           forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1).
           (a ~ '(b, c) => Proxy b) -> Want a
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 6ec2a439e6..0e0d66a676 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -154,3 +154,4 @@ test('T12055a', normal, compile_fail, [''])
 test('T12593', normal, compile_fail, [''])
 test('T12668', normal, compile, [''])
 test('T12718', normal, compile, [''])
+test('T12444', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/Improvement.hs b/testsuite/tests/typecheck/should_compile/Improvement.hs
index e7e11901a8..8df81c26a7 100644
--- a/testsuite/tests/typecheck/should_compile/Improvement.hs
+++ b/testsuite/tests/typecheck/should_compile/Improvement.hs
@@ -1,5 +1,15 @@
 {-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-}
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+-- This one relies on doing instance reduction
+-- on a /derived/ class
+--    [W] C (F a0) a0, F a0 ~ Bool
+-- Currently (Oct 16) I've disabled this because it seems like
+-- overkill.
+--
+-- See Note Note [No reduction for Derived class constraints]
+-- in TcInteract
+
 module Foo where
 
 type family F a
@@ -14,5 +24,5 @@ blug = error "Urk"
 
 foo :: Bool
 foo = blug undefined
--- [W] C (F a0) a0, F a0 ~ Bool
+
 
diff --git a/testsuite/tests/typecheck/should_compile/T6018.hs b/testsuite/tests/typecheck/should_compile/T6018.hs
index 5fdb03b220..91a67c5e57 100644
--- a/testsuite/tests/typecheck/should_compile/T6018.hs
+++ b/testsuite/tests/typecheck/should_compile/T6018.hs
@@ -8,6 +8,38 @@
 
 module T6018 where
 
+{-
+barapp2 :: Int
+barapp2 = bar 1
+
+bar :: Bar a -> Bar a
+bar x = x
+
+type family Bar a = r | r -> a where
+    Bar Int  = Bool
+    Bar Bool = Int
+    Bar Bool = Char
+
+type family F a b c = (result :: k) | result -> a b c
+
+type family FClosed a b c = result | result -> a b c where
+    FClosed Int  Char Bool = Bool
+    FClosed Char Bool Int  = Int
+    FClosed Bool Int  Char = Char
+-}
+{-
+g6_use :: [Char]
+g6_use = g6_id "foo"
+
+g6_id :: G6 a -> G6 a
+g6_id x = x
+
+type family G6 a = r | r -> a
+type instance G6 [a]  = [Gi a]
+type family Gi a = r | r -> a
+type instance Gi Int = Char
+-}
+
 import T6018a -- defines G, identical to F
 
 type family F a b c = (result :: k) | result -> a b c
diff --git a/testsuite/tests/typecheck/should_compile/T6018.stderr b/testsuite/tests/typecheck/should_compile/T6018.stderr
index 91d6b300d6..57eed50c46 100644
--- a/testsuite/tests/typecheck/should_compile/T6018.stderr
+++ b/testsuite/tests/typecheck/should_compile/T6018.stderr
@@ -2,10 +2,10 @@
 [2 of 3] Compiling T6018a          (.hs -> .o)
 [3 of 3] Compiling T6018           (.hs -> .o)
 
-T6018.hs:75:5: warning:
+T6018.hs:107:5: warning:
     Type family instance equation is overlapped:
-      Foo Bool = Bool -- Defined at T6018.hs:75:5
+      Foo Bool = Bool -- Defined at T6018.hs:107:5
 
-T6018.hs:82:5: warning:
+T6018.hs:114:5: warning:
     Type family instance equation is overlapped:
-      Bar Bool = Char -- Defined at T6018.hs:82:5
+      Bar Bool = Char -- Defined at T6018.hs:114:5
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/Makefile b/testsuite/tests/typecheck/should_fail/Makefile
index 9101fbd40a..f994435d03 100644
--- a/testsuite/tests/typecheck/should_fail/Makefile
+++ b/testsuite/tests/typecheck/should_fail/Makefile
@@ -1,3 +1,8 @@
 TOP=../../..
 include $(TOP)/mk/boilerplate.mk
 include $(TOP)/mk/test.mk
+
+.PHONEY: foo
+
+foo:
+	echo hello
diff --git a/testsuite/tests/typecheck/should_fail/T5691.stderr b/testsuite/tests/typecheck/should_fail/T5691.stderr
index 9d4e587166..ad5c7e452f 100644
--- a/testsuite/tests/typecheck/should_fail/T5691.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5691.stderr
@@ -1,12 +1,12 @@
 
-T5691.hs:15:24: error:
+T5691.hs:14:9: error:
     • Couldn't match type ‘p’ with ‘PrintRuleInterp’
       Expected type: PrintRuleInterp a
         Actual type: p a
-    • In the first argument of ‘printRule_’, namely ‘f’
-      In the second argument of ‘($)’, namely ‘printRule_ f’
-      In the expression: MkPRI $ printRule_ f
-    • Relevant bindings include f :: p a (bound at T5691.hs:14:9)
+    • When checking that the pattern signature: p a
+        fits the type of its context: PrintRuleInterp a
+      In the pattern: f :: p a
+      In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f
 
 T5691.hs:24:10: error:
     • No instance for (Alternative RecDecParser)
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index 62385ea1df..719895af6c 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,22 +1,22 @@
 
 T5853.hs:15:46: error:
-    • Could not deduce: Subst (Subst t2 t) t1 ~ Subst t2 t1
+    • Could not deduce: Subst (Subst fa a) b ~ Subst fa b
         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 fa,
+                         Elem fa ~ Elem fa,
+                         Elem (Subst fa b) ~ b,
+                         Subst fa b ~ Subst fa b,
+                         Subst (Subst fa b) (Elem fa) ~ fa,
+                         F (Subst fa a),
+                         Elem (Subst fa a) ~ a,
+                         Elem fa ~ Elem fa,
+                         Subst (Subst fa a) (Elem fa) ~ fa,
+                         Subst fa a ~ Subst fa a)
         bound by the RULE "map/map" at T5853.hs:15:2-57
       NB: ‘Subst’ is a type function, and may not be injective
     • 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 :: Elem fa -> b (bound at T5853.hs:15:19)
+        g :: a -> Elem fa (bound at T5853.hs:15:21)
+        xs :: Subst fa a (bound at T5853.hs:15:23)
diff --git a/testsuite/tests/typecheck/should_fail/T8450.stderr b/testsuite/tests/typecheck/should_fail/T8450.stderr
index 8ba84a76f1..7503f4d37e 100644
--- a/testsuite/tests/typecheck/should_fail/T8450.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8450.stderr
@@ -1,11 +1,15 @@
 
-T8450.hs:8:7: error:
-    • Couldn't match expected type ‘a’ with actual type ‘()’
+T8450.hs:8:20: error:
+    • Couldn't match type ‘a’ with ‘Bool’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           run :: forall a. a
         at T8450.hs:7:1-18
-    • In the expression: runEffect $ (undefined :: Either a ())
+      Expected type: Either Bool ()
+        Actual type: Either a ()
+    • In the second argument of ‘($)’, namely
+        ‘(undefined :: Either a ())’
+      In the expression: runEffect $ (undefined :: Either a ())
       In an equation for ‘run’:
           run = runEffect $ (undefined :: Either a ())
     • Relevant bindings include run :: a (bound at T8450.hs:8:1)
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 4d58d4f0de..6f99a94ff4 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -336,7 +336,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, [''])