Simple subsumptionwip/T17775

This patch simplifies GHC to use simple subsumption.
  Ticket #17775

Implements GHC proposal #287
   https://github.com/ghc-proposals/ghc-proposals/blob/master/
   proposals/0287-simplify-subsumption.rst

All the motivation is described there; I will not repeat it here.
The implementation payload:
 * tcSubType and friends become noticably simpler, because it no
   longer uses eta-expansion when checking subsumption.
 * No deeplyInstantiate or deeplySkolemise

That in turn means that some tests fail, by design; they can all
be fixed by eta expansion.  There is a list of such changes below.

Implementing the patch led me into a variety of sticky corners, so
the patch includes several othe changes, some quite significant:

* I made String wired-in, so that
    "foo" :: String   rather than
    "foo" :: [Char]
  This improves error messages, and fixes #15679

* The pattern match checker relies on knowing about in-scope equality
  constraints, andd adds them to the desugarer's environment using
  addTyCsDs.  But the co_fn in a FunBind was missed, and for some reason
  simple-subsumption ends up with dictionaries there. So I added a
  call to addTyCsDs.  This is really part of #18049.

* I moved the ic_telescope field out of Implication and into
  ForAllSkol instead.  This is a nice win; just expresses the code
  much better.

* There was a bug in GHC.Tc.TyCl.Instance.tcDataFamInstHeader.
  We called checkDataKindSig inside tc_kind_sig, /before/
  solveEqualities and zonking.  Obviously wrong, easily fixed.

* solveLocalEqualitiesX: there was a whole mess in here, around
  failing fast enough.  I discovered a bad latent bug where we
  could successfully kind-check a type signature, and use it,
  but have unsolved constraints that could fill in coercion
  holes in that signature --  aargh.

  It's all explained in Note [Failure in local type signatures]
  in GHC.Tc.Solver. Much better now.

* I fixed a serious bug in anonymous type holes. IN
    f :: Int -> (forall a. a -> _) -> Int
  that "_" should be a unification variable at the /outer/
  level; it cannot be instantiated to 'a'.  This was plain
  wrong.  New fields mode_lvl and mode_holes in TcTyMode,
  and auxiliary data type GHC.Tc.Gen.HsType.HoleMode.

  This fixes #16292, but makes no progress towards the more
  ambitious #16082

* I got sucked into an enormous refactoring of the reporting of
  equality errors in GHC.Tc.Errors, especially in
      mkEqErr1
      mkTyVarEqErr
      misMatchMsg
      misMatchMsgOrCND
  In particular, the very tricky mkExpectedActualMsg function
  is gone.

  It took me a full day.  But the result is far easier to understand.
  (Still not easy!)  This led to various minor improvements in error
  output, and an enormous number of test-case error wibbles.

  One particular point: for occurs-check errors I now just say
     Can't match 'a' against '[a]'
  rather than using the intimidating language of "occurs check".

* Pretty-printing AbsBinds

Tests review

* Eta expansions
   T11305: one eta expansion
   T12082: one eta expansion (undefined)
   T13585a: one eta expansion
   T3102:  one eta expansion
   T3692:  two eta expansions (tricky)
   T2239:  two eta expansions
   T16473: one eta
   determ004: two eta expansions (undefined)
   annfail06: two eta (undefined)
   T17923: four eta expansions (a strange program indeed!)
   tcrun035: one eta expansion

* Ambiguity check at higher rank.  Now that we have simple
  subsumption, a type like
     f :: (forall a. Eq a => Int) -> Int
  is no longer ambiguous, because we could write
     g :: (forall a. Eq a => Int) -> Int
     g = f
  and it'd typecheck just fine.  But f's type is a bit
  suspicious, and we might want to consider making the
  ambiguity check do a check on each sub-term.  Meanwhile,
  these tests are accepted, whereas they were previously
  rejected as ambiguous:
     T7220a
     T15438
     T10503
     T9222

* Some more interesting error message wibbles
   T13381: Fine: one error (Int ~ Exp Int)
           rather than two (Int ~ Exp Int, Exp Int ~ Int)
   T9834:  Small change in error (improvement)
   T10619: Improved
   T2414:  Small change, due to order of unification, fine
   T2534:  A very simple case in which a change of unification order
           means we get tow unsolved constraints instead of one
   tc211: bizarre impredicative tests; just accept this for now

Updates Cabal and haddock submodules.

Metric Increase:
  T12150
  T12234
  T5837
  haddock.base
Metric Decrease:
  haddock.compiler
  haddock.Cabal
  haddock.base

Merge note: This appears to break the
`UnliftedNewtypesDifficultUnification` test. It has been marked as
broken in the interest of merging.

(cherry picked from commit 66b7b195cb3dce93ed5078b80bf568efae904cc5)

46 files changed, 228 insertions, 173 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
index 5b6863c740..5ba9df0d1a 100644
--- a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
+++ b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
@@ -22,7 +22,8 @@ PushedInAsGivens.hs:10:31: error:
         bar :: a -> (a, Int) (bound at PushedInAsGivens.hs:9:1)
 
 PushedInAsGivens.hs:11:15: error:
-    • Couldn't match type ‘F Int’ with ‘[a]’
+    • Couldn't match type: F Int
+                     with: [a]
         arising from a use of ‘foo’
     • In the expression: foo y
       In the expression: (y, foo y)
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.hs b/testsuite/tests/indexed-types/should_compile/Simple14.hs
index 0a47a649a5..dba26194f1 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.hs
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.hs
@@ -5,21 +5,23 @@ module Simple14 where
 data EQ_ x y = EQ_
 
 -- Nov 2014: actually eqE has an ambiguous type
+-- Apr 2020: now it doesn't again
 eqE :: EQ_ x y -> (x~y => EQ_ z z) -> p
-eqE = error "eqE"
+eqE x y = error "eqE"
 
 eqI :: EQ_ x x
 eqI = error "eqI"
 
 ntI :: (forall p. EQ_ x y -> p) -> EQ_ x y
-ntI = error "ntI" 
+ntI x = error "ntI"
 
 foo :: forall m n. EQ_ (Maybe m) (Maybe n)
