Remove flattening variables

This patch redesigns the flattener to simplify type family applications
directly instead of using flattening meta-variables and skolems. The key new
innovation is the CanEqLHS type and the new CEqCan constraint (Ct). A CanEqLHS
is either a type variable or exactly-saturated type family application; either
can now be rewritten using a CEqCan constraint in the inert set.

Because the flattener no longer reduces all type family applications to
variables, there was some performance degradation if a lengthy type family
application is now flattened over and over (not making progress). To
compensate, this patch contains some extra optimizations in the flattener,
leading to a number of performance improvements.

Close #18875.
Close #18910.

There are many extra parts of the compiler that had to be affected in writing
this patch:

* The family-application cache (formerly the flat-cache) sometimes stores
  coercions built from Given inerts. When these inerts get kicked out, we must
  kick out from the cache as well. (This was, I believe, true previously, but
  somehow never caused trouble.) Kicking out from the cache requires adding a
  filterTM function to TrieMap.

* This patch obviates the need to distinguish "blocking" coercion holes from
  non-blocking ones (which, previously, arose from CFunEqCans). There is thus
  some simplification around coercion holes.

* Extra commentary throughout parts of the code I read through, to preserve
  the knowledge I gained while working.

* A change in the pure unifier around unifying skolems with other types.
  Unifying a skolem now leads to SurelyApart, not MaybeApart, as documented
  in Note [Binding when looking up instances] in GHC.Core.InstEnv.

* Some more use of MCoercion where appropriate.

* Previously, class-instance lookup automatically noticed that e.g. C Int was
  a "unifier" to a target [W] C (F Bool), because the F Bool was flattened to
  a variable. Now, a little more care must be taken around checking for
  unifying instances.

* Previously, tcSplitTyConApp_maybe would split (Eq a => a). This is silly,
  because (=>) is not a tycon in Haskell. Fixed now, but there are some
  knock-on changes in e.g. TrieMap code and in the canonicaliser.

* New function anyFreeVarsOf{Type,Co} to check whether a free variable
  satisfies a certain predicate.

* Type synonyms now remember whether or not they are "forgetful"; a forgetful
  synonym drops at least one argument. This is useful when flattening; see
  flattenView.

* The pattern-match completeness checker invokes the solver. This invocation
  might need to look through newtypes when checking representational equality.
  Thus, the desugarer needs to keep track of the in-scope variables to know
  what newtype constructors are in scope. I bet this bug was around before but
  never noticed.

* Extra-constraints wildcards are no longer simplified before printing.
  See Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.

* Whether or not there are Given equalities has become slightly subtler.
  See the new HasGivenEqs datatype.

* Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
  explains a significant new wrinkle in the new approach.

* See Note [What might match later?] in GHC.Tc.Solver.Interact, which
  explains the fix to #18910.

* The inert_count field of InertCans wasn't actually used, so I removed
  it.

Though I (Richard) did the implementation, Simon PJ was very involved
in design and review.

This updates the Haddock submodule to avoid #18932 by adding
a type signature.

-------------------------
Metric Decrease:
    T12227
    T5030
    T9872a
    T9872b
    T9872c
Metric Increase:
    T9872d
-------------------------

22 files changed, 340 insertions, 62 deletions

