Allow recursive (undecidable) superclasses

This patch fulfils the request in Trac #11067, #10318, and #10592,
by lifting the conservative restrictions on superclass constraints.

These restrictions are there (and have been since Haskell was born) to
ensure that the transitive superclasses of a class constraint is a finite
set.  However (a) this restriction is conservative, and can be annoying
when there really is no recursion, and (b) sometimes genuinely recursive
superclasses are useful (see the tickets).

Dimitrios and I worked out that there is actually a relatively simple way
to do the job. It’s described in some detail in

   Note [The superclass story] in TcCanonical
   Note [Expanding superclasses] in TcType

In brief, the idea is to expand superclasses only finitely, but to
iterate (using a loop that already existed) if there are more
superclasses to explore.

Other small things

- I improved grouping of error messages a bit in TcErrors

- I re-centred the haddock.compiler test, which was at 9.8%
  above the norm, and which this patch pushed slightly over

44 files changed, 310 insertions, 362 deletions

diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr
index a5fe638fea..6472310ece 100644
--- a/testsuite/tests/ado/ado004.stderr
+++ b/testsuite/tests/ado/ado004.stderr
@@ -3,23 +3,23 @@ TYPE SIGNATURES
     forall (f :: * -> *). Applicative f => (Int -> f Int) -> f Int
   test2 ::
     forall (f :: * -> *) b a.
-    (Num b, Num a, Applicative f) =>
+    (Applicative f, Num a, Num b) =>
     (a -> f b) -> f b
   test3 ::
     forall (m :: * -> *) a a1 a2.