-foo = ntI (`eqE` (eqI :: EQ_ m n))
+foo = ntI (\x -> x `eqE` (eqI :: EQ_ m n))
+
 -- Alternative
 -- foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
 
 -- eq :: EQ_ (Maybe m) (Maybe n)
 -- Need (Maybe m ~ Maybe n) =>  EQ_ m n ~ EQ_ zeta zeta
 -- which reduces to (m~n) => m ~ zeta
--- but then we are stuck
\ No newline at end of file
+-- but then we are stuck
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
index 4c61d95cc9..6159b08898 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.stderr
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -1,17 +1,21 @@
 
-Simple14.hs:8:8: error:
-    • Couldn't match type ‘z0’ with ‘z’
+Simple14.hs:19:27: error:
+    • Couldn't match type ‘z0’ with ‘n’
+      Expected: EQ_ z0 z0
+        Actual: EQ_ m n
         ‘z0’ is untouchable
-          inside the constraints: x ~ y
+          inside the constraints: Maybe m ~ Maybe n
           bound by a type expected by the context:
-                     (x ~ y) => EQ_ z0 z0
-          at Simple14.hs:8:8-39
-      ‘z’ is a rigid type variable bound by
+                     (Maybe m ~ Maybe n) => EQ_ z0 z0
+          at Simple14.hs:19:26-41
+      ‘n’ is a rigid type variable bound by
         the type signature for:
-          eqE :: forall x y z p. EQ_ x y -> ((x ~ y) => EQ_ z z) -> p
-        at Simple14.hs:8:8-39
-      Expected type: EQ_ z0 z0
-        Actual type: EQ_ z z
-    • In the ambiguity check for ‘eqE’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature: eqE :: EQ_ x y -> (x ~ y => EQ_ z z) -> p
+          foo :: forall m n. EQ_ (Maybe m) (Maybe n)
+        at Simple14.hs:18:1-42
+    • In the second argument of ‘eqE’, namely ‘(eqI :: EQ_ m n)’
+      In the expression: x `eqE` (eqI :: EQ_ m n)
+      In the first argument of ‘ntI’, namely
+        ‘(\ x -> x `eqE` (eqI :: EQ_ m n))’
+    • Relevant bindings include
+        x :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:19:13)
+        foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:19:1)
diff --git a/testsuite/tests/indexed-types/should_compile/T10806.stderr b/testsuite/tests/indexed-types/should_compile/T10806.stderr
index c78a10bd7b..96284e6c75 100644
--- a/testsuite/tests/indexed-types/should_compile/T10806.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T10806.stderr
@@ -1,7 +1,7 @@
 
 T10806.hs:11:32: error:
-    • Couldn't match expected type ‘Char -> Bool’
-                  with actual type ‘IO ()’
+    • Couldn't match expected type: Char -> Bool
+                  with actual type: IO ()
     • The function ‘print’ is applied to two value arguments,
         but its type ‘Char -> IO ()’ has only one
       In the expression: print 'x' 'y'
diff --git a/testsuite/tests/indexed-types/should_compile/T12538.stderr b/testsuite/tests/indexed-types/should_compile/T12538.stderr
index ca106246e7..7a26b9c483 100644
--- a/testsuite/tests/indexed-types/should_compile/T12538.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T12538.stderr
@@ -3,10 +3,11 @@ 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
+      Expected: a -> b
+        Actual: a -> DF (Tagged Int a)
       ‘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)
+        the instance declaration
+        at T12538.hs:36:10-46
     • In the expression: DF . tag
       In an equation for ‘df’: df = DF . tag
       In the instance declaration for ‘ToDF a b’
diff --git a/testsuite/tests/indexed-types/should_compile/T17923.hs b/testsuite/tests/indexed-types/should_compile/T17923.hs
index 8c34024864..a6840ff616 100644
--- a/testsuite/tests/indexed-types/should_compile/T17923.hs
+++ b/testsuite/tests/indexed-types/should_compile/T17923.hs
@@ -38,7 +38,7 @@ data ShowCharSym0 :: E ~> E ~> E
 
 sShow_tuple :: SLambda Sym4
 sShow_tuple
-  = applySing (singFun2 @Sym3 und)
+  = applySing (singFun2 @Sym3 (\x -> und x))
           (und (singFun2 @Sym3
-                 (und (applySing (singFun2 @Sym3 und)
-                                 (applySing (singFun2 @ShowCharSym0 und) und)))))
+                     (\y -> und (applySing (singFun2 @Sym3 (\x -> und x))
+                                 (applySing (singFun2 @ShowCharSym0 (\x -> und x)) und)) y)))
diff --git a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
index 5bc6aca64c..63f24fa268 100644
--- a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
@@ -1,6 +1,7 @@
 
 ExtraTcsUntch.hs:23:18: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[p]’
+    • Couldn't match expected type: F Int
+                  with actual type: [p]
     • In the first argument of ‘h’, namely ‘[x]’
       In the expression: h [x]
       In an equation for ‘g1’: g1 _ = h [x]
@@ -9,7 +10,8 @@ ExtraTcsUntch.hs:23:18: error:
         f :: p -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
 ExtraTcsUntch.hs:25:38: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[[a0]]’
+    • Couldn't match expected type: F Int
+                  with actual type: [[a0]]
       The type variable ‘a0’ is ambiguous
     • In the first argument of ‘h’, namely ‘[[undefined]]’
       In the expression: h [[undefined]]
diff --git a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
index 9eab513529..1f155bbea0 100644
--- a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
+++ b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
@@ -1,8 +1,9 @@
 
 NoMatchErr.hs:19:7: error:
-    • Couldn't match type ‘Memo d0’ with ‘Memo d’
-      Expected type: Memo d a -> Memo d a
-        Actual type: Memo d0 a -> Memo d0 a
+    • Couldn't match type: Memo d0
+                     with: Memo d
+      Expected: Memo d a -> Memo d a
+        Actual: Memo d0 a -> Memo d0 a
       NB: ‘Memo’ is a non-injective type family
       The type variable ‘d0’ is ambiguous
     • In the ambiguity check for ‘f’