diff --git a/testsuite/tests/typecheck/should_compile/CbvOverlap.hs b/testsuite/tests/typecheck/should_compile/CbvOverlap.hs
new file mode 100644
index 0000000000..4e3b40f161
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/CbvOverlap.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}
+
+module CbvOverlap where
+
+-- This is concerned with Note [Type variable cycles in Givens] and class lookup
+
+class C a where
+  meth :: a -> ()
+
+instance C Int where
+  meth _ = ()
+
+type family F a
+
+foo :: C (F a) => a -> Int -> ()
+foo _ n = meth n
diff --git a/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs
new file mode 100644
index 0000000000..765379a203
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses,
+             TypeFamilies, FlexibleContexts, AllowAmbiguousTypes #-}
+
+module InstanceGivenOverlap where
+
+-- See Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
+-- This tests the Note when the Wanted contains a type family.
+
+class P a
+class Q a
+class R a b
+
+instance P x => Q [x]
+instance (x ~ y) => R y [x]
+
+type family F a b where
+  F [a] a = a
+
+wob :: forall a b. (Q [F a b], R b a) => a -> Int
+wob = undefined
+
+g :: forall a. Q [a] => [a] -> Int
+g x = wob x
diff --git a/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs
new file mode 100644
index 0000000000..67c475ee23
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
+             TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
+             MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module InstanceGivenOverlap2 where
+
+import Data.Proxy
+
+class P a
+class Q a
+class R a b
+
+newtype Tagged (t :: k) a = Tagged a
+
+type family F a
+type instance F (Tagged @Bool t a) = [a]
+
+instance P x => Q [x]
+instance (x ~ y) => R y [x]
+
+wob :: forall a b. (Q [b], R b a) => a -> Int
+wob = undefined
+
+it'sABoolNow :: forall (t :: Bool). Int
+it'sABoolNow = undefined
+
+class HasBoolKind t
+instance k ~ Bool => HasBoolKind (t :: k)
+
+it'sABoolLater :: forall t. HasBoolKind t => Int
+it'sABoolLater = undefined
+
+g :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g _ x = it'sABoolNow @t + wob x
+
+g2 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g2 _ x = wob x + it'sABoolNow @t
+
+g3 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g3 _ x = it'sABoolLater @t + wob x
+
+g4 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
+g4 _ x = wob x + it'sABoolLater @t
diff --git a/testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs b/testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
new file mode 100644
index 0000000000..f1280205b2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE RankNTypes, TypeFamilies, FlexibleInstances #-}
+{-# OPTIONS_GHC -Wno-missing-methods -Wno-unused-matches #-}
+
+module LocalGivenEqs where
+
+-- See Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad;
+-- this tests custom treatment for LocalGivenEqs
+
+{-
+I (Richard E) tried somewhat half-heartedly to minimize this, but failed.
+The key bit is the use of the ECP constructor inside the lambda in happyReduction_508.
+(The lack of a type signature on that is not at issue, I believe.) The type
+of ECP is
+  (forall b. DisambECP b => PV (Located b)) -> ECP
+So, the argument to ECP gets a [G] DisambECP b, which (via its superclass) grants
+us [G] b ~ (Body b) GhcPs. In order to infer the type of happy_var_2, we need to
+float some wanted out past this equality. We have Note [Let-bound skolems]
+in GHC.Tc.Solver.Monad to consider this Given equality to be let-like, and thus
+not prevent floating. But, note that the equality isn't quite let-like, because
+it mentions b in its RHS. It thus triggers Note [Type variable cycles in Givens]
+in GHC.Tc.Solver.Canonical. That Note says we change the situation to
+  [G] b ~ cbv GhcPs
+  [G] Body b ~ cbv
+for some fresh CycleBreakerTv cbv. Now, our original equality looks to be let-like,
+but the new cbv equality is *not* let-like -- note that the variable is on the RHS.
+The solution is to consider any equality whose free variables are all at the current
+level to not stop equalities from floating. These are called *local*. Because both
+Givens are local in this way, they no longer prevent floating, and we can type-check
+this example.
+-}
+
+import Data.Kind ( Type )
+import GHC.Exts ( Any )
+
+infixr 9 `HappyStk`
+data HappyStk a = HappyStk a (HappyStk a)
+newtype HappyWrap201 = HappyWrap201 (ECP)
+newtype HappyWrap205 = HappyWrap205 (([Located Token],Bool))
+
+newtype HappyAbsSyn  = HappyAbsSyn HappyAny
+type HappyAny = Any
+
+newtype ECP =
+  ECP { unECP :: forall b. DisambECP b => PV (Located b) }
+
+data PV a
+data P a
+data GhcPs
+data Token
+data Located a
+data AnnKeywordId = AnnIf | AnnThen | AnnElse | AnnSemi
+data AddAnn
+data SrcSpan
+type LHsExpr a = Located (HsExpr a)
+data HsExpr a
+
+class b ~ (Body b) GhcPs => DisambECP b where
+  type Body b :: Type -> Type
+  mkHsIfPV :: SrcSpan
+         -> LHsExpr GhcPs
+         -> Bool  -- semicolon?
+         -> Located b
+         -> Bool  -- semicolon?
+         -> Located b
+         -> PV (Located b)
+
+instance DisambECP (HsExpr GhcPs) where
+  type Body (HsExpr GhcPs) = HsExpr
+  mkHsIfPV = undefined
+
+instance Functor P
+instance Applicative P
+instance Monad P
+
+instance Functor PV
+instance Applicative PV
+instance Monad PV
+
+mj :: AnnKeywordId -> Located e -> AddAnn
+mj = undefined
+
+amms :: Monad m => m (Located a) -> [AddAnn] -> m (Located a)
+amms = undefined
+
+happyIn208 :: ECP -> HappyAbsSyn
+happyIn208 = undefined
+
+happyReturn :: () => a -> P a
+happyReturn = (return)
+
+happyThen :: () => P a -> (a -> P b) -> P b
+happyThen = (>>=)
+
+comb2 :: Located a -> Located b -> SrcSpan
+comb2 = undefined
+
+runPV :: PV a -> P a
+runPV = undefined
+
+happyOutTok :: HappyAbsSyn -> Located Token
+happyOutTok = undefined
+
+happyOut201 :: HappyAbsSyn -> HappyWrap201
+happyOut201 = undefined
+
+happyOut205 :: HappyAbsSyn -> HappyWrap205
+happyOut205 = undefined
+
+happyReduction_508 (happy_x_8 `HappyStk`
+        happy_x_7 `HappyStk`
+        happy_x_6 `HappyStk`
+        happy_x_5 `HappyStk`
+        happy_x_4 `HappyStk`
+        happy_x_3 `HappyStk`
+        happy_x_2 `HappyStk`
+        happy_x_1 `HappyStk`
+        happyRest) tk
+         = happyThen ((case happyOutTok happy_x_1 of { happy_var_1 ->
+        case happyOut201 happy_x_2 of { (HappyWrap201 happy_var_2) ->
+        case happyOut205 happy_x_3 of { (HappyWrap205 happy_var_3) ->
+        case happyOutTok happy_x_4 of { happy_var_4 ->
+        case happyOut201 happy_x_5 of { (HappyWrap201 happy_var_5) ->
+        case happyOut205 happy_x_6 of { (HappyWrap205 happy_var_6) ->
+        case happyOutTok happy_x_7 of { happy_var_7 ->
+        case happyOut201 happy_x_8 of { (HappyWrap201 happy_var_8) ->
+                          -- uncomment this next signature to avoid the need
+                          -- for special treatment of floating described above
+        ( runPV (unECP happy_var_2 {- :: PV (LHsExpr GhcPs) -}) >>= \ happy_var_2 ->
+                            return $ ECP $
+                              unECP happy_var_5 >>= \ happy_var_5 ->
+                              unECP happy_var_8 >>= \ happy_var_8 ->
+                              amms (mkHsIfPV (comb2 happy_var_1 happy_var_8) happy_var_2 (snd happy_var_3) happy_var_5 (snd happy_var_6) happy_var_8)
+                                  (mj AnnIf happy_var_1:mj AnnThen happy_var_4
+                                     :mj AnnElse happy_var_7
+                                     :(map (\l -> mj AnnSemi l) (fst happy_var_3))
+                                    ++(map (\l -> mj AnnSemi l) (fst happy_var_6))))}}}}}}}})
+        ) (\r -> happyReturn (happyIn208 r))
diff --git a/testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs b/testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs
new file mode 100644
index 0000000000..f15ab92de7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/LocalGivenEqs2.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, GADTSyntax, ExistentialQuantification #-}
+
+-- This is a simple case that exercises the LocalGivenEqs bullet
+-- of Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad
+-- If a future change rejects this, that's not the end of the world, but it's nice
+-- to be able to infer `f`.
+
+module LocalGivenEqs2 where
+
+type family F a
+type family G b
+
+data T where
+  MkT :: F a ~ G b => a -> b -> T
+
+f (MkT _ _) = True
diff --git a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr
index bde2a0d703..0f1fd3e6c2 100644
--- a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr
+++ b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr
@@ -8,13 +8,3 @@ PolytypeDecomp.hs:30:17: error:
     • In the expression: x
       In the first argument of ‘myLength’, namely ‘[x, f]’
       In the expression: myLength [x, f]
-
-PolytypeDecomp.hs:30:19: error:
-    • Couldn't match type ‘a0’ with ‘[forall a. F [a]]’
-      Expected: Id a0
-        Actual: [forall a. F [a]]
-      Cannot instantiate unification variable ‘a0’
-      with a type involving polytypes: [forall a. F [a]]
-    • In the expression: f
-      In the first argument of ‘myLength’, namely ‘[x, f]’
-      In the expression: myLength [x, f]
diff --git a/testsuite/tests/typecheck/should_compile/T13651.stderr b/testsuite/tests/typecheck/should_compile/T13651.stderr
index 150291c210..cc7af849d3 100644
--- a/testsuite/tests/typecheck/should_compile/T13651.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13651.stderr
@@ -1,6 +1,6 @@
 
 T13651.hs:11:8: error:
-    • Could not deduce: F cr (Bar (Foo h) (Foo u)) ~ Bar h (Bar r u)
+    • Could not deduce: F cr (Bar h (Foo u)) ~ Bar h (Bar r u)
       from the context: (F cr cu ~ Bar h (Bar r u),
                          F cu cs ~ Bar (Foo h) (Bar u s))
         bound by the type signature for:
diff --git a/testsuite/tests/typecheck/should_compile/T15368.stderr b/testsuite/tests/typecheck/should_compile/T15368.stderr
index 7f022744c4..33b0407730 100644
--- a/testsuite/tests/typecheck/should_compile/T15368.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15368.stderr
@@ -15,8 +15,8 @@ T15368.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
         trigger :: a -> b -> (F a b, F b a) (bound at T15368.hs:11:1)
 
 T15368.hs:11:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type: F b a
-                     with: F b0 a0
+    • Couldn't match type: F b0 a0
+                     with: F b a
       Expected: (F a b, F b a)
         Actual: (F a b, F b0 a0)
       NB: ‘F’ is a non-injective type family
diff --git a/testsuite/tests/typecheck/should_compile/T5490.hs b/testsuite/tests/typecheck/should_compile/T5490.hs
index b5b7a2d98c..5679ee9baa 100644
--- a/testsuite/tests/typecheck/should_compile/T5490.hs
+++ b/testsuite/tests/typecheck/should_compile/T5490.hs
@@ -16,7 +16,7 @@ import Data.Functor
 import Control.Exception
 
 data Attempt α = Success α
-               | ∀ e . Exception e ⇒ Failure e 
+               | ∀ e . Exception e ⇒ Failure e
 
 fromAttempt ∷ Attempt α → IO α
 fromAttempt (Success a) = return a
@@ -136,7 +136,7 @@ instance IsPeano PZero where
   peano = PZero
 
 instance IsPeano p ⇒ IsPeano (PSucc p) where
-  peano = PSucc peano 
+  peano = PSucc peano
 
 class (n ~ PSucc (PPred n)) ⇒ PHasPred n where
   type PPred n
@@ -297,4 +297,3 @@ hGetIfNth _        _                  = Nothing
 
 elem0 ∷ HNonEmpty l ⇒ HElemOf l → Maybe (HHead l)
 elem0 = hGetIfNth PZero
-
diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr
index 5963781325..2c410de0f2 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9834.stderr
@@ -1,11 +1,14 @@
 
 T9834.hs:23:12: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘p’ with ‘(->) (p a0)’
+    • Couldn't match type ‘a’ with ‘p a0’
       Expected: p a
         Actual: p a0 -> p a0
-      ‘p’ is a rigid type variable bound by
-        the class declaration for ‘ApplicativeFix’
-        at T9834.hs:21:39
+      ‘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-74
     • In the expression: wrapIdComp f
       In an equation for ‘afix’: afix f = wrapIdComp f
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
index a7645a0b3e..3984df496a 100644
--- a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
@@ -20,4 +20,4 @@ data family D (a :: TYPE r) :: TYPE r
 newtype instance D a = MkWordD Word#
 
 newtype instance D a :: TYPE (KindOf a) where
-  MkIntD :: forall (a :: TYPE 'IntRep). Int# -> D a
+  MkIntD :: forall a. Int# -> D a
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 08f4b803c8..5aeb4d0a58 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -731,3 +731,8 @@ test('T18939_Compile', normal, compile, [''])
 test('T15942', normal, compile, [''])
 test('ClassDefaultInHsBoot', [extra_files(['ClassDefaultInHsBootA1.hs','ClassDefaultInHsBootA2.hs','ClassDefaultInHsBootA2.hs-boot','ClassDefaultInHsBootA3.hs'])], multimod_compile, ['ClassDefaultInHsBoot', '-v0'])
 test('T17186', normal, compile, [''])
+test('CbvOverlap', normal, compile, [''])
+test('InstanceGivenOverlap', normal, compile, [''])
+test('InstanceGivenOverlap2', normal, compile, [''])
+test('LocalGivenEqs', normal, compile, [''])
+test('LocalGivenEqs2', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.hs b/testsuite/tests/typecheck/should_fail/ContextStack2.hs
index 53634a5cd5..0e01ab6956 100644
--- a/testsuite/tests/typecheck/should_fail/ContextStack2.hs
+++ b/testsuite/tests/typecheck/should_fail/ContextStack2.hs
@@ -12,11 +12,11 @@ type instance TF (a,b) = (TF a, TF b)
 t :: (a ~ TF (a,Int)) => Int
 t = undefined
 
-{- a ~ TF (a,Int)  
+{- a ~ TF (a,Int)
      ~ (TF a, TF Int)
      ~ (TF (TF (a,Int)), TF Int)
      ~ (TF (TF a, TF Int), TF Int)
-     ~ ((TF (TF a), TF (TF Int)), TF Int) 
+     ~ ((TF (TF a), TF (TF Int)), TF Int)
 
 
       fsk ~ a
@@ -28,7 +28,7 @@ t = undefined
          a ~ (TF a, TF Int)
         (flatten rhs)
         a ~ (fsk1, TF Int)
-(wk)  TF a ~ fsk1   
+(wk)  TF a ~ fsk1
 
 --> (rewrite inert)
 
@@ -43,7 +43,7 @@ t = undefined
 *     TF (fsk1, fsk2) ~ fsk1
 (wk)  TF Tnt ~ fsk2
 
--->   
+-->
       fsk ~ (fsk1, TF Int)
       a   ~ (fsk1, TF Int)
 
@@ -51,7 +51,7 @@ t = undefined
         (flatten rhs)
         fsk1 ~ (fsk3, TF fsk2)
 
-   
+
 (wk)  TF Int ~ fsk2
       TF fsk1 ~ fsk3
 -}
diff --git a/testsuite/tests/typecheck/should_fail/GivenForallLoop.hs b/testsuite/tests/typecheck/should_fail/GivenForallLoop.hs
new file mode 100644
index 0000000000..a5f109949c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/GivenForallLoop.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies, ImpredicativeTypes #-}
+
+module GivenForallLoop where
+
+type family F a b
+
+loopy :: (a ~ (forall b. F a b)) => a -> b
+loopy x = x
diff --git a/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
new file mode 100644
index 0000000000..e4260e62ed
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
@@ -0,0 +1,20 @@
+
+GivenForallLoop.hs:8:11: error:
+    • Could not deduce: a ~ b
+      from the context: a ~ (forall b1. F a b1)
+        bound by the type signature for:
+                   loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+        at GivenForallLoop.hs:7:1-42
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+        at GivenForallLoop.hs:7:1-42
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+        at GivenForallLoop.hs:7:1-42
+    • In the expression: x
+      In an equation for ‘loopy’: loopy x = x
+    • Relevant bindings include
+        x :: a (bound at GivenForallLoop.hs:8:7)
+        loopy :: a -> b (bound at GivenForallLoop.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr
index 3599acef73..c1d751bee2 100644
--- a/testsuite/tests/typecheck/should_fail/T15629.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15629.stderr
@@ -1,17 +1,26 @@
 
-T15629.hs:26:37: error:
+T15629.hs:26:31: error:
     • Couldn't match kind ‘z’ with ‘ab’
-      Expected kind ‘x ~> F x ab’,
-        but ‘F1Sym :: x ~> F x z’ has kind ‘x ~> F x z’
+      Expected kind ‘F x ab ~> F x ab’,
+        but ‘Comp (F1Sym :: x ~> F x z) F2Sym’ has kind ‘TyFun
+                                                           (F x ab) (F x z)
+                                                         -> *’
       ‘z’ is a rigid type variable bound by
         an explicit forall z ab
         at T15629.hs:26:17
       ‘ab’ is a rigid type variable bound by
         an explicit forall z ab
         at T15629.hs:26:19-20
-    • In the first argument of ‘Comp’, namely ‘(F1Sym :: x ~> F x z)’
-      In the first argument of ‘Proxy’, namely
+    • In the first argument of ‘Proxy’, namely
         ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’
       In the type signature:
-        g :: forall z ab. Proxy ((Comp (F1Sym :: x
-                                                 ~> F x z) F2Sym) :: F x ab ~> F x ab)
+        g :: forall z ab.
+             Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+      In an equation for ‘f’:
+          f _
+            = ()
+            where
+                g ::
+                  forall z ab.
+                  Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+                g = sg Proxy Proxy
diff --git a/testsuite/tests/typecheck/should_fail/T16512a.stderr b/testsuite/tests/typecheck/should_fail/T16512a.stderr
index f18e9738bf..a799bcca21 100644
--- a/testsuite/tests/typecheck/should_fail/T16512a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16512a.stderr
@@ -1,12 +1,16 @@
 
 T16512a.hs:41:25: error:
-    • Reduction stack overflow; size = 201
-      When simplifying the following type: ListVariadic as b
-      Use -freduction-depth=0 to disable this check
-      (any upper bound you could choose might fail unpredictably with
-       minor updates to GHC, so disabling the check is recommended if
-       you're sure that type checking should terminate)
+    • Couldn't match type: ListVariadic as (a -> b)
+                     with: a -> ListVariadic as b
+      Expected: AST (ListVariadic (a : as) b)
+        Actual: AST (ListVariadic as (a -> b))
     • In the first argument of ‘AnApplication’, namely ‘g’
       In the expression: AnApplication g (a `ConsAST` as)
       In a case alternative:
           AnApplication g as -> AnApplication g (a `ConsAST` as)
+    • Relevant bindings include
+        as :: ASTs as (bound at T16512a.hs:40:25)
+        g :: AST (ListVariadic as (a -> b)) (bound at T16512a.hs:40:23)
+        a :: AST a (bound at T16512a.hs:38:15)
+        f :: AST (a -> b) (bound at T16512a.hs:38:10)
+        unapply :: AST b -> AnApplication b (bound at T16512a.hs:38:1)
diff --git a/testsuite/tests/typecheck/should_fail/T3406.stderr b/testsuite/tests/typecheck/should_fail/T3406.stderr
index 70fffee3ac..70791b2cdc 100644
--- a/testsuite/tests/typecheck/should_fail/T3406.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3406.stderr
@@ -1,6 +1,6 @@
 
 T3406.hs:11:28: error:
-    • Couldn't match type ‘Int’ with ‘a -> ItemColID a b’
+    • Couldn't match type ‘Int’ with ‘a -> Int’
       Expected: a -> ItemColID a b
         Actual: ItemColID a1 b1
     • In the expression: x :: ItemColID a b
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index 5d42625796..b25e1fca91 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,16 +1,18 @@
 
 T5853.hs:15:52: error:
-    • Could not deduce: Subst (Subst fa a) b ~ Subst fa b
+    • Could not deduce: Subst fa1 (Elem fb) ~ fb
         arising from a use of ‘<$>’
-      from the context: (F fa, Elem (Subst fa b) ~ b,
-                         Subst fa b ~ Subst fa b, Subst (Subst fa b) (Elem fa) ~ fa,
-                         F (Subst fa a), Elem (Subst fa a) ~ a, Elem fa ~ Elem fa,
-                         Subst (Subst fa a) (Elem fa) ~ fa, Subst fa a ~ Subst fa a)
+      from the context: (F fa, Elem fb ~ Elem fb,
+                         Subst fa (Elem fb) ~ fb, Subst fb (Elem fa) ~ fa, F fa1,
+                         Elem fa1 ~ Elem fa1, Elem fa ~ Elem fa, Subst fa1 (Elem fa) ~ fa,
+                         Subst fa (Elem fa1) ~ fa1)
         bound by the RULE "map/map" at T5853.hs:15:2-57
-      NB: ‘Subst’ is a non-injective type family
+      ‘fb’ is a rigid type variable bound by
+        the RULE "map/map"
+        at T5853.hs:15:2-57
     • In the expression: (f . g) <$> xs
       When checking the rewrite rule "map/map"
     • Relevant bindings include
-        f :: Elem fa -> b (bound at T5853.hs:15:19)
-        g :: a -> Elem fa (bound at T5853.hs:15:21)
-        xs :: Subst fa a (bound at T5853.hs:15:23)
+        f :: Elem fa -> Elem fb (bound at T5853.hs:15:19)
+        g :: Elem fa1 -> Elem fa (bound at T5853.hs:15:21)
+        xs :: fa1 (bound at T5853.hs:15:23)
diff --git a/testsuite/tests/typecheck/should_fail/T8142.stderr b/testsuite/tests/typecheck/should_fail/T8142.stderr
index a9f4590e44..a362d35367 100644
--- a/testsuite/tests/typecheck/should_fail/T8142.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8142.stderr
@@ -1,10 +1,10 @@
 
 T8142.hs:6:10: error:
-    • Couldn't match type: Nu ((,) a0)
+    • Couldn't match type: Nu f0
                      with: c -> f c
       Expected: (c -> f c) -> c -> f c
         Actual: Nu ((,) a0) -> Nu f0
-      The type variable ‘a0’ is ambiguous
+      The type variable ‘f0’ is ambiguous
     • In the expression: h
       In an equation for ‘tracer’:
           tracer
@@ -12,15 +12,17 @@ T8142.hs:6:10: error:
             where
                 h = (\ (_, b) -> ((outI . fmap h) b)) . out
     • Relevant bindings include
+        h :: Nu ((,) a0) -> Nu f0 (bound at T8142.hs:6:18)
         tracer :: (c -> f c) -> c -> f c (bound at T8142.hs:6:1)
 
 T8142.hs:6:57: error:
-    • Couldn't match type: Nu ((,) a)
-                     with: f1 (Nu ((,) a))
-      Expected: Nu ((,) a) -> (a, f1 (Nu ((,) a)))
-        Actual: Nu ((,) a) -> (a, Nu ((,) a))
+    • Couldn't match type: Nu ((,) a0)
+                     with: f0 (Nu ((,) a0))
+      Expected: Nu ((,) a0) -> (a0, f0 (Nu ((,) a0)))
+        Actual: Nu ((,) a0) -> (a0, Nu ((,) a0))
+      The type variables ‘f0’, ‘a0’ are ambiguous
     • In the second argument of ‘(.)’, namely ‘out’
       In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
       In an equation for ‘h’: h = (\ (_, b) -> ((outI . fmap h) b)) . out
     • Relevant bindings include
-        h :: Nu ((,) a) -> Nu f1 (bound at T8142.hs:6:18)
+        h :: Nu ((,) a0) -> Nu f0 (bound at T8142.hs:6:18)
diff --git a/testsuite/tests/typecheck/should_fail/T9260.stderr b/testsuite/tests/typecheck/should_fail/T9260.stderr
index 2a6c0ac16c..b3752e4279 100644
--- a/testsuite/tests/typecheck/should_fail/T9260.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9260.stderr
@@ -1,8 +1,7 @@
 
-T9260.hs:12:14: error:
-    • Couldn't match type ‘1’ with ‘0’
-      Expected: Fin 0
-        Actual: Fin (0 + 1)
-    • In the first argument of ‘Fsucc’, namely ‘Fzero’
-      In the expression: Fsucc Fzero
+T9260.hs:12:8: error:
+    • Couldn't match type ‘2’ with ‘1’
+      Expected: Fin 1
+        Actual: Fin ((0 + 1) + 1)
+    • In the expression: Fsucc Fzero
       In an equation for ‘test’: test = Fsucc Fzero
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 5ce09273a2..958811d428 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -590,3 +590,4 @@ test('T18640b', normal, compile_fail, [''])
 test('T18640c', normal, compile_fail, [''])
 test('T10709', normal, compile_fail, [''])
 test('T10709b', normal, compile_fail, [''])
+test('GivenForallLoop', normal, compile_fail, [''])