-    (Monad m, Num a2) =>
+    (Num a2, Monad m) =>
     (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a
   test4 ::
     forall (m :: * -> *) a a1 a2.
-    (Monad m, Num a2) =>
+    (Num a2, Monad m) =>
     (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a
   test5 ::
     forall (m :: * -> *) a a1 a2.
-    (Monad m, Num a2) =>
+    (Num a2, Monad m) =>
     (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a
   test6 ::
     forall r (m :: * -> *) a.
-    (Monad m, Num (m a)) =>
+    (Num (m a), Monad m) =>
     (m a -> m (m a)) -> r -> m a
 TYPE CONSTRUCTORS
 COERCION AXIOMS
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 1b4f8e65ae..b6d04ef6c1 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -34,6 +34,7 @@ expectedGhcOnlyExtensions = ["RelaxedLayout",
                              "AlternativeLayoutRule",
                              "AlternativeLayoutRuleTransitional",
                              "OverloadedLabels",
+                             "UndecidableSuperClasses",
                              "TemplateHaskellQuotes",
                              "MonadFailDesugaring",
                              "TypeInType"]
diff --git a/testsuite/tests/ghci/scripts/ghci013.stdout b/testsuite/tests/ghci/scripts/ghci013.stdout
index 245881f02b..d5afe0a691 100644
--- a/testsuite/tests/ghci/scripts/ghci013.stdout
+++ b/testsuite/tests/ghci/scripts/ghci013.stdout
@@ -1 +1 @@
-f :: (Monad m, ?callStack::CallStack) => (m a, r) -> m b
+f :: (?callStack::CallStack, Monad m) => (m a, r) -> m b
diff --git a/testsuite/tests/indexed-types/should_compile/T10318.hs b/testsuite/tests/indexed-types/should_compile/T10318.hs
new file mode 100644
index 0000000000..04a2ca105c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T10318.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE FlexibleContexts, TypeSynonymInstances,
+             FlexibleInstances, TypeFamilies,
+             UndecidableSuperClasses #-}
+
+module T10318 where
+
+-- | Product of non-zero elements always non-zero.
+-- Every integral domain has a field of fractions.
+-- The field of fractions of any field is itself.
+class (Frac (Frac a) ~ Frac a, Fractional (Frac a), IntegralDomain (Frac a))
+  => IntegralDomain a where
+  type Frac a :: *
+  embed :: a -> Frac a
+
+instance IntegralDomain Integer where
+  type Frac Integer = Rational
+  embed = fromInteger
+
+instance IntegralDomain Rational where
+  type Frac Rational = Rational
+  embed = id
+
+g :: IntegralDomain a => a -> a
+g x = g x
+
+h :: a -> Frac a
+h x = h x
+
+-- This is the test function
+
+f :: IntegralDomain a => a -> Frac a
+f x = g (h (h x))
+  -- Given: IntegralDomain (Frac a)
+  -- Wanted: IntegralDomain (Frac (Frac a))
+
diff --git a/testsuite/tests/indexed-types/should_compile/T11067.hs b/testsuite/tests/indexed-types/should_compile/T11067.hs
new file mode 100644
index 0000000000..0074fae685
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T11067.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module T11067 where
+
+import Data.Monoid
+import GHC.Exts (Constraint)
+
+type family Skolem (p :: k -> Constraint) :: k
+type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1
+
+-- | A quantified constraint
+type Forall (p :: k -> Constraint) = p (Skolem p)
+type ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) = p (f (SkolemF p f))
+
+-- These work
+class ForallF Monoid t => Monoid1 t
+instance ForallF Monoid t => Monoid1 t
+
+class ForallF Monoid1 t => Monoid2 t
+instance ForallF Monoid1 t => Monoid2 t
+
+-- Changing f a ~ g a to, (Ord (f a), Ord (g a)), say, removes the error
+class (f a ~ g a) => H f g a
+instance (f a ~ g a) => H f g a
+
+-- This one gives a superclass cycle error.
+class Forall (H f g) => H1 f g
+instance Forall (H f g) => H1 f g
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
index 53d7942958..1300626e17 100644
--- a/testsuite/tests/indexed-types/should_compile/T3017.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -1,7 +1,7 @@
 TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   test2 ::
-    forall c t t1. (Num t, Num t1, Coll c, Elem c ~ (t, t1)) => c -> c
+    forall c t t1. (Elem c ~ (t, t1), Coll c, Num t1, Num t) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c open
diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.stderr b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
index 0a0a491f17..c017701a27 100644
--- a/testsuite/tests/indexed-types/should_compile/T3208b.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
@@ -1,14 +1,4 @@
 
-T3208b.hs:15:10: error:
-    • Could not deduce: OTerm o0 ~ STerm o0 arising from a use of ‘fce’
-      from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
-        bound by the type signature for:
-                   fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
-        at T3208b.hs:14:1-56
-      The type variable ‘o0’ is ambiguous
-    • In the expression: fce (apply f)
-      In an equation for ‘fce'’: fce' f = fce (apply f)
-
 T3208b.hs:15:15: error:
     • Could not deduce: OTerm o0 ~ STerm a
         arising from a use of ‘apply’
diff --git a/testsuite/tests/indexed-types/should_compile/T8889.stderr b/testsuite/tests/indexed-types/should_compile/T8889.stderr
index 77e05d764b..44cb453421 100644
--- a/testsuite/tests/indexed-types/should_compile/T8889.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T8889.stderr
@@ -1,6 +1,6 @@
 
-T8889.hs:12:1: Warning:
+T8889.hs:12:1: warning:
     Top-level binding with no type signature:
       f :: forall (f :: * -> *) a b.
-           (C_fmap f a, C f) =>
+           (C f, C_fmap f a) =>
            (a -> b) -> f a -> f b
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 5de25bfe6b..d4ff607b56 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -266,3 +266,5 @@ test('T10806', normal, compile_fail, [''])
 test('T10815', normal, compile, [''])
 test('T10931', normal, compile, [''])
 test('T11187', normal, compile, [''])
+test('T11067', normal, compile, [''])
+test('T10318', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T1897b.stderr b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
index 459f6c8a17..e70a256f98 100644
--- a/testsuite/tests/indexed-types/should_fail/T1897b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
@@ -1,13 +1,13 @@
 
 T1897b.hs:16:1: error:
-    Couldn't match type ‘Depend a’ with ‘Depend a0’
-    NB: ‘Depend’ is a type function, and may not be injective
-    The type variable ‘a0’ is ambiguous
-    Expected type: t (Depend a) -> Bool
-      Actual type: t (Depend a0) -> Bool
-    In the ambiguity check for the inferred type for ‘isValid’
-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-    When checking the inferred type
-      isValid :: forall a (t :: * -> *).
-                 (Foldable t, Bug a) =>
-                 t (Depend a) -> Bool
+    • Couldn't match type ‘Depend a’ with ‘Depend a0’
+      NB: ‘Depend’ is a type function, and may not be injective
+      The type variable ‘a0’ is ambiguous
+      Expected type: t (Depend a) -> Bool
+        Actual type: t (Depend a0) -> Bool
+    • In the ambiguity check for the inferred type for ‘isValid’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the inferred type
+        isValid :: forall a (t :: * -> *).
+                   (Bug a, Foldable t) =>
+                   t (Depend a) -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T3330a.stderr b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
index ea3b1d4001..f6a5deeeb7 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
@@ -1,23 +1,5 @@
 
 T3330a.hs:19:34: error:
-    • Couldn't match type ‘ix’
-                     with ‘r ix1 -> Writer [AnyF s] (r'0 ix1)’
-      ‘ix’ is a rigid type variable bound by
-        the type signature for:
-          children :: forall (s :: * -> *) ix (r :: * -> *).
-                      s ix -> PF s r ix -> [AnyF s]
-        at T3330a.hs:18:13
-      Expected type: (s0 ix0 -> ix1)
-                     -> r ix1 -> Writer [AnyF s] (r'0 ix1)
-      Actual type: s ix
-    • In the first argument of ‘hmapM’, namely ‘p’
-      In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
-    • Relevant bindings include
-        x :: PF s r ix (bound at T3330a.hs:19:12)
-        p :: s ix (bound at T3330a.hs:19:10)
-        children :: s ix -> PF s r ix -> [AnyF s] (bound at T3330a.hs:19:1)
-
-T3330a.hs:19:34: error:
     • Couldn't match type ‘s’ with ‘(->) (s0 ix0 -> ix1)’
       ‘s’ is a rigid type variable bound by
         the type signature for:
@@ -26,7 +8,7 @@ T3330a.hs:19:34: error:
         at T3330a.hs:18:13
       Expected type: (s0 ix0 -> ix1)
                      -> r ix1 -> Writer [AnyF s] (r'0 ix1)
-      Actual type: s ix
+        Actual type: s ix
     • In the first argument of ‘hmapM’, namely ‘p’
       In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
     • Relevant bindings include
@@ -43,7 +25,7 @@ T3330a.hs:19:44: error:
                       s ix -> PF s r ix -> [AnyF s]
         at T3330a.hs:18:13
       Expected type: PF s r (r0 ix0 -> Writer [AnyF s0] (r0 ix0))
-      Actual type: PF s r ix
+        Actual type: PF s r ix
     • In the third argument of ‘hmapM’, namely ‘x’
       In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
     • Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr b/testsuite/tests/indexed-types/should_fail/T4174.stderr
index 60ae24ccfa..2b0524fa2f 100644
--- a/testsuite/tests/indexed-types/should_fail/T4174.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr
@@ -14,19 +14,3 @@ T4174.hs:42:12: error:
     • Relevant bindings include
         testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)
           (bound at T4174.hs:42:1)
-
-T4174.hs:42:12: error:
-    • Couldn't match type ‘b’ with ‘RtsSpinLock’
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          testcase :: forall (m :: * -> *) minor n t p a b.
-                      Monad m =>
-                      m (Field (Way (GHC6'8 minor) n t p) a b)
-        at T4174.hs:41:13
-      Expected type: m (Field (Way (GHC6'8 minor) n t p) a b)
-        Actual type: m (Field (WayOf m) SmStep RtsSpinLock)
-    • In the expression: sync_large_objects
-      In an equation for ‘testcase’: testcase = sync_large_objects
-    • Relevant bindings include
-        testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)
-          (bound at T4174.hs:42:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr
index d52f4b447d..8ac3d94a55 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -1,25 +1,12 @@
 
-T8227.hs:16:27:
-    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
-      seg :: a (bound at T8227.hs:16:21)
-      eps :: Scalar (V a) (bound at T8227.hs:16:17)
-      absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
-        (bound at T8227.hs:16:1)
-
-T8227.hs:16:44:
-    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
-    Relevant bindings include
-      seg :: a (bound at T8227.hs:16:21)
-      eps :: Scalar (V a) (bound at T8227.hs:16:17)
-      absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
-        (bound at T8227.hs:16:1)
+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
+    • Relevant bindings include
+        seg :: a (bound at T8227.hs:16:21)
+        eps :: Scalar (V a) (bound at T8227.hs:16:17)
+        absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
+          (bound at T8227.hs:16:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 2d55f9dcea..36b0716a9a 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,77 +1,21 @@
 
-T9662.hs:49:7: error:
-    • Couldn't match type ‘k’ with ‘n’
+T9662.hs:47:8: error:
+    • Couldn't match type ‘k’ with ‘Int’
       ‘k’ is a rigid type variable bound by
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
         at T9662.hs:44:9
-      ‘n’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. k) :. m) :. n)
-        Actual type: Exp (((sh :. k) :. m) :. n)
-                     -> Exp (((sh :. k) :. m) :. n)
-    • In the second argument of ‘backpermute’, namely ‘id’
-      In the expression:
-        backpermute
-          (modify
-             (atom :. atom :. atom :. atom)
-             (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
-          id
-    • Relevant bindings include
-        test :: Shape (((sh :. k) :. m) :. n)
-                -> Shape (((sh :. m) :. n) :. k)
-          (bound at T9662.hs:45:1)
-
-T9662.hs:49:7: error:
-    • Couldn't match type ‘m’ with ‘k’
-      ‘m’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      ‘k’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. k) :. m) :. n)
-        Actual type: Exp (((sh :. k) :. m) :. n)
-                     -> Exp (((sh :. k) :. m) :. n)
-    • In the second argument of ‘backpermute’, namely ‘id’
-      In the expression:
-        backpermute
-          (modify
-             (atom :. atom :. atom :. atom)
-             (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
-          id
-    • Relevant bindings include
-        test :: Shape (((sh :. k) :. m) :. n)
-                -> Shape (((sh :. m) :. n) :. k)
-          (bound at T9662.hs:45:1)
-
-T9662.hs:49:7: error:
-    • Couldn't match type ‘n’ with ‘m’
-      ‘n’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      ‘m’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. k) :. m) :. n)
-        Actual type: Exp (((sh :. k) :. m) :. n)
-                     -> Exp (((sh :. k) :. m) :. n)
-    • In the second argument of ‘backpermute’, namely ‘id’
+      Expected type: Exp (((sh :. k) :. m) :. n)
+                     -> Exp (((sh :. m) :. n) :. k)
+        Actual type: Exp
+                       (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
+                     -> Exp
+                          (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
+    • In the first argument of ‘backpermute’, namely
+        ‘(modify
+            (atom :. atom :. atom :. atom)
+            (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’
       In the expression:
         backpermute
           (modify
diff --git a/testsuite/tests/module/mod40.stderr b/testsuite/tests/module/mod40.stderr
index cd977d1e77..bd4fcf4bd9 100644
--- a/testsuite/tests/module/mod40.stderr
+++ b/testsuite/tests/module/mod40.stderr
@@ -1,8 +1,14 @@
 
-mod40.hs:3:1:
-    Cycle in class declaration (via superclasses): C1 -> C2 -> C1
-    In the class declaration for ‘C1’
+mod40.hs:3:1: error:
+    • Superclass cycle for ‘C1’
+        one of whose superclasses is ‘C2’
+        one of whose superclasses is ‘C1’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘C1’
 
-mod40.hs:4:1:
-    Cycle in class declaration (via superclasses): C2 -> C1 -> C2
-    In the class declaration for ‘C2’
+mod40.hs:4:1: error:
+    • Superclass cycle for ‘C2’
+        one of whose superclasses is ‘C1’
+        one of whose superclasses is ‘C2’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘C2’
diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
index 7554ce953d..0f0d6f91b2 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
@@ -1,8 +1,8 @@
 TYPE SIGNATURES
-  arbitCs1 :: forall a. (Enum a, Eq a, Show a) => a -> String
-  arbitCs2 :: forall a. (Show a, Enum a, Eq a) => a -> String
+  arbitCs1 :: forall a. (Show a, Eq a, Enum a) => a -> String
+  arbitCs2 :: forall a. (Show a, Eq a, Enum a) => a -> String
   arbitCs3 :: forall a. (Show a, Enum a, Eq a) => a -> String
-  arbitCs4 :: forall a. (Eq a, Enum a, Show a) => a -> String
+  arbitCs4 :: forall a. (Eq a, Show a, Enum a) => a -> String
   arbitCs5 :: forall a. (Eq a, Enum a, Show a) => a -> String
 TYPE CONSTRUCTORS
 COERCION AXIOMS
diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
index 0c0410d0f2..e7fc912a12 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
@@ -21,8 +21,8 @@ TYPE SIGNATURES
   >> :: forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
   >>= ::
     forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
-  ^ :: forall a b. (Integral b, Num a) => a -> b -> a
-  ^^ :: forall a b. (Fractional a, Integral b) => a -> b -> a
+  ^ :: forall a b. (Num a, Integral b) => a -> b -> a
+  ^^ :: forall a b. (Integral b, Fractional a) => a -> b -> a
   abs :: forall a. Num a => a -> a
   acos :: forall a. Floating a => a -> a
   acosh :: forall a. Floating a => a -> a
@@ -39,7 +39,7 @@ TYPE SIGNATURES
   atan2 :: forall a. RealFloat a => a -> a -> a
   atanh :: forall a. Floating a => a -> a
   break :: forall a. (a -> Bool) -> [a] -> ([a], [a])
-  ceiling :: forall a b. (Integral b, RealFrac a) => a -> b
+  ceiling :: forall a b. (RealFrac a, Integral b) => a -> b
   compare :: forall a. Ord a => a -> a -> Ordering
   concat :: forall (t :: * -> *) a. Foldable t => t [a] -> [a]
   concatMap ::
@@ -56,7 +56,7 @@ TYPE SIGNATURES
   dropWhile :: forall a. (a -> Bool) -> [a] -> [a]
   either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
   elem ::
-    forall (t :: * -> *) a. (Eq a, Foldable t) => a -> t a -> Bool
+    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
   encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
   enumFrom :: forall a. Enum a => a -> [a]
   enumFromThen :: forall a. Enum a => a -> a -> [a]
@@ -72,7 +72,7 @@ TYPE SIGNATURES
   floatDigits :: forall a. RealFloat a => a -> Int
   floatRadix :: forall a. RealFloat a => a -> Integer
   floatRange :: forall a. RealFloat a => a -> (Int, Int)
-  floor :: forall a b. (Integral b, RealFrac a) => a -> b
+  floor :: forall a b. (RealFrac a, Integral b) => a -> b
   fmap ::
     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
   foldl ::
@@ -89,7 +89,7 @@ TYPE SIGNATURES
     forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
   fromEnum :: forall a. Enum a => a -> Int
   fromInteger :: forall a. Num a => Integer -> a
-  fromIntegral :: forall a b. (Integral a, Num b) => a -> b
+  fromIntegral :: forall a b. (Num b, Integral a) => a -> b
   fromRational :: forall a. Fractional a => Rational -> a
   fst :: forall a b. (a, b) -> a
   gcd :: forall a. Integral a => a -> a -> a
@@ -118,24 +118,24 @@ TYPE SIGNATURES
   map :: forall a b. (a -> b) -> [a] -> [b]
   mapM ::
     forall (t :: * -> *) (m :: * -> *) a b.
-    (Monad m, Traversable t) =>
+    (Traversable t, Monad m) =>
     (a -> m b) -> t a -> m (t b)
   mapM_ ::
     forall (t :: * -> *) (m :: * -> *) a b.
-    (Monad m, Foldable t) =>
+    (Foldable t, Monad m) =>
     (a -> m b) -> t a -> m ()
   max :: forall a. Ord a => a -> a -> a
   maxBound :: forall t. Bounded t => t
-  maximum :: forall (t :: * -> *) a. (Ord a, Foldable t) => t a -> a
+  maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
   maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
   min :: forall a. Ord a => a -> a -> a
   minBound :: forall t. Bounded t => t
-  minimum :: forall (t :: * -> *) a. (Ord a, Foldable t) => t a -> a
+  minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
   mod :: forall a. Integral a => a -> a -> a
   negate :: forall a. Num a => a -> a
   not :: Bool -> Bool
   notElem ::
-    forall (t :: * -> *) a. (Eq a, Foldable t) => a -> t a -> Bool
+    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
   null :: forall (t :: * -> *) a. Foldable t => t a -> Bool
   odd :: forall a. Integral a => a -> Bool
   or :: forall (t :: * -> *). Foldable t => t Bool -> Bool
@@ -143,9 +143,9 @@ TYPE SIGNATURES
   pi :: forall t. Floating t => t
   pred :: forall a. Enum a => a -> a
   print :: forall a. Show a => a -> IO ()
-  product :: forall (t :: * -> *) a. (Num a, Foldable t) => t a -> a
+  product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
   properFraction ::
-    forall a b. (Integral b, RealFrac a) => a -> (b, a)
+    forall a b. (RealFrac a, Integral b) => a -> (b, a)
   putChar :: Char -> IO ()
   putStr :: String -> IO ()
   putStrLn :: String -> IO ()
@@ -159,14 +159,14 @@ TYPE SIGNATURES
   readParen :: forall a. Bool -> ReadS a -> ReadS a
   reads :: forall a. Read a => ReadS a
   readsPrec :: forall a. Read a => Int -> ReadS a
-  realToFrac :: forall a b. (Fractional b, Real a) => a -> b
+  realToFrac :: forall a b. (Real a, Fractional b) => a -> b
   recip :: forall a. Fractional a => a -> a
   rem :: forall a. Integral a => a -> a -> a
   repeat :: forall a. a -> [a]
   replicate :: forall a. Int -> a -> [a]
   return :: forall (m :: * -> *) a. Monad m => a -> m a
   reverse :: forall a. [a] -> [a]
-  round :: forall a b. (Integral b, RealFrac a) => a -> b
+  round :: forall a b. (RealFrac a, Integral b) => a -> b
   scaleFloat :: forall a. RealFloat a => Int -> a -> a
   scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
   scanl1 :: forall a. (a -> a -> a) -> [a] -> [a]
@@ -175,11 +175,11 @@ TYPE SIGNATURES
   seq :: forall a b. a -> b -> b
   sequence ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (Monad m, Traversable t) =>
+    (Traversable t, Monad m) =>
     t (m a) -> m (t a)
   sequence_ ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (Monad m, Foldable t) =>
+    (Foldable t, Monad m) =>
     t (m a) -> m ()
   show :: forall a. Show a => a -> String
   showChar :: Char -> ShowS
@@ -198,7 +198,7 @@ TYPE SIGNATURES
   sqrt :: forall a. Floating a => a -> a
   subtract :: forall a. Num a => a -> a -> a
   succ :: forall a. Enum a => a -> a
-  sum :: forall (t :: * -> *) a. (Num a, Foldable t) => t a -> a
+  sum :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
   tail :: forall a. [a] -> [a]
   take :: forall a. Int -> [a] -> [a]
   takeWhile :: forall a. (a -> Bool) -> [a] -> [a]
@@ -207,7 +207,7 @@ TYPE SIGNATURES
   toEnum :: forall a. Enum a => Int -> a
   toInteger :: forall a. Integral a => a -> Integer
   toRational :: forall a. Real a => a -> Rational
-  truncate :: forall a b. (Integral b, RealFrac a) => a -> b
+  truncate :: forall a b. (RealFrac a, Integral b) => a -> b
   uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
   undefined :: forall t. (?callStack::CallStack) => t
   unlines :: [String] -> String
diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
index 8b9eb466ad..3fd0860bb8 100644
--- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
@@ -10,7 +10,7 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
 WarningWildcardInstantiations.hs:5:14: warning:
     • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of foo :: (Enum a, Show a) => a -> String
+               the inferred type of foo :: (Show a, Enum a) => a -> String
                at WarningWildcardInstantiations.hs:6:1
     • In the type signature:
         foo :: (Show _a, _) => _a -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
index 2df15443c9..30efb8fc14 100644
--- a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
@@ -2,7 +2,7 @@
 InstantiatedNamedWildcardsInConstraints.hs:4:14: error:
     • Found type wildcard ‘_a’ standing for ‘b’
       Where: ‘b’ is a rigid type variable bound by
-               the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
+               the inferred type of foo :: (Show b, Enum b) => b -> (String, b)
                at InstantiatedNamedWildcardsInConstraints.hs:4:8
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
diff --git a/testsuite/tests/partial-sigs/should_fail/T10999.stderr b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
index 408529185f..3244db60ca 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10999.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
@@ -1,7 +1,7 @@
 
 T10999.hs:5:6: error:
-    Found constraint wildcard ‘_’ standing for ‘(Ord a,
-                                                 ?callStack::CallStack)’
+    Found constraint wildcard ‘_’ standing for ‘(?callStack::CallStack,
+                                                 Ord a)’
     To use the inferred type, enable PartialTypeSignatures
     In the type signature:
       f :: _ => () -> _
@@ -10,7 +10,7 @@ T10999.hs:5:17: error:
     • Found type wildcard ‘_’ standing for ‘Set.Set a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of
-               f :: (Ord a, ?callStack::CallStack) => () -> Set.Set a
+               f :: (?callStack::CallStack, Ord a) => () -> Set.Set a
                at T10999.hs:6:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
index ddbb9e2b6c..ff18935c8d 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
@@ -2,7 +2,7 @@
 WildcardInstantiations.hs:5:14: error:
     • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of foo :: (Enum a, Show a) => a -> String
+               the inferred type of foo :: (Show a, Enum a) => a -> String
                at WildcardInstantiations.hs:6:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
diff --git a/testsuite/tests/perf/haddock/all.T b/testsuite/tests/perf/haddock/all.T
index 9b8785f9c8..49a126bad9 100644
--- a/testsuite/tests/perf/haddock/all.T
+++ b/testsuite/tests/perf/haddock/all.T
@@ -91,7 +91,7 @@ test('haddock.Cabal',
 test('haddock.compiler',
      [unless(in_tree_compiler(), skip), req_haddock
      ,stats_num_field('bytes allocated',
-          [(wordsize(64), 44721228752, 10)
+          [(wordsize(64), 49395782136, 10)
             # 2012P-08-14: 26070600504 (amd64/Linux)
             # 2012-08-29: 26353100288 (amd64/Linux, new CG)
             # 2012-09-18: 26882813032 (amd64/Linux)
@@ -103,6 +103,7 @@ test('haddock.compiler',
             # 2015-06-02: 36740649320 (amd64/Linux) unknown cause
             # 2015-06-29: 40624322224 (amd64/Linux) due to #10482, not yet investigated
             # 2015-12-03: 44721228752 (amd64/Linux) slow creep upwards
+            # 2015-12-15: 49395782136 (amd64/Linux) more creep, following kind-equalities
 
           ,(platform('i386-unknown-mingw32'),   902576468, 10)
             # 2012-10-30:                     13773051312 (x86/Windows)
diff --git a/testsuite/tests/pmcheck/should_compile/T3927b.hs b/testsuite/tests/pmcheck/should_compile/T3927b.hs
index d2eb8cd6cb..98e4cb9a33 100644
--- a/testsuite/tests/pmcheck/should_compile/T3927b.hs
+++ b/testsuite/tests/pmcheck/should_compile/T3927b.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
 
 module T3927b where
diff --git a/testsuite/tests/polykinds/T7332.hs b/testsuite/tests/polykinds/T7332.hs
index 79623e9803..a18b32b838 100644
--- a/testsuite/tests/polykinds/T7332.hs
+++ b/testsuite/tests/polykinds/T7332.hs
@@ -35,18 +35,36 @@ instance (Build dc r, a ~ dc) => Build dc (a->r) where
 tspan :: (Build (DC d) r, BuildR r ~ DC d) => r
 tspan = build (id :: DC d -> DC d) mempty
 
-{- Wanted:
+{- Solving 'tspan'
+
+Given:    Build (DC d) r, BuildR r ~ DC d
+ (by sc)  Monoid (DC d)
+
+   Wanted:
        Build acc0 r0
        Monid acc0
        acc0 ~ DC d0
        DC d0 ~ BuildR r0
+       r ~ r0
 ==>
-       Build (DC d0) r0
+       Build (DC d0) r
        Monoid (DC d0)  -->  Monoid d0
-       DC d- ~ BuildR r0
-
-In fact Monoid (DC d0) is a superclass of (Build (DC do) r0)
-But during inference we do not take upserclasses of wanteds
+       DC d0 ~ BuildR r
+
+From Given: BuildR r = DC d, hence
+       DC d0 ~ DC d
+hence
+       d0 ~ d
+
+===>
+       Build (DC d) r
+       Monoid (DC d)
+
+Now things are delicate.  Either the instance Monoid (DC d) will fire or,
+if we are lucky, we might spot that (Monoid (DC d)) is a superclass of
+a given.  But now (Decl 15) we add superclasses lazily, so that is less
+likely to happen, and was always fragile.  So include (MOnoid d) in the
+signature, as was the case in the orignal ticket.
 -}
 
 
diff --git a/testsuite/tests/polykinds/T7594.hs b/testsuite/tests/polykinds/T7594.hs
index 18da70342c..ae21956d45 100644
--- a/testsuite/tests/polykinds/T7594.hs
+++ b/testsuite/tests/polykinds/T7594.hs
@@ -1,11 +1,13 @@
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE UndecidableInstances  #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs           #-}
 {-# LANGUAGE Rank2Types      #-}
+
 module T7594 where
 
 import GHC.Exts (Constraint)
diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr
index 3ee902ad78..2f1844ecdb 100644
--- a/testsuite/tests/polykinds/T7594.stderr
+++ b/testsuite/tests/polykinds/T7594.stderr
@@ -1,15 +1,16 @@
 
-T7594.hs:33:12:
-    Couldn't match type ‘b’ with ‘IO ()’
-      ‘b’ is untouchable
-        inside the constraints: (:&:) c0 Real a
-        bound by a type expected by the context: (:&:) c0 Real a => a -> b
-        at T7594.hs:33:8-19
+T7594.hs:35:12: error:
+    • Couldn't match type ‘b’ with ‘IO ()’
+        ‘b’ is untouchable
+          inside the constraints: (:&:) c0 Real a
+          bound by a type expected by the context:
+                     (:&:) c0 Real a => a -> b
+          at T7594.hs:35:8-19
       ‘b’ is a rigid type variable bound by
-          the inferred type of bar2 :: b at T7594.hs:33:1
-    Possible fix: add a type signature for ‘bar2’
-    Expected type: a -> b
-      Actual type: a -> IO ()
-    In the first argument of ‘app’, namely ‘print’
-    In the expression: app print q2
-    Relevant bindings include bar2 :: b (bound at T7594.hs:33:1)
+        the inferred type of bar2 :: b at T7594.hs:35:1
+      Possible fix: add a type signature for ‘bar2’
+      Expected type: a -> b
+        Actual type: a -> IO ()
+    • In the first argument of ‘app’, namely ‘print’
+      In the expression: app print q2
+    • Relevant bindings include bar2 :: b (bound at T7594.hs:35:1)
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index 857d11aa96..4a2473ab51 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -11,16 +11,3 @@ T9017.hs:8:7: error:
       In an equation for ‘foo’: foo = arr return
     • Relevant bindings include
         foo :: a b (m b) (bound at T9017.hs:8:1)
-
-T9017.hs:8:7: error:
-    • Couldn't match kind ‘k1’ with ‘*’
-      ‘k1’ is a rigid type variable bound by
-        the type signature for:
-          foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k).
-                 a b (m b)
-        at T9017.hs:7:8
-      When matching the kind of ‘a’
-    • In the expression: arr return
-      In an equation for ‘foo’: foo = arr return
-    • Relevant bindings include
-        foo :: a b (m b) (bound at T9017.hs:8:1)
diff --git a/testsuite/tests/simplCore/should_compile/T4398.stderr b/testsuite/tests/simplCore/should_compile/T4398.stderr
index e2411e13c7..296e691e80 100644
--- a/testsuite/tests/simplCore/should_compile/T4398.stderr
+++ b/testsuite/tests/simplCore/should_compile/T4398.stderr
@@ -1,5 +1,5 @@
 
-T4398.hs:6:11: Warning:
+T4398.hs:6:11: warning:
     Forall'd constraint ‘Ord a’ is not bound in RULE lhs
       Orig bndrs: [a, $dOrd, x, y]
       Orig lhs: let {
diff --git a/testsuite/tests/typecheck/should_compile/T10100.hs b/testsuite/tests/typecheck/should_compile/T10100.hs
index b88803c633..031be76ce2 100644
--- a/testsuite/tests/typecheck/should_compile/T10100.hs
+++ b/testsuite/tests/typecheck/should_compile/T10100.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 module T10100 where
 
diff --git a/testsuite/tests/typecheck/should_compile/T10109.hs b/testsuite/tests/typecheck/should_compile/T10109.hs
index a61b2bc294..a517eea7f9 100644
--- a/testsuite/tests/typecheck/should_compile/T10109.hs
+++ b/testsuite/tests/typecheck/should_compile/T10109.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies,
              UndecidableInstances, FlexibleInstances #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 module T10109 where
 
diff --git a/testsuite/tests/typecheck/should_compile/T10564.hs b/testsuite/tests/typecheck/should_compile/T10564.hs
index 7b19f0092d..4579dbec77 100644
--- a/testsuite/tests/typecheck/should_compile/T10564.hs
+++ b/testsuite/tests/typecheck/should_compile/T10564.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,
              DataKinds, TypeFamilies, KindSignatures, PolyKinds, FunctionalDependencies #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 module T10564 where
 
diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr
index b3a6240a6b..6232a4b78c 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9834.stderr
@@ -1,41 +1,16 @@
 
 T9834.hs:23:10: warning:
-    • Couldn't match type ‘a’ with ‘p a0’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          afix :: forall a.
-                  (forall (q :: * -> *). Applicative q => Comp p q a -> Comp p q a)
-                  -> p a
-        at T9834.hs:22:11
-         Expected type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Comp p q a -> Comp p q a)
-                        -> p a
-           Actual type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Nat (Comp p q) (Comp p q))
-                        -> p a0 -> p a0
-    • In the expression: wrapIdComp
-      In an equation for ‘afix’: afix = wrapIdComp
-    • Relevant bindings include
-        afix :: (forall (q :: * -> *).
-                 Applicative q =>
-                 Comp p q a -> Comp p q a)
-                -> p a
-          (bound at T9834.hs:23:3)
-
-T9834.hs:23:10: warning:
     • Couldn't match type ‘p’ with ‘(->) (p a0)’
       ‘p’ is a rigid type variable bound by
         the class declaration for ‘ApplicativeFix’ at T9834.hs:21:39
-         Expected type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Comp p q a -> Comp p q a)
-                        -> p a
-           Actual type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Nat (Comp p q) (Comp p q))
-                        -> p a0 -> p a0
+      Expected type: (forall (q :: * -> *).
+                      Applicative q =>
+                      Comp p q a -> Comp p q a)
+                     -> p a
+        Actual type: (forall (q :: * -> *).
+                      Applicative q =>
+                      Nat (Comp p q) (Comp p q))
+                     -> p a0 -> p a0
     • In the expression: wrapIdComp
       In an equation for ‘afix’: afix = wrapIdComp
     • Relevant bindings include
@@ -59,8 +34,8 @@ T9834.hs:23:10: warning:
           Applicative q =>
           Comp p q a1 -> Comp p q a1
         at T9834.hs:23:10
-         Expected type: Comp p q a1 -> Comp p q a1
-           Actual type: Comp p q a -> Comp p q a
+      Expected type: Comp p q a1 -> Comp p q a1
+        Actual type: Comp p q a -> Comp p q a
     • In the expression: wrapIdComp
       In an equation for ‘afix’: afix = wrapIdComp
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_compile/tc256.hs b/testsuite/tests/typecheck/should_compile/tc256.hs
index d33f7a6401..15c096e81c 100644
--- a/testsuite/tests/typecheck/should_compile/tc256.hs
+++ b/testsuite/tests/typecheck/should_compile/tc256.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances, UndecidableSuperClasses #-}
 module Ctx where
 
 import Data.Kind ( Constraint )
diff --git a/testsuite/tests/typecheck/should_fail/T2714.stderr b/testsuite/tests/typecheck/should_fail/T2714.stderr
index 0991ddeec0..bba821bcac 100644
--- a/testsuite/tests/typecheck/should_fail/T2714.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2714.stderr
@@ -1,26 +1,13 @@
-

-T2714.hs:8:5: error:

-    Couldn't match type ‘a’ with ‘f0 b’

-    ‘a’ is a rigid type variable bound by

-    the type signature for:

-      f :: forall a b. ((a -> b) -> b) -> forall c. c -> a

-    at T2714.hs:7:6

-    Expected type: ((a -> b) -> b) -> c -> a

-      Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b

-    In the expression: ffmap

-    In an equation for ‘f’: f = ffmap

-    Relevant bindings include

-      f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)

-

-T2714.hs:8:5: error:

-    Couldn't match type ‘c’ with ‘f0 (a -> b)’

-    ‘c’ is a rigid type variable bound by

-    the type signature for:

-      f :: forall c. ((a -> b) -> b) -> c -> a

-    at T2714.hs:8:1

-    Expected type: ((a -> b) -> b) -> c -> a

-      Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b

-    In the expression: ffmap

-    In an equation for ‘f’: f = ffmap

-    Relevant bindings include

-      f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)

+
+T2714.hs:8:5: error:
+    • Couldn't match type ‘a’ with ‘f0 b’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. ((a -> b) -> b) -> forall c. c -> a
+        at T2714.hs:7:6
+      Expected type: ((a -> b) -> b) -> c -> a
+        Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b
+    • In the expression: ffmap
+      In an equation for ‘f’: f = ffmap
+    • Relevant bindings include
+        f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index dc23d4a064..33ae4e16ce 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,23 +1,23 @@
 
 T5853.hs:15:52: error:
-    • Could not deduce: Subst t1 (Elem t2) ~ t2
+    • Could not deduce: Subst t2 (Elem t1) ~ t1
         arising from a use of ‘<$>’
       from the context: (F t,
                          Elem t ~ Elem t,
-                         Elem t2 ~ Elem t2,
-                         Subst t (Elem t2) ~ t2,
-                         Subst t2 (Elem t) ~ t,
-                         F t1,
                          Elem t1 ~ Elem t1,
-                         Elem t ~ Elem t,
+                         Subst t (Elem t1) ~ t1,
                          Subst t1 (Elem t) ~ t,
-                         Subst t (Elem t1) ~ t1)
+                         F t2,
+                         Elem t2 ~ Elem t2,
+                         Elem t ~ Elem t,
+                         Subst t2 (Elem t) ~ t,
+                         Subst t (Elem t2) ~ t2)
         bound by the RULE "map/map" at T5853.hs:15:2-57
-      ‘t2’ is a rigid type variable bound by
+      ‘t1’ is a rigid type variable bound by
         the RULE "map/map" at T5853.hs:15:2
     • In the expression: (f . g) <$> xs
       When checking the transformation rule "map/map"
     • Relevant bindings include
-        f :: Elem t -> Elem t2 (bound at T5853.hs:15:19)
-        g :: Elem t1 -> Elem t (bound at T5853.hs:15:21)
-        xs :: t1 (bound at T5853.hs:15:23)
+        f :: Elem t -> Elem t1 (bound at T5853.hs:15:19)
+        g :: Elem t2 -> Elem t (bound at T5853.hs:15:21)
+        xs :: t2 (bound at T5853.hs:15:23)
diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr
index 6431c274e5..f906a95e3e 100644
--- a/testsuite/tests/typecheck/should_fail/T7869.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7869.stderr
@@ -1,29 +1,16 @@
 
-T7869.hs:3:12:
-    Couldn't match type ‘a’ with ‘a1’
-      because type variable ‘a1’ would escape its scope
-    This (rigid, skolem) type variable is bound by
-      an expression type signature: [a1] -> b1
-      at T7869.hs:3:5-27
-    Expected type: [a1] -> b1
-      Actual type: [a] -> b
-    In the expression: f x
-    In the expression: (\ x -> f x) :: [a] -> b
-    In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    Relevant bindings include
-      x :: [a1] (bound at T7869.hs:3:7)
-      f :: [a] -> b (bound at T7869.hs:3:1)
-
-T7869.hs:3:12:
-    Couldn't match type ‘b’ with ‘b1’
-      because type variable ‘b1’ would escape its scope
-    This (rigid, skolem) type variable is bound by
-      an expression type signature: [a1] -> b1
-      at T7869.hs:3:5-27
-    Expected type: [a1] -> b1
-      Actual type: [a] -> b
-    In the expression: f x
-    In the expression: (\ x -> f x) :: [a] -> b
-    In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
-
+T7869.hs:3:12: error:
+    • Couldn't match type ‘a’ with ‘a1’
+        because type variable ‘a1’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        an expression type signature:
+          [a1] -> b1
+        at T7869.hs:3:5-27
+      Expected type: [a1] -> b1
+        Actual type: [a] -> b
+    • In the expression: f x
+      In the expression: (\ x -> f x) :: [a] -> b
+      In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
+    • Relevant bindings include
+        x :: [a1] (bound at T7869.hs:3:7)
+        f :: [a] -> b (bound at T7869.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/T8883.stderr b/testsuite/tests/typecheck/should_fail/T8883.stderr
index b18a97acb1..25fd7c06a0 100644
--- a/testsuite/tests/typecheck/should_fail/T8883.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8883.stderr
@@ -1,8 +1,8 @@
-

-T8883.hs:20:1: error:

-    Non type-variable argument in the constraint: Functor (PF a)

-    (Use FlexibleContexts to permit this)

-    When checking the inferred type

-      fold :: forall b a.

-              (Functor (PF a), Regular a) =>

-              (PF a b -> b) -> a -> b

+
+T8883.hs:20:1: error:
+    • Non type-variable argument in the constraint: Functor (PF a)
+      (Use FlexibleContexts to permit this)
+    • When checking the inferred type
+        fold :: forall b a.
+                (Regular a, Functor (PF a)) =>
+                (PF a b -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_fail/T9415.stderr b/testsuite/tests/typecheck/should_fail/T9415.stderr
index 516759ee30..3250b67cd3 100644
--- a/testsuite/tests/typecheck/should_fail/T9415.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9415.stderr
@@ -1,8 +1,14 @@
 
-T9415.hs:3:1:
-    Cycle in class declaration (via superclasses): C -> D -> C
-    In the class declaration for ‘C’
+T9415.hs:3:1: error:
+    • Superclass cycle for ‘C’
+        one of whose superclasses is ‘D’
+        one of whose superclasses is ‘C’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘C’
 
-T9415.hs:5:1:
-    Cycle in class declaration (via superclasses): D -> C -> D
-    In the class declaration for ‘D’
+T9415.hs:5:1: error:
+    • Superclass cycle for ‘D’
+        one of whose superclasses is ‘C’
+        one of whose superclasses is ‘D’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘D’
diff --git a/testsuite/tests/typecheck/should_fail/T9739.stderr b/testsuite/tests/typecheck/should_fail/T9739.stderr
index 34e2f114f8..c35440a234 100644
--- a/testsuite/tests/typecheck/should_fail/T9739.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9739.stderr
@@ -1,10 +1,14 @@
 
-T9739.hs:4:1:
-    Cycle in class declaration (via superclasses):
-      Class1 -> Class3 -> Class1
-    In the class declaration for ‘Class1’
+T9739.hs:4:1: error:
+    • Superclass cycle for ‘Class1’
+        one of whose superclasses is ‘Class3’
+        one of whose superclasses is ‘Class1’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘Class1’
 
-T9739.hs:9:1:
-    Cycle in class declaration (via superclasses):
-      Class3 -> Class1 -> Class3
-    In the class declaration for ‘Class3’
+T9739.hs:9:1: error:
+    • Superclass cycle for ‘Class3’
+        one of whose superclasses is ‘Class1’
+        one of whose superclasses is ‘Class3’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘Class3’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail027.stderr b/testsuite/tests/typecheck/should_fail/tcfail027.stderr
index 9cfdcf4a9a..e8b2770e2b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail027.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail027.stderr
@@ -1,8 +1,14 @@
 
-tcfail027.hs:4:1:
-    Cycle in class declaration (via superclasses): A -> B -> A
-    In the class declaration for ‘A’
+tcfail027.hs:4:1: error:
+    • Superclass cycle for ‘A’
+        one of whose superclasses is ‘B’
+        one of whose superclasses is ‘A’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘A’
 
-tcfail027.hs:7:1:
-    Cycle in class declaration (via superclasses): B -> A -> B
-    In the class declaration for ‘B’
+tcfail027.hs:7:1: error:
+    • Superclass cycle for ‘B’
+        one of whose superclasses is ‘A’
+        one of whose superclasses is ‘B’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘B’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail216.hs b/testsuite/tests/typecheck/should_fail/tcfail216.hs
index 34d4882e02..16a56e082e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail216.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail216.hs
@@ -1,4 +1,3 @@
--- Test we do get a cycle for superclasses escaping via a free tyvar
 {-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, UndecidableInstances #-}
 module TcFail where
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail216.stderr b/testsuite/tests/typecheck/should_fail/tcfail216.stderr
index d354867480..520f5590dd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail216.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail216.stderr
@@ -1,4 +1,7 @@
 
-tcfail216.hs:5:1:
-    Cycle in class declaration (via superclasses): A -> A
-    In the class declaration for ‘A’
+tcfail216.hs:4:1: error:
+    • Potential superclass cycle for ‘A’
+        one of whose superclass constraints is headed by a type variable:
+          ‘cls (A cls)’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘A’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail217.hs b/testsuite/tests/typecheck/should_fail/tcfail217.hs
index 47c5078f02..62a6e5bae8 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail217.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail217.hs
@@ -4,4 +4,4 @@ module TcFail where
 
 type Aish = A
 
-class cls (Aish cls) => A cls c where
+class Aish a => A a where
diff --git a/testsuite/tests/typecheck/should_fail/tcfail217.stderr b/testsuite/tests/typecheck/should_fail/tcfail217.stderr
index 0dc1a593b1..729080373c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail217.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail217.stderr
@@ -1,4 +1,6 @@
 
 tcfail217.hs:7:1: error:
-    Cycle in class declaration (via superclasses): A -> Aish -> A
-    In the class declaration for ‘A’
+    • Superclass cycle for ‘A’
+        one of whose superclasses is ‘A’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘A’