diff --git a/testsuite/tests/indexed-types/should_fail/Overlap6.stderr b/testsuite/tests/indexed-types/should_fail/Overlap6.stderr
index c0b1d64889..b1aaea25b1 100644
--- a/testsuite/tests/indexed-types/should_fail/Overlap6.stderr
+++ b/testsuite/tests/indexed-types/should_fail/Overlap6.stderr
@@ -1,12 +1,12 @@
 
 Overlap6.hs:15:7: error:
     • Couldn't match type ‘x’ with ‘And x 'True’
+      Expected: Proxy (And x 'True)
+        Actual: Proxy x
       ‘x’ is a rigid type variable bound by
         the type signature for:
           g :: forall (x :: Bool). Proxy x -> Proxy (And x 'True)
         at Overlap6.hs:14:1-34
-      Expected type: Proxy (And x 'True)
-        Actual type: Proxy x
     • In the expression: x
       In an equation for ‘g’: g x = x
     • Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
index fa635378a4..df131da8a3 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
@@ -1,9 +1,10 @@
 
 SimpleFail16.hs:10:12: error:
-    Couldn't match expected type ‘p0 a0’ with actual type ‘F ()’
-    The type variables ‘p0’, ‘a0’ are ambiguous
-    In the first argument of ‘foo’, namely ‘(undefined :: F ())’
-    In the expression: foo (undefined :: F ())
-    In an equation for ‘bar’: bar = foo (undefined :: F ())
-    Relevant bindings include
-      bar :: p0 a0 (bound at SimpleFail16.hs:10:1)
+    • Couldn't match expected type: p0 a0
+                  with actual type: F ()
+      The type variables ‘p0’, ‘a0’ are ambiguous
+    • In the first argument of ‘foo’, namely ‘(undefined :: F ())’
+      In the expression: foo (undefined :: F ())
+      In an equation for ‘bar’: bar = foo (undefined :: F ())
+    • Relevant bindings include
+        bar :: p0 a0 (bound at SimpleFail16.hs:10:1)
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
index 69a7170504..c437d95501 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
@@ -1,12 +1,12 @@
 
 SimpleFail5a.hs:31:11: error:
     • Couldn't match type ‘a’ with ‘Int’
+      Expected: S3 a
+        Actual: S3 Int
       ‘a’ is a rigid type variable bound by
         the type signature for:
           bar3wrong :: forall a. S3 a -> a
         at SimpleFail5a.hs:30:1-22
-      Expected type: S3 a
-        Actual type: S3 Int
     • In the pattern: D3Int
       In an equation for ‘bar3wrong’: bar3wrong D3Int = 1
     • Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail5b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail5b.stderr
index 0dfd570cc0..7398ef0fe8 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail5b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail5b.stderr
@@ -1,7 +1,7 @@
 
-SimpleFail5b.hs:31:12:
-    Couldn't match type ‘Char’ with ‘Int’
-    Expected type: S3 Int
-      Actual type: S3 Char
-    In the pattern: D3Char
-    In an equation for ‘bar3wrong'’: bar3wrong' D3Char = 'a'
+SimpleFail5b.hs:31:12: error:
+    • Couldn't match type ‘Char’ with ‘Int’
+      Expected: S3 Int
+        Actual: S3 Char
+    • In the pattern: D3Char
+      In an equation for ‘bar3wrong'’: bar3wrong' D3Char = 'a'
diff --git a/testsuite/tests/indexed-types/should_fail/T13674.stderr b/testsuite/tests/indexed-types/should_fail/T13674.stderr
index 53a7cb705c..55798b1189 100644
--- a/testsuite/tests/indexed-types/should_fail/T13674.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13674.stderr
@@ -1,8 +1,12 @@
 
 T13674.hs:56:21: error:
-    • Occurs check: cannot construct the infinite type: m ~ Lcm m m
-      Expected type: GF m
-        Actual type: GF (Lcm m m)
+    • Couldn't match type ‘m’ with ‘Lcm m m’
+      Expected: GF m
+        Actual: GF (Lcm m m)
+      ‘m’ is a rigid type variable bound by
+        the type signature for:
+          bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
+        at T13674.hs:55:1-44
     • In the first argument of ‘(-)’, namely ‘foo x y’
       In the expression:
         foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
@@ -15,9 +19,13 @@ T13674.hs:56:21: error:
         bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1)
 
 T13674.hs:56:31: error:
-    • Occurs check: cannot construct the infinite type: m ~ Lcm m m
-      Expected type: GF m
-        Actual type: GF (Lcm m m)
+    • Couldn't match type ‘m’ with ‘Lcm m m’
+      Expected: GF m
+        Actual: GF (Lcm m m)
+      ‘m’ is a rigid type variable bound by
+        the type signature for:
+          bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
+        at T13674.hs:55:1-44
     • In the first argument of ‘(\\)’, namely ‘foo y x’
       In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
       In the second argument of ‘(-)’, namely
diff --git a/testsuite/tests/indexed-types/should_fail/T13784.stderr b/testsuite/tests/indexed-types/should_fail/T13784.stderr
index 63edf0482f..11b1a188f2 100644
--- a/testsuite/tests/indexed-types/should_fail/T13784.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13784.stderr
@@ -1,11 +1,11 @@
 
 T13784.hs:29:28: error:
     • Couldn't match type ‘as’ with ‘a : Divide a as’
+      Expected: Product (Divide a (a : as))
+        Actual: Product as1
       ‘as’ is a rigid type variable bound by
         the instance declaration
         at T13784.hs:25:10-30
-      Expected type: Product (Divide a (a : as))
-        Actual type: Product as1
     • In the expression: as
       In the expression: (a, as)
       In an equation for ‘divide’: divide (a :* as) = (a, as)
@@ -14,10 +14,10 @@ T13784.hs:29:28: error:
           (bound at T13784.hs:29:5)
 
 T13784.hs:33:24: error:
-    • Couldn't match type ‘Product (a : as0)’
-                     with ‘(b, Product (Divide b (a : as)))’
-      Expected type: (b, Product (Divide b (a : as)))
-        Actual type: Product (a1 : as0)
+    • Couldn't match type: Product (a : as0)
+                     with: (b, Product (Divide b (a : as)))
+      Expected: (b, Product (Divide b (a : as)))
+        Actual: Product (a1 : as0)
     • In the expression: a :* divide as
       In an equation for ‘divide’: divide (a :* as) = a :* divide as
       In the instance declaration for ‘Divideable b (a : as)’
@@ -26,10 +26,10 @@ T13784.hs:33:24: error:
           (bound at T13784.hs:33:5)
 
 T13784.hs:33:29: error:
-    • Couldn't match type ‘(a0, Product (Divide a0 as))’
-                     with ‘Product as0’
-      Expected type: Product as0
-        Actual type: (a0, Product (Divide a0 as1))
+    • Couldn't match type: (a0, Product (Divide a0 as))
+                     with: Product as0
+      Expected: Product as0
+        Actual: (a0, Product (Divide a0 as1))
     • In the second argument of ‘(:*)’, namely ‘divide as’
       In the expression: a :* divide as
       In an equation for ‘divide’: divide (a :* as) = a :* divide as
diff --git a/testsuite/tests/indexed-types/should_fail/T14246.stderr b/testsuite/tests/indexed-types/should_fail/T14246.stderr
index fcc2605527..d6bfde7b5b 100644
--- a/testsuite/tests/indexed-types/should_fail/T14246.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14246.stderr
@@ -5,20 +5,24 @@ T14246.hs:18:5: error:
       In the type family declaration for ‘KLN’
 
 T14246.hs:22:27: error:
-    • Expected kind ‘Vect (KLN f) L’,
+    • Couldn't match kind: 'S (KLN (f t))
+                     with: KLN f
+      Expected kind ‘Vect (KLN f) L’,
         but ‘Cons (Label (t :: v)) l’ has kind ‘Vect ('S (KLN (f t))) (*)’
     • In the second argument of ‘Reveal’, namely
         ‘(Cons (Label (t :: v)) l)’
       In the type family declaration for ‘Reveal’
 
 T14246.hs:22:67: error:
-    • Expected kind ‘Vect (KLN (f t)) L’,
+    • Couldn't match kind ‘*’ with ‘L’
+      Expected kind ‘Vect (KLN (f t)) L’,
         but ‘l’ has kind ‘Vect (KLN (f t)) (*)’
     • In the second argument of ‘Reveal’, namely ‘l’
       In the type ‘Reveal (f t) l’
       In the type family declaration for ‘Reveal’
 
 T14246.hs:23:24: error:
-    • Expected kind ‘Vect (KLN a) L’, but ‘Nil’ has kind ‘Vect 'Z L’
+    • Couldn't match kind ‘'Z’ with ‘KLN a’
+      Expected kind ‘Vect (KLN a) L’, but ‘Nil’ has kind ‘Vect 'Z L’
     • In the second argument of ‘Reveal’, namely ‘Nil’
       In the type family declaration for ‘Reveal’
diff --git a/testsuite/tests/indexed-types/should_fail/T14369.stderr b/testsuite/tests/indexed-types/should_fail/T14369.stderr
index accd2d9b01..d31a77b2fa 100644
--- a/testsuite/tests/indexed-types/should_fail/T14369.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14369.stderr
@@ -1,8 +1,9 @@
 
 T14369.hs:29:5: error:
-    • Couldn't match type ‘Demote a’ with ‘Demote a1’
-      Expected type: Sing x -> Maybe (Demote a1)
-        Actual type: Sing x -> Demote (Maybe a)
+    • Couldn't match type: Demote a
+                     with: Demote a1
+      Expected: Sing x -> Maybe (Demote a1)
+        Actual: Sing x -> Demote (Maybe a)
     • In the expression: fromSing
       In an equation for ‘f’: f = fromSing
     • Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/T14904.stderr b/testsuite/tests/indexed-types/should_fail/T14904.stderr
index dd5506c855..8a7142d350 100644
--- a/testsuite/tests/indexed-types/should_fail/T14904.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14904.stderr
@@ -1,6 +1,8 @@
 
 T14904.hs:8:8: error:
     • Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k0’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: forall (a :: k1). g a
     • In the first argument of ‘F’, namely
         ‘((f :: forall a. g a) :: forall a. g a)’
       In the type family declaration for ‘F’
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr
index 4acacbab50..2cba04fd97 100644
--- a/testsuite/tests/indexed-types/should_fail/T15870.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr
@@ -1,6 +1,7 @@
 
 T15870.hs:32:34: error:
-    • Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
+    • Couldn't match kind ‘k’ with ‘*’
+      Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
     • In the second argument of ‘Get’, namely ‘g2’
       In the type ‘Get a g2’
       In the type instance declaration for ‘Get’
diff --git a/testsuite/tests/indexed-types/should_fail/T1897b.stderr b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
index a2055816ae..9048b59770 100644
--- a/testsuite/tests/indexed-types/should_fail/T1897b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
@@ -1,8 +1,9 @@
 
 T1897b.hs:16:1: error:
-    • Couldn't match type ‘Depend a’ with ‘Depend a0’
-      Expected type: t (Depend a) -> Bool
-        Actual type: t (Depend a0) -> Bool
+    • Couldn't match type: Depend a0
+                     with: Depend a
+      Expected: t (Depend a) -> Bool
+        Actual: t (Depend a0) -> Bool
       NB: ‘Depend’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for the inferred type for ‘isValid’
diff --git a/testsuite/tests/indexed-types/should_fail/T1900.stderr b/testsuite/tests/indexed-types/should_fail/T1900.stderr
index 4b144f85f6..a9fb9051e8 100644
--- a/testsuite/tests/indexed-types/should_fail/T1900.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1900.stderr
@@ -1,8 +1,9 @@
 
 T1900.hs:7:3: error:
-    • Couldn't match type ‘Depend s0’ with ‘Depend s’
-      Expected type: Depend s -> Depend s
-        Actual type: Depend s0 -> Depend s0
+    • Couldn't match type: Depend s0
+                     with: Depend s
+      Expected: Depend s -> Depend s
+        Actual: Depend s0 -> Depend s0
       NB: ‘Depend’ is a non-injective type family
       The type variable ‘s0’ is ambiguous
     • In the ambiguity check for ‘trans’
diff --git a/testsuite/tests/indexed-types/should_fail/T2239.hs b/testsuite/tests/indexed-types/should_fail/T2239.hs
index 0d675b175c..c64021c070 100644
--- a/testsuite/tests/indexed-types/should_fail/T2239.hs
+++ b/testsuite/tests/indexed-types/should_fail/T2239.hs
@@ -45,11 +45,11 @@ simpleTF = id :: (forall b. b~Bool => b->b)
 
 -- Actually these two do not involve impredicative instantiation,
 -- so they now succeed
-complexFD = id :: (forall b. MyEq b Bool => b->b)
-               -> (forall c. MyEq c Bool => c->c)
+complexFD = (\x -> x) :: (forall b. MyEq b Bool => b->b)
+                      -> (forall c. MyEq c Bool => c->c)
 
-complexTF = id :: (forall b. b~Bool => b->b)
-               -> (forall c. c~Bool => c->c)
+complexTF = (\x -> x) :: (forall b. b~Bool => b->b)
+                      -> (forall c. c~Bool => c->c)
 
 {- For example, here is how the subsumption check works for complexTF
    when type-checking the expression
@@ -65,4 +65,4 @@ complexTF = id :: (forall b. b~Bool => b->b)
       b~Bool |-3  alpha[3] ~ b->b,  (forall c. c~Bool => c->c) <= a
 
    And this is perfectly soluble.  alpha is touchable; and c is instantiated.
--}
\ No newline at end of file
+-}
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 6b1a6bd075..40409c10cc 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,8 +1,9 @@
 
 T2544.hs:19:18: error:
-    • Couldn't match type ‘IxMap i0’ with ‘IxMap l’
-      Expected type: IxMap l [Int]
-        Actual type: IxMap i0 [Int]
+    • Couldn't match type: IxMap i0
+                     with: IxMap l
+      Expected: IxMap l [Int]
+        Actual: IxMap i0 [Int]
       NB: ‘IxMap’ is a non-injective type family
       The type variable ‘i0’ is ambiguous
     • In the first argument of ‘BiApp’, namely ‘empty’
diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.stderr b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
index 63f11b97f1..b69883ab88 100644
--- a/testsuite/tests/indexed-types/should_fail/T2627b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
@@ -1,8 +1,18 @@
 
 T2627b.hs:20:24: error:
-    • Occurs check: cannot construct the infinite type:
-        b0 ~ Dual (Dual b0)
+    • Could not deduce: Dual (Dual b0) ~ b0
         arising from a use of ‘conn’
+      from the context: (Dual a ~ b, Dual b ~ a)
+        bound by the type signature for:
+                   conn :: forall a b.
+                           (Dual a ~ b, Dual b ~ a) =>
+                           Comm a -> Comm b -> (Int, Int)
+        at T2627b.hs:19:1-66
+      or from: a ~ R c d
+        bound by a pattern with constructor:
+                   Rd :: forall c d. (c -> Comm d) -> Comm (R c d),
+                 in an equation for ‘conn’
+        at T2627b.hs:20:7-10
       The type variable ‘b0’ is ambiguous
     • In the expression: conn undefined undefined
       In an equation for ‘conn’:
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
index f52703865f..64fa851258 100644
--- a/testsuite/tests/indexed-types/should_fail/T2664.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -7,8 +7,8 @@ T2664.hs:31:9: error:
                                ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
                                IO (PChan (a :*: b), PChan c)
         at T2664.hs:23:5-12
-      Expected type: IO (PChan (a :*: b), PChan c)
-        Actual type: IO (PChan (a :*: b), PChan (Dual b :+: Dual a))
+      Expected: IO (PChan (a :*: b), PChan c)
+        Actual: IO (PChan (a :*: b), PChan (Dual b :+: Dual a))
       NB: ‘Dual’ is a non-injective type family
     • In a stmt of a 'do' block:
         return
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.stderr b/testsuite/tests/indexed-types/should_fail/T2693.stderr
index f9485d1d42..57d4303849 100644
--- a/testsuite/tests/indexed-types/should_fail/T2693.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -1,6 +1,7 @@
 
 T2693.hs:12:15: error:
-    • Couldn't match expected type ‘(a8, b1)’ with actual type ‘TFn a6’
+    • Couldn't match expected type: (a8, b1)
+                  with actual type: TFn a6
       The type variables ‘a6’, ‘a8’, ‘b1’ are ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the first argument of ‘(+)’, namely ‘fst x’
@@ -8,7 +9,8 @@ T2693.hs:12:15: error:
     • Relevant bindings include n :: a8 (bound at T2693.hs:12:7)
 
 T2693.hs:12:23: error:
-    • Couldn't match expected type ‘(a8, b2)’ with actual type ‘TFn a7’
+    • Couldn't match expected type: (a8, b2)
+                  with actual type: TFn a7
       The type variables ‘a7’, ‘a8’, ‘b2’ are ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the second argument of ‘(+)’, namely ‘fst x’
@@ -16,7 +18,8 @@ T2693.hs:12:23: error:
     • Relevant bindings include n :: a8 (bound at T2693.hs:12:7)
 
 T2693.hs:19:15: error:
-    • Couldn't match expected type ‘(a5, b0)’ with actual type ‘TFn a2’
+    • Couldn't match expected type: (a5, b0)
+                  with actual type: TFn a2
       The type variables ‘a2’, ‘a5’, ‘b0’ are ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the first argument of ‘(+)’, namely ‘fst x’
@@ -24,7 +27,8 @@ T2693.hs:19:15: error:
     • Relevant bindings include n :: a5 (bound at T2693.hs:19:7)
 
 T2693.hs:19:23: error:
-    • Couldn't match expected type ‘(a4, a5)’ with actual type ‘TFn a3’
+    • Couldn't match expected type: (a4, a5)
+                  with actual type: TFn a3
       The type variables ‘a3’, ‘a4’, ‘a5’ are ambiguous
     • In the first argument of ‘snd’, namely ‘x’
       In the second argument of ‘(+)’, namely ‘snd x’
@@ -32,9 +36,10 @@ T2693.hs:19:23: error:
     • Relevant bindings include n :: a5 (bound at T2693.hs:19:7)
 
 T2693.hs:29:20: error:
-    • Couldn't match type ‘TFn a0’ with ‘PVR a1’
-      Expected type: () -> Maybe (PVR a1)
-        Actual type: () -> Maybe (TFn a0)
+    • Couldn't match type: TFn a0
+                     with: PVR a1
+      Expected: () -> Maybe (PVR a1)
+        Actual: () -> Maybe (TFn a0)
       The type variables ‘a0’, ‘a1’ are ambiguous
     • In the first argument of ‘mapM’, namely ‘g’
       In a stmt of a 'do' block: pvs <- mapM g undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T3330a.stderr b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
index dfc2e4223d..1fba198ab7 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
@@ -2,14 +2,13 @@
 T3330a.hs:19:34: error:
     • Couldn't match type ‘ix’
                      with ‘r ix1 -> Writer [AnyF s] (r'0 ix1)’
+      Expected: (s0 ix0 -> ix1) -> r ix1 -> Writer [AnyF s] (r'0 ix1)
+        Actual: s ix
       ‘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:1-43
-      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)’
       In the expression: execWriter (hmapM p collect x)
@@ -21,13 +20,13 @@ T3330a.hs:19:34: error:
 T3330a.hs:19:44: error:
     • Couldn't match type ‘ix’
                      with ‘r0 ix0 -> Writer [AnyF s0] (r0 ix0)’
+      Expected: PF s r (r0 ix0 -> Writer [AnyF s0] (r0 ix0))
+        Actual: PF s r ix
       ‘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:1-43
-      Expected type: PF s r (r0 ix0 -> Writer [AnyF s0] (r0 ix0))
-        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)’
       In the expression: execWriter (hmapM p collect x)
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
index 943dbb148b..9222e6fffe 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -4,8 +4,8 @@ T3330c.hs:25:43: error:
       When matching types
         f1 :: * -> *
         f1 x :: *
-      Expected type: Der ((->) x) (f1 x)
-        Actual type: R f1
+      Expected: Der ((->) x) (f1 x)
+        Actual: 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)
diff --git a/testsuite/tests/indexed-types/should_fail/T4093a.stderr b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
index 826fe1934a..81d9c404ed 100644
--- a/testsuite/tests/indexed-types/should_fail/T4093a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
@@ -5,12 +5,12 @@ T4093a.hs:8:8: error:
         bound by the type signature for:
                    hang :: forall e. (Foo e ~ Maybe e) => Foo e
         at T4093a.hs:7:1-34
+      Expected: Foo e
+        Actual: Maybe ()
       ‘e’ is a rigid type variable bound by
         the type signature for:
           hang :: forall e. (Foo e ~ Maybe e) => Foo e
         at T4093a.hs:7:1-34
-      Expected type: Foo e
-        Actual type: Maybe ()
     • In the expression: Just ()
       In an equation for ‘hang’: hang = Just ()
     • Relevant bindings include hang :: Foo e (bound at T4093a.hs:8:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T4093b.stderr b/testsuite/tests/indexed-types/should_fail/T4093b.stderr
index 195b113ede..367c904e4f 100644
--- a/testsuite/tests/indexed-types/should_fail/T4093b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4093b.stderr
@@ -9,6 +9,8 @@ T4093b.hs:31:13: error:
                                        EitherCO x (A C C n) (A C O n) ~ A C x n) =>
                                       Block n e x -> A e x n
         at T4093b.hs:(19,1)-(22,26)
+      Expected: EitherCO e (A C O n) (A O O n)
+        Actual: (MaybeC C (n C O), MaybeC O (n O C))
       ‘e’ is a rigid type variable bound by
         the type signature for:
           blockToNodeList :: forall (n :: * -> * -> *) e x.
@@ -16,8 +18,6 @@ T4093b.hs:31:13: error:
                               EitherCO x (A C C n) (A C O n) ~ A C x n) =>
                              Block n e x -> A e x n
         at T4093b.hs:(19,1)-(22,26)
-      Expected type: EitherCO e (A C O n) (A O O n)
-        Actual type: (MaybeC C (n C O), MaybeC O (n O C))
     • In the expression: (JustC n, NothingC)
       In an equation for ‘f’: f n _ = (JustC n, NothingC)
       In an equation for ‘blockToNodeList’:
diff --git a/testsuite/tests/indexed-types/should_fail/T4099.stderr b/testsuite/tests/indexed-types/should_fail/T4099.stderr
index acc2ed29ae..5ed4d36640 100644
--- a/testsuite/tests/indexed-types/should_fail/T4099.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4099.stderr
@@ -1,6 +1,7 @@
 
 T4099.hs:11:30: error:
-    • Couldn't match expected type ‘T a0’ with actual type ‘T b’
+    • Couldn't match expected type: T a0
+                  with actual type: T b
       NB: ‘T’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the second argument of ‘foo’, namely ‘x’
@@ -12,7 +13,8 @@ T4099.hs:11:30: error:
         bar1 :: b -> T b -> Int (bound at T4099.hs:11:1)
 
 T4099.hs:14:30: error:
-    • Couldn't match expected type ‘T a1’ with actual type ‘Maybe b’
+    • Couldn't match expected type: T a1
+                  with actual type: Maybe b
       The type variable ‘a1’ is ambiguous
     • In the second argument of ‘foo’, namely ‘x’
       In the expression: foo (error "urk") x
diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr b/testsuite/tests/indexed-types/should_fail/T4174.stderr
index ccc88ced1e..ae962edf36 100644
--- a/testsuite/tests/indexed-types/should_fail/T4174.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr
@@ -1,14 +1,14 @@
 
 T4174.hs:44:12: error:
     • Couldn't match type ‘b’ with ‘RtsSpinLock’
+      Expected: m (Field (Way (GHC6'8 minor) n t p) a b)
+        Actual: m (Field (WayOf m) SmStep 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:43:1-63
-      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
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index 2f0d5e3644..4665a1a321 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -1,12 +1,12 @@
 
 T4179.hs:26:16: error:
-    • 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)))
+    • Couldn't match type: A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                     with: A2 (FCon x)
+      Expected: x (A2 (FCon x) -> A3 (FCon x))
+                -> A2 (FCon x) -> A3 (FCon x)
+        Actual: x (A2 (FCon x) -> A3 (FCon x))
+                -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
       NB: ‘A2’ is a non-injective type family
     • In the first argument of ‘foldDoC’, namely ‘op’
       In the expression: foldDoC op
diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
index f0c5ab57f0..69df514c0f 100644
--- a/testsuite/tests/indexed-types/should_fail/T4272.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -1,9 +1,12 @@
 
 T4272.hs:15:26: error:
-    • Occurs check: cannot construct the infinite type:
-        a ~ TermFamily a a
-      Expected type: TermFamily a (TermFamily a a)
-        Actual type: TermFamily a a
+    • Couldn't match type ‘a’ with ‘TermFamily a a’
+      Expected: TermFamily a (TermFamily a a)
+        Actual: TermFamily a a
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          laws :: forall a b. TermLike a => TermFamily a a -> b
+        at T4272.hs:14:1-53
     • In the first argument of ‘terms’, namely
         ‘(undefined :: TermFamily a a)’
       In the second argument of ‘prune’, namely
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index f712d47f0e..5dcce91edb 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -1,8 +1,8 @@
 
 T5439.hs:82:33: error:
-    • Couldn't match expected type ‘Attempt (HElemOf rs)’
-                  with actual type ‘Attempt (HHead (HDrop n0 l0))
-                                    -> Attempt (HElemOf l0)’
+    • Couldn't match expected type: Attempt (HElemOf rs)
+                  with actual type: Attempt (HHead (HDrop n0 l0))
+                                    -> Attempt (HElemOf l0)
     • In the second argument of ‘($)’, namely
         ‘inj $ Failure (e :: SomeException)’
       In a stmt of a 'do' block:
@@ -21,8 +21,8 @@ T5439.hs:82:33: error:
           (bound at T5439.hs:61:3)
 
 T5439.hs:82:39: error:
-    • Couldn't match expected type ‘Peano n0’
-                  with actual type ‘Attempt α0’
+    • Couldn't match expected type: Peano n0
+                  with actual type: Attempt α0
     • In the second argument of ‘($)’, namely
         ‘Failure (e :: SomeException)’
       In the second argument of ‘($)’, namely
diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr
index e7448a9722..48f8bacef5 100644
--- a/testsuite/tests/indexed-types/should_fail/T5934.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr
@@ -1,7 +1,8 @@
 
 T5934.hs:12:7: error:
-    • Cannot instantiate unification variable ‘a0’
+    • Couldn't match expected type ‘(forall s. GenST s) -> Int’
+                  with actual type ‘a0’
+      Cannot instantiate unification variable ‘a0’
       with a type involving polytypes: (forall s. GenST s) -> Int
-        GHC doesn't yet support impredicative polymorphism
     • In the expression: 0
       In an equation for ‘run’: run = 0
diff --git a/testsuite/tests/indexed-types/should_fail/T6123.stderr b/testsuite/tests/indexed-types/should_fail/T6123.stderr
index 0ae1a5e3c1..eafd27c454 100644
--- a/testsuite/tests/indexed-types/should_fail/T6123.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T6123.stderr
@@ -1,7 +1,6 @@
 
 T6123.hs:10:14: error:
-    • Occurs check: cannot construct the infinite type: a0 ~ Id a0
-        arising from a use of ‘cid’
+    • Couldn't match type ‘a0’ with ‘Id a0’ arising from a use of ‘cid’
       The type variable ‘a0’ is ambiguous
     • In the expression: cid undefined
       In an equation for ‘cundefined’: cundefined = cid undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T7010.stderr b/testsuite/tests/indexed-types/should_fail/T7010.stderr
index 0da40f7a69..12f443df7d 100644
--- a/testsuite/tests/indexed-types/should_fail/T7010.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7010.stderr
@@ -1,8 +1,9 @@
 
 T7010.hs:53:27: error:
-    • Couldn't match type ‘IO Float’ with ‘Serial (IO Float)’
-      Expected type: (Float, ValueTuple Vector)
-        Actual type: (Float, ValueTuple Float)
+    • Couldn't match type: IO Float
+                     with: Serial (IO Float)
+      Expected: (Float, ValueTuple Vector)
+        Actual: (Float, ValueTuple Float)
     • In the first argument of ‘withArgs’, namely ‘plug’
       In the expression: withArgs plug
       In an equation for ‘filterFormants’: filterFormants = withArgs plug
diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr
index b7b70b8f4e..1a20e096f1 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr
@@ -1,9 +1,8 @@
 
 T7354.hs:28:11: error:
-    • Occurs check: cannot construct the infinite type:
-        p ~ Base t (Prim [p] p)
-      Expected type: Prim [p] p -> Base t (Prim [p] p)
-        Actual type: Prim [p] p -> p
+    • Couldn't match type ‘p’ with ‘Base t (Prim [p] p)’
+      Expected: Prim [p] p -> Base t (Prim [p] p)
+        Actual: Prim [p] p -> p
     • In the first argument of ‘ana’, namely ‘alg’
       In the expression: ana alg
       In an equation for ‘foo’: foo = ana alg
diff --git a/testsuite/tests/indexed-types/should_fail/T7729.stderr b/testsuite/tests/indexed-types/should_fail/T7729.stderr
index b209c9c4b7..baf93df666 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729.stderr
@@ -1,8 +1,9 @@
 
 T7729.hs:36:14: error:
-    • Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
-      Expected type: t0 (BasePrimMonad m) a -> Rand m a
-        Actual type: BasePrimMonad (Rand m) a -> Rand m a
+    • Couldn't match type: BasePrimMonad m
+                     with: t0 (BasePrimMonad m)
+      Expected: t0 (BasePrimMonad m) a -> Rand m a
+        Actual: BasePrimMonad (Rand m) a -> Rand m a
       The type variable ‘t0’ is ambiguous
     • In the first argument of ‘(.)’, namely ‘liftPrim’
       In the expression: liftPrim . lift
diff --git a/testsuite/tests/indexed-types/should_fail/T7729a.stderr b/testsuite/tests/indexed-types/should_fail/T7729a.stderr
index e5a6289d96..60be4271ed 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729a.stderr
@@ -1,8 +1,9 @@
 
 T7729a.hs:36:26: error:
-    • Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
-      Expected type: BasePrimMonad (Rand m) a
-        Actual type: t0 (BasePrimMonad m) a
+    • Couldn't match type: BasePrimMonad m
+                     with: t0 (BasePrimMonad m)
+      Expected: BasePrimMonad (Rand m) a
+        Actual: t0 (BasePrimMonad m) a
       The type variable ‘t0’ is ambiguous
     • In the first argument of ‘liftPrim’, namely ‘(lift x)’
       In the expression: liftPrim (lift x)
diff --git a/testsuite/tests/indexed-types/should_fail/T7967.stderr b/testsuite/tests/indexed-types/should_fail/T7967.stderr
index 63d2ba8328..8a7e419a5d 100644
--- a/testsuite/tests/indexed-types/should_fail/T7967.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7967.stderr
@@ -1,7 +1,8 @@
 
 T7967.hs:33:26: error:
-    • Couldn't match type ‘h0 : t0’ with ‘'[]’
-      Expected type: Index n l
-        Actual type: Index 'Zero (h0 : t0)
+    • Couldn't match type: h0 : t0
+                     with: '[]
+      Expected: Index n l
+        Actual: Index 'Zero (h0 : t0)
     • In the expression: IZero
       In an equation for ‘sNatToIndex’: sNatToIndex SZero HNil = IZero
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr
index f86ac68d95..99d1763163 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -1,10 +1,10 @@
 
 T8227.hs:17: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)))
+    • Couldn't match type: Scalar (V a)
+                     with: Scalar (V a) -> Scalar (V a)
+      Expected: Scalar (V a)
+        Actual: 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
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index b18202fec9..1f244f9ee2 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -1,7 +1,7 @@
 
 T8518.hs:14:18: error:
-    • Couldn't match expected type ‘Z c -> B c -> Maybe (F c)’
-                  with actual type ‘F c’
+    • Couldn't match expected type: Z c -> B c -> Maybe (F c)
+                  with actual type: F c
     • The function ‘rpt’ is applied to four value arguments,
         but its type ‘Int -> c -> F c’ has only two
       In the expression: rpt (4 :: Int) c z b
@@ -18,9 +18,10 @@ T8518.hs:14:18: error:
         callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
 
 T8518.hs:16:9: error:
-    • Couldn't match type ‘F t1’ with ‘Z t1 -> B t1 -> F t1’
-      Expected type: t -> t1 -> F t1
-        Actual type: t -> t1 -> Z t1 -> B t1 -> F t1
+    • Couldn't match type: F t1
+                     with: Z t1 -> B t1 -> F t1
+      Expected: t -> t1 -> F t1
+        Actual: t -> t1 -> Z t1 -> B t1 -> F t1
     • In an equation for ‘callCont’:
           callCont c z b
             = rpt (4 :: Int) c z b
diff --git a/testsuite/tests/indexed-types/should_fail/T9036.stderr b/testsuite/tests/indexed-types/should_fail/T9036.stderr
index 151dfb7f2d..0f783738ba 100644
--- a/testsuite/tests/indexed-types/should_fail/T9036.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9036.stderr
@@ -1,9 +1,10 @@
 
 T9036.hs:18:17: error:
-    • Couldn't match type ‘Curried t0 [t0]’ with ‘Curried t [t]’
-      Expected type: Maybe (GetMonad t after) -> Curried t [t]
-        Actual type: Maybe (GetMonad t0 after) -> Curried t0 [t0]
-      NB: ‘Curried’ is a non-injective type family
+    • Couldn't match type: GetMonad t0
+                     with: GetMonad t
+      Expected: Maybe (GetMonad t after) -> Curried t [t]
+        Actual: Maybe (GetMonad t0 after) -> Curried t0 [t0]
+      NB: ‘GetMonad’ is a non-injective type family
       The type variable ‘t0’ is ambiguous
     • In the ambiguity check for ‘simpleLogger’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
diff --git a/testsuite/tests/indexed-types/should_fail/T9171.stderr b/testsuite/tests/indexed-types/should_fail/T9171.stderr
index 320a6add8d..6922be8ade 100644
--- a/testsuite/tests/indexed-types/should_fail/T9171.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9171.stderr
@@ -1,9 +1,9 @@
 
 T9171.hs:10:20: error:
-    • Couldn't match expected type ‘GetParam
-                                      @(*) @k2 @(*) Base (GetParam @(*) @(*) @k2 Base Int)’
-                  with actual type ‘GetParam
-                                      @(*) @k20 @(*) Base (GetParam @(*) @(*) @k20 Base Int)’
+    • Couldn't match expected type: GetParam
+                                      @(*) @k2 @(*) Base (GetParam @(*) @(*) @k2 Base Int)
+                  with actual type: GetParam
+                                      @(*) @k20 @(*) Base (GetParam @(*) @(*) @k20 Base Int)
       NB: ‘GetParam’ is a non-injective type family
       The type variable ‘k20’ is ambiguous
     • In the ambiguity check for an expression type signature
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 4f35d92b5e..04acdc653d 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,17 +1,17 @@
 
 T9662.hs:49:8: error:
-    • Couldn't match type ‘k’ with ‘Int’
-      ‘k’ is a rigid type variable bound by
+    • Couldn't match type ‘n’ with ‘Int’
+      Expected: Exp (((sh :. k) :. m) :. n)
+                -> Exp (((sh :. k) :. m) :. n)
+        Actual: Exp
+                  (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
+                -> Exp
+                     (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
+      ‘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:46:1-50
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> 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)