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
-------------------------

74 files changed, 566 insertions, 181 deletions

diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr
index 5770e03c70..3a5fc99fb3 100644
--- a/testsuite/tests/gadt/T3169.stderr
+++ b/testsuite/tests/gadt/T3169.stderr
@@ -1,17 +1,20 @@
 
-T3169.hs:13:22: error:
+T3169.hs:13:13: error:
     • Couldn't match type ‘elt’ with ‘Map b elt’
-      Expected: Map a (Map b elt)
-        Actual: Map (a, b) elt
+      Expected: Maybe (Map b elt)
+        Actual: Maybe elt
       ‘elt’ is a rigid type variable bound by
         the type signature for:
           lookup :: forall elt. (a, b) -> Map (a, b) elt -> Maybe elt
         at T3169.hs:12:3-8
-    • In the second argument of ‘lookup’, namely ‘m’
-      In the expression: lookup a m :: Maybe (Map b elt)
+    • In the expression: lookup a m :: Maybe (Map b elt)
       In the expression:
         case lookup a m :: Maybe (Map b elt) of {
           Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
+      In an equation for ‘lookup’:
+          lookup (a, b) (m :: Map (a, b) elt)
+            = case lookup a m :: Maybe (Map b elt) of {
+                Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
     • Relevant bindings include
         m :: Map (a, b) elt (bound at T3169.hs:12:17)
         b :: b (bound at T3169.hs:12:13)
diff --git a/testsuite/tests/gadt/T7293.stderr b/testsuite/tests/gadt/T7293.stderr
index 87856d4009..5625ff01c5 100644
--- a/testsuite/tests/gadt/T7293.stderr
+++ b/testsuite/tests/gadt/T7293.stderr
@@ -4,7 +4,7 @@ T7293.hs:26:1: error: [-Woverlapping-patterns (in -Wdefault), -Werror=overlappin
     In an equation for ‘nth’: nth Nil _ = ...
 
 T7293.hs:26:5: error: [-Winaccessible-code (in -Wdefault), -Werror=inaccessible-code]
-    • Couldn't match type ‘'True’ with ‘'False’
+    • Couldn't match type ‘'False’ with ‘'True’
       Inaccessible code in
         a pattern with constructor: Nil :: forall a. Vec a 'Zero,
         in an equation for ‘nth’
diff --git a/testsuite/tests/gadt/T7294.stderr b/testsuite/tests/gadt/T7294.stderr
index d7b53ee9e2..f694af8d0c 100644
--- a/testsuite/tests/gadt/T7294.stderr
+++ b/testsuite/tests/gadt/T7294.stderr
@@ -4,7 +4,7 @@ T7294.hs:27:1: warning: [-Woverlapping-patterns (in -Wdefault)]
     In an equation for ‘nth’: nth Nil _ = ...
 
 T7294.hs:27:5: warning: [-Winaccessible-code (in -Wdefault)]
-    • Couldn't match type ‘'True’ with ‘'False’
+    • Couldn't match type ‘'False’ with ‘'True’
       Inaccessible code in
         a pattern with constructor: Nil :: forall a. Vec a 'Zero,
         in an equation for ‘nth’
diff --git a/testsuite/tests/indexed-types/should_compile/CEqCanOccursCheck.hs b/testsuite/tests/indexed-types/should_compile/CEqCanOccursCheck.hs
new file mode 100644
index 0000000000..f3c9918847
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/CEqCanOccursCheck.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE TypeFamilies #-}
+-- Important: no AllowAmbiguousTypes
+
+module CEqCanOccursCheck where
+
+type family F a where
+  F Bool = Bool
+type family G a b where
+  G a a = a
+
+{-
+[W] F alpha ~ alpha
+[W] F alpha ~ beta
+[W] G alpha beta ~ Int
+-}
+
+foo :: (F a ~ a, F a ~ b) => G a b -> ()
+foo _ = ()
+
+bar :: ()
+bar = foo True
+
+{-
+[G] F a ~ a
+[W] F alpha ~ alpha
+[W] F alpha ~ F a
+-}
+
+notAmbig :: F a ~ a => F a
+notAmbig = undefined
diff --git a/testsuite/tests/indexed-types/should_compile/GivenLoop.hs b/testsuite/tests/indexed-types/should_compile/GivenLoop.hs
new file mode 100644
index 0000000000..d8ece8cb26
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GivenLoop.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module GivenLoop where
+
+type family UnMaybe a where
+  UnMaybe (Maybe b) = b
+
+class C c where
+  meth :: c
+
+instance C (Maybe d) where
+  meth = Nothing
+
+f :: (e ~ Maybe (UnMaybe e)) => e
+f = meth
diff --git a/testsuite/tests/indexed-types/should_compile/Simple13.hs b/testsuite/tests/indexed-types/should_compile/Simple13.hs
index 9e463e8e05..d4e39a9335 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple13.hs
+++ b/testsuite/tests/indexed-types/should_compile/Simple13.hs
@@ -21,7 +21,7 @@ foo p = same p (mkf p)
   [G] g : a ~ [F a]
   [W] w : a ~ [F a]
 
----> 
+--->
   g' = g;[x]                g'=aq4
   [G] g'  : a ~ [fsk]       g=aqW
   [W] x : F a ~ fsk         x=aq3
@@ -36,7 +36,7 @@ foo p = same p (mkf p)
       w = g' ; w2
   [W] w2 : [fsk] ~ [F a]
 
-  --> decompose 
+  --> decompose
        w2 = [w3]
    [W] w3 : fsk ~ F a
 
@@ -44,5 +44,5 @@ foo p = same p (mkf p)
 
 cycle is
    aq3 = Sym (F aq4) ; aq5    x = Sym (F g') ; x2
-   aq4 = apw ; aq3            g' = 
+   aq4 = apw ; aq3            g' =
 -}
diff --git a/testsuite/tests/indexed-types/should_compile/T18875.hs b/testsuite/tests/indexed-types/should_compile/T18875.hs
new file mode 100644
index 0000000000..60fd1cb86a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T18875.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T18875 where
+
+-- This exercises Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
+
+type family G a b where
+  G (Maybe c) d = d
+
+h :: (e ~ Maybe (G e f)) => e -> f
+h (Just x) = x
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
index 20032b6ad4..a860b3c76b 100644
--- a/testsuite/tests/indexed-types/should_compile/T3017.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   insert :: forall c. Coll c => Elem c -> c -> c
   test2 ::
     forall {c} {a} {b}.
-    (Coll c, Num a, Num b, Elem c ~ (a, b)) =>
+    (Elem c ~ (a, b), Coll c, Num a, Num b) =>
     c -> c
 TYPE CONSTRUCTORS
   class Coll{1} :: * -> Constraint
@@ -20,4 +20,4 @@ CLASS INSTANCES
 FAMILY INSTANCES
   type instance Elem (ListColl a) = a -- Defined at T3017.hs:13:9
 Dependent modules: []
-Dependent packages: [base-4.13.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
+Dependent packages: [base-4.15.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 8b3dd5e866..285619f570 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -297,3 +297,6 @@ test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
 test('T17923', normal, compile, [''])
 test('T18065', normal, compile, ['-O'])
 test('T18809', normal, compile, ['-O'])
+test('CEqCanOccursCheck', normal, compile, [''])
+test('GivenLoop', normal, compile, [''])
+test('T18875', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/ExpandTFs.hs b/testsuite/tests/indexed-types/should_fail/ExpandTFs.hs
new file mode 100644
index 0000000000..7a0915d298
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExpandTFs.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, DataKinds #-}
+
+module ExpandTFs where
+
+-- from https://mail.haskell.org/pipermail/ghc-devs/2020-November/019366.html,
+-- where it is requested to expand (Foo Int) in the error message
+
+type family Foo a where Foo Int = String
+type family Bar a :: Maybe (Foo Int) where Bar a = '()
diff --git a/testsuite/tests/indexed-types/should_fail/ExpandTFs.stderr b/testsuite/tests/indexed-types/should_fail/ExpandTFs.stderr
new file mode 100644
index 0000000000..ff2daf734f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/ExpandTFs.stderr
@@ -0,0 +1,6 @@
+
+ExpandTFs.hs:9:52: error:
+    • Couldn't match kind ‘()’ with ‘Maybe String’
+      Expected kind ‘Maybe (Foo Int)’, but ‘'()’ has kind ‘()’
+    • In the type ‘'()’
+      In the type family declaration for ‘Bar’
diff --git a/testsuite/tests/indexed-types/should_fail/Simple13.stderr b/testsuite/tests/indexed-types/should_fail/Simple13.stderr
new file mode 100644
index 0000000000..129ae473c5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/Simple13.stderr
@@ -0,0 +1,13 @@
+
+Simple13.hs:17:17: error:
+    • Couldn't match type: F [F a]
+                     with: F a
+      Expected: a
+        Actual: [F a]
+      NB: ‘F’ is a non-injective type family
+    • In the second argument of ‘same’, namely ‘(mkf p)’
+      In the expression: same p (mkf p)
+      In an equation for ‘foo’: foo p = same p (mkf p)
+    • Relevant bindings include
+        p :: a (bound at Simple13.hs:17:5)
+        foo :: a -> a (bound at Simple13.hs:17:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T13784.stderr b/testsuite/tests/indexed-types/should_fail/T13784.stderr
index 11b1a188f2..04156ccdc9 100644
--- a/testsuite/tests/indexed-types/should_fail/T13784.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13784.stderr
@@ -15,7 +15,7 @@ T13784.hs:29:28: error:
 
 T13784.hs:33:24: error:
     • Couldn't match type: Product (a : as0)
-                     with: (b, Product (Divide b (a : as)))
+                     with: (b, Product (a : Divide b as))
       Expected: (b, Product (Divide b (a : as)))
         Actual: Product (a1 : as0)
     • In the expression: a :* divide as
diff --git a/testsuite/tests/indexed-types/should_fail/T14369.stderr b/testsuite/tests/indexed-types/should_fail/T14369.stderr
index d31a77b2fa..a3a9eb73f7 100644
--- a/testsuite/tests/indexed-types/should_fail/T14369.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14369.stderr
@@ -1,9 +1,20 @@
 
 T14369.hs:29:5: error:
-    • Couldn't match type: Demote a
-                     with: Demote a1
+    • Couldn't match type ‘a’ with ‘a1’
       Expected: Sing x -> Maybe (Demote a1)
         Actual: Sing x -> Demote (Maybe a)
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall {a} (x :: forall a1. Maybe a1) a1.
+               SingKind a1 =>
+               Sing x -> Maybe (Demote a1)
+        at T14369.hs:28:1-80
+      ‘a1’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall {a} (x :: forall a1. Maybe a1) a1.
+               SingKind a1 =>
+               Sing x -> Maybe (Demote a1)
+        at T14369.hs:28:1-80
     • In the expression: fromSing
       In an equation for ‘f’: f = fromSing
     • Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 40409c10cc..721267e75d 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,13 +1,13 @@
 
-T2544.hs:19:18: error:
-    • Couldn't match type: IxMap i0
-                     with: IxMap l
-      Expected: IxMap l [Int]
-        Actual: IxMap i0 [Int]
+T2544.hs:19:12: error:
+    • Couldn't match type: IxMap i1
+                     with: IxMap r
+      Expected: IxMap (l :|: r) [Int]
+        Actual: BiApp (IxMap i0) (IxMap i1) [Int]
       NB: ‘IxMap’ is a non-injective type family
-      The type variable ‘i0’ is ambiguous
-    • In the first argument of ‘BiApp’, namely ‘empty’
-      In the expression: BiApp empty empty
+      The type variable ‘i1’ is ambiguous
+    • In the expression: BiApp empty empty
       In an equation for ‘empty’: empty = BiApp empty empty
+      In the instance declaration for ‘Ix (l :|: r)’
     • Relevant bindings include
         empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.stderr b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
index b69883ab88..2db3dd6397 100644
--- a/testsuite/tests/indexed-types/should_fail/T2627b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
@@ -1,6 +1,6 @@
 
 T2627b.hs:20:24: error:
-    • Could not deduce: Dual (Dual b0) ~ b0
+    • Could not deduce: Dual (Dual a0) ~ a0
         arising from a use of ‘conn’
       from the context: (Dual a ~ b, Dual b ~ a)
         bound by the type signature for:
@@ -13,7 +13,12 @@ T2627b.hs:20:24: error:
                    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
+      or from: b ~ W e f
+        bound by a pattern with constructor:
+                   Wr :: forall e f. e -> Comm f -> Comm (W e f),
+                 in an equation for ‘conn’
+        at T2627b.hs:20:14-19
+      The type variable ‘a0’ is ambiguous
     • In the expression: conn undefined undefined
       In an equation for ‘conn’:
           conn (Rd k) (Wr a r) = conn undefined undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
index 9222e6fffe..3947abddb6 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -3,14 +3,14 @@ T3330c.hs:25:43: error:
     • Couldn't match kind ‘*’ with ‘* -> *’
       When matching types
         f1 :: * -> *
-        f1 x :: *
-      Expected: Der ((->) x) (f1 x)
+        Der f1 x :: *
+      Expected: Der ((->) x) (Der 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)
     • Relevant bindings include
         x :: x (bound at T3330c.hs:25:29)
-        df :: f1 x (bound at T3330c.hs:25:25)
+        df :: Der f1 x (bound at T3330c.hs:25:25)
         rf :: R f1 (bound at T3330c.hs:25:13)
         plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:25:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr b/testsuite/tests/indexed-types/should_fail/T4174.stderr
index ae962edf36..396fab9469 100644
--- a/testsuite/tests/indexed-types/should_fail/T4174.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr
@@ -1,9 +1,9 @@
 
 T4174.hs:44:12: error:
-    • Couldn't match type ‘b’ with ‘RtsSpinLock’
+    • Couldn't match type ‘a’ with ‘SmStep’
       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
+      ‘a’ is a rigid type variable bound by
         the type signature for:
           testcase :: forall (m :: * -> *) minor n t p a b.
                       Monad m =>
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index 4665a1a321..545c03754d 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -1,13 +1,13 @@
 
 T4179.hs:26:16: error:
-    • Couldn't match type: A2 (x (A2 (FCon x) -> A3 (FCon x)))
-                     with: A2 (FCon x)
+    • Couldn't match type: A3 (x (A2 (FCon x) -> A3 (FCon x)))
+                     with: A3 (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
+      NB: ‘A3’ is a non-injective type family
     • In the first argument of ‘foldDoC’, namely ‘op’
       In the expression: foldDoC op
       In an equation for ‘fCon’: fCon = foldDoC op
diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
index 69df514c0f..c921445d2e 100644
--- a/testsuite/tests/indexed-types/should_fail/T4272.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -1,17 +1,16 @@
 
-T4272.hs:15:26: error:
-    • Couldn't match type ‘a’ with ‘TermFamily a a’
-      Expected: TermFamily a (TermFamily a a)
-        Actual: TermFamily a a
+T4272.hs:15:19: error:
+    • Couldn't match expected type ‘TermFamily a a’
+                  with actual type ‘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
+    • In the second argument of ‘prune’, namely
         ‘(terms (undefined :: TermFamily a a))’
       In the expression: prune t (terms (undefined :: TermFamily a a))
+      In an equation for ‘laws’:
+          laws t = prune t (terms (undefined :: TermFamily a a))
     • Relevant bindings include
         t :: TermFamily a a (bound at T4272.hs:15:6)
         laws :: TermFamily a a -> b (bound at T4272.hs:15:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr
index 48f8bacef5..9024f516b8 100644
--- a/testsuite/tests/indexed-types/should_fail/T5934.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr
@@ -1,8 +1,11 @@
 
 T5934.hs:12:7: error:
-    • Couldn't match expected type ‘(forall s. GenST s) -> Int’
-                  with actual type ‘a0’
+    • Couldn't match type ‘a0’
+                     with ‘(forall s. Gen (PrimState (ST s))) -> Int’
+      Expected: (forall s. GenST s) -> Int
+        Actual: a0
       Cannot instantiate unification variable ‘a0’
-      with a type involving polytypes: (forall s. GenST s) -> Int
+      with a type involving polytypes:
+        (forall s. Gen (PrimState (ST s))) -> Int
     • In the expression: 0
       In an equation for ‘run’: run = 0
diff --git a/testsuite/tests/indexed-types/should_fail/T7788.stderr b/testsuite/tests/indexed-types/should_fail/T7788.stderr
index e591fa9b63..65c78aea3b 100644
--- a/testsuite/tests/indexed-types/should_fail/T7788.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7788.stderr
@@ -1,7 +1,7 @@
 
 T7788.hs:9:7: error:
     • Reduction stack overflow; size = 201
-      When simplifying the following type: F (Fix Id)
+      When simplifying the following type: F (Id (Fix Id))
       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
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr
index 99d1763163..0c8cef576d 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -1,10 +1,8 @@
 
 T8227.hs:17:27: error:
-    • 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)))
+    • 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
@@ -13,3 +11,17 @@ T8227.hs:17:27: error:
         eps :: Scalar (V a) (bound at T8227.hs:17:17)
         absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
           (bound at T8227.hs:17:1)
+
+T8227.hs:17:44: error:
+    • Couldn't match expected type: Scalar (V (Scalar (V a)))
+                  with actual type: Scalar (V a)
+      NB: ‘Scalar’ is a non-injective type family
+    • In the first argument of ‘arcLengthToParam’, namely ‘eps’
+      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:17:21)
+        eps :: Scalar (V a) (bound at T8227.hs:17:17)
+        absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
+          (bound at T8227.hs:17:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index 1f244f9ee2..89ba8308a1 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -1,10 +1,9 @@
 
 T8518.hs:14:18: error:
-    • 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
+    • Couldn't match type: F c
+                     with: Z c -> B c -> F c
+        arising from a use of ‘rpt’
+    • In the expression: rpt (4 :: Int) c z b
       In an equation for ‘callCont’:
           callCont c z b
             = rpt (4 :: Int) c z b
@@ -16,17 +15,3 @@ T8518.hs:14:18: error:
         z :: Z c (bound at T8518.hs:14:12)
         c :: c (bound at T8518.hs:14:10)
         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: 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
-            where
-                rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
-                rpt i c' z' b' = let ... in rpt (i - 1) c''
-    • Relevant bindings include
-        rpt :: t -> t1 -> F t1 (bound at T8518.hs:16:9)
diff --git a/testsuite/tests/indexed-types/should_fail/T9554.stderr b/testsuite/tests/indexed-types/should_fail/T9554.stderr
index 2bd5c2ab75..b62badda9d 100644
--- a/testsuite/tests/indexed-types/should_fail/T9554.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9554.stderr
@@ -2,7 +2,7 @@
 T9554.hs:11:9: error:
     • Reduction stack overflow; size = 201
       When simplifying the following type:
-        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       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
@@ -13,7 +13,7 @@ T9554.hs:11:9: error:
 T9554.hs:13:17: error:
     • Reduction stack overflow; size = 201
       When simplifying the following type:
-        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       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
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 428ab8d4f1..9d2c68f095 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -163,3 +163,4 @@ test('T17008a', normal, compile_fail, ['-fprint-explicit-kinds'])
 test('T13571', normal, compile_fail, [''])
 test('T13571a', normal, compile_fail, [''])
 test('T18648', normal, compile_fail, [''])
+test('ExpandTFs', normal, compile_fail, [''])
diff --git a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
index ea48244e0c..7a0ad230f4 100644
--- a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
@@ -65,7 +65,7 @@ SplicesUsed.hs:16:2: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • In the type signature: foo :: _ => _
 
 SplicesUsed.hs:16:2: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Eq a’
+    • Found extra-constraints wildcard standing for ‘Eq a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: Eq a => a -> a -> Bool
                at SplicesUsed.hs:16:2-11
diff --git a/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr b/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
index a11164482c..0f1a1fa77b 100644
--- a/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
@@ -1,4 +1,4 @@
 
 SuperCls.hs:4:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
     • In the type signature: f :: (Ord a, _) => a -> Bool
diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index a3cdc763fc..1a7162d612 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -1,6 +1,6 @@
 
 T10403.hs:15:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Functor f’
+    • Found extra-constraints wildcard standing for ‘Functor f’
       Where: ‘f’ is a rigid type variable bound by
                the inferred type of h1 :: Functor f => (a -> a1) -> f a -> H f
                at T10403.hs:17:1-41
diff --git a/testsuite/tests/partial-sigs/should_compile/T10519.stderr b/testsuite/tests/partial-sigs/should_compile/T10519.stderr
index 13f1104da7..d2db5da38e 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10519.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10519.stderr
@@ -1,6 +1,6 @@
 
 T10519.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Eq a’
+    • Found extra-constraints wildcard standing for ‘Eq a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: Eq a => a -> a -> Bool
                at T10519.hs:5:15
diff --git a/testsuite/tests/partial-sigs/should_compile/T11016.stderr b/testsuite/tests/partial-sigs/should_compile/T11016.stderr
index 49363fb24c..8d3ffe4cf5 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11016.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11016.stderr
@@ -1,6 +1,6 @@
 
 T11016.hs:5:19: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
     • In the type signature: f1 :: (?x :: Int, _) => Int
 
 T11016.hs:8:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
diff --git a/testsuite/tests/partial-sigs/should_compile/T11670.stderr b/testsuite/tests/partial-sigs/should_compile/T11670.stderr
index 87e36e5fc5..2d26722373 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11670.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11670.stderr
@@ -9,7 +9,7 @@ T11670.hs:10:42: warning: [-Wpartial-type-signatures (in -Wdefault)]
         peek :: Ptr a -> IO CLong (bound at T11670.hs:10:1)
 
 T11670.hs:13:40: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Storable w’
+    • Found extra-constraints wildcard standing for ‘Storable w’
       Where: ‘w’ is a rigid type variable bound by
                the inferred type of <expression> :: Storable w => IO w
                at T11670.hs:13:40-48
diff --git a/testsuite/tests/partial-sigs/should_compile/T12844.stderr b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
index 3d8031143c..331570aa93 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12844.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
@@ -1,10 +1,10 @@
 
 T12844.hs:12:9: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’
-        standing for ‘(Foo rngs, Head rngs ~ '(r, r'))’
-      Where: ‘rngs’, ‘k’, ‘r’, ‘k1’, ‘r'’
+    • Found extra-constraints wildcard standing for
+        ‘(Head rngs ~ '(r, r'), Foo rngs)’
+      Where: ‘r’, ‘r'’, ‘k’, ‘k1’, ‘rngs’
                are rigid type variables bound by
                the inferred type of
-                 bar :: (Foo rngs, Head rngs ~ '(r, r')) => FooData rngs
+                 bar :: (Head rngs ~ '(r, r'), Foo rngs) => FooData rngs
                at T12844.hs:(12,1)-(13,9)
     • In the type signature: bar :: _ => FooData rngs
diff --git a/testsuite/tests/partial-sigs/should_compile/T12845.stderr b/testsuite/tests/partial-sigs/should_compile/T12845.stderr
index 0ca72ce5e3..fb7cc70db4 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12845.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12845.stderr
@@ -1,6 +1,6 @@
 
 T12845.hs:18:70: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
     • In the type signature:
         broken :: forall r r' rngs.
                   ('(r, r') ~ Head rngs, Bar r r' ~ 'True, _) =>
diff --git a/testsuite/tests/partial-sigs/should_compile/T13482.stderr b/testsuite/tests/partial-sigs/should_compile/T13482.stderr
index dc2b156703..85cd1115dc 100644
--- a/testsuite/tests/partial-sigs/should_compile/T13482.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T13482.stderr
@@ -1,6 +1,6 @@
 
 T13482.hs:10:32: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘(Eq m, Monoid m)’
+    • Found extra-constraints wildcard standing for ‘(Eq m, Monoid m)’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of
                  minimal1_noksig :: (Eq m, Monoid m) => Int -> Bool
@@ -9,21 +9,21 @@ T13482.hs:10:32: warning: [-Wpartial-type-signatures (in -Wdefault)]
         minimal1_noksig :: forall m. _ => Int -> Bool
 
 T13482.hs:13:33: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘(Eq m, Monoid m)’
+    • Found extra-constraints wildcard standing for ‘(Eq m, Monoid m)’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal1 :: (Eq m, Monoid m) => Bool
                at T13482.hs:13:21
     • In the type signature: minimal1 :: forall (m :: Type). _ => Bool
 
 T13482.hs:16:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Monoid m’
+    • Found extra-constraints wildcard standing for ‘Monoid m’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal2 :: (Eq m, Monoid m) => Bool
                at T13482.hs:16:20
     • In the type signature: minimal2 :: forall m. (Eq m, _) => Bool
 
 T13482.hs:19:34: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Eq m’
+    • Found extra-constraints wildcard standing for ‘Eq m’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal3 :: (Monoid m, Eq m) => Bool
                at T13482.hs:19:20
diff --git a/testsuite/tests/partial-sigs/should_compile/T14217.stderr b/testsuite/tests/partial-sigs/should_compile/T14217.stderr
index 97f7854cdf..913753be98 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14217.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14217.stderr
@@ -1,14 +1,14 @@
 
 T14217.hs:32:11: error:
-    • Found type wildcard ‘_’
-        standing for ‘(Eq a1, Eq a2, Eq a3, Eq a4, Eq a5, Eq a6, Eq a7,
-                       Eq a8, Eq a9, Eq a10, Eq a11, Eq a12, Eq a13, Eq a14, Eq a15,
-                       Eq a16, Eq a17, Eq a18, Eq a19, Eq a20, Eq a21, Eq a22, Eq a23,
-                       Eq a24, Eq a25, Eq a26, Eq a27, Eq a28, Eq a29, Eq a30, Eq a31,
-                       Eq a32, Eq a33, Eq a34, Eq a35, Eq a36, Eq a37, Eq a38, Eq a39,
-                       Eq a40, Eq a41, Eq a42, Eq a43, Eq a44, Eq a45, Eq a46, Eq a47,
-                       Eq a48, Eq a49, Eq a50, Eq a51, Eq a52, Eq a53, Eq a54, Eq a55,
-                       Eq a56, Eq a57, Eq a58, Eq a59, Eq a60, Eq a61, Eq a62, Eq a63)’
+    • Found extra-constraints wildcard standing for
+        ‘(Eq a1, Eq a2, Eq a3, Eq a4, Eq a5, Eq a6, Eq a7, Eq a8, Eq a9,
+          Eq a10, Eq a11, Eq a12, Eq a13, Eq a14, Eq a15, Eq a16, Eq a17,
+          Eq a18, Eq a19, Eq a20, Eq a21, Eq a22, Eq a23, Eq a24, Eq a25,
+          Eq a26, Eq a27, Eq a28, Eq a29, Eq a30, Eq a31, Eq a32, Eq a33,
+          Eq a34, Eq a35, Eq a36, Eq a37, Eq a38, Eq a39, Eq a40, Eq a41,
+          Eq a42, Eq a43, Eq a44, Eq a45, Eq a46, Eq a47, Eq a48, Eq a49,
+          Eq a50, Eq a51, Eq a52, Eq a53, Eq a54, Eq a55, Eq a56, Eq a57,
+          Eq a58, Eq a59, Eq a60, Eq a61, Eq a62, Eq a63)’
       Where: ‘a1’, ‘a2’, ‘a3’, ‘a4’, ‘a5’, ‘a6’, ‘a7’, ‘a8’, ‘a9’, ‘a10’,
              ‘a11’, ‘a12’, ‘a13’, ‘a14’, ‘a15’, ‘a16’, ‘a17’, ‘a18’, ‘a19’,
              ‘a20’, ‘a21’, ‘a22’, ‘a23’, ‘a24’, ‘a25’, ‘a26’, ‘a27’, ‘a28’,
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643.stderr b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
index 60288670fb..e2dd144bd3 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14643.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
@@ -1,8 +1,8 @@
 
 T14643.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
     • In the type signature: ag :: (Num a, _) => a -> a
 
 T14643.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
     • In the type signature: af :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643a.stderr b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
index 1514ac92ed..6f41472472 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
@@ -1,8 +1,8 @@
 
 T14643a.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
     • In the type signature: af :: (Num a, _) => a -> a
 
 T14643a.hs:8:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
     • In the type signature: ag :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T14715.stderr b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
index 901ece018f..e352f0d644 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14715.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
@@ -1,6 +1,7 @@
 
 T14715.hs:13:53: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Reduce (LiftOf zq) zq’
+    • Found extra-constraints wildcard standing for
+        ‘Reduce (LiftOf zq) zq’
       Where: ‘zq’ is a rigid type variable bound by
                the inferred type of
                  bench_mulPublic :: (z ~ LiftOf zq, Reduce (LiftOf zq) zq) =>
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
index e52d911cac..1f07a650ac 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
@@ -48,7 +48,7 @@ T15039a.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         ex6 :: Dict (Coercible a b) -> () (bound at T15039a.hs:33:1)
 
 T15039a.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Coercible a b’
+    • Found extra-constraints wildcard standing for ‘Coercible a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible a b => Coercion a b
                at T15039a.hs:35:1-44
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
index da14f26a17..73d366eb65 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
@@ -49,7 +49,8 @@ T15039b.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         ex6 :: Dict (Coercible @(*) a b) -> () (bound at T15039b.hs:33:1)
 
 T15039b.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Coercible @(*) a b’
+    • Found extra-constraints wildcard standing for
+        ‘Coercible @(*) a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible @(*) a b => Coercion @{*} a b
                at T15039b.hs:35:1-44
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
index c7ad5e861b..658c30c2b7 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
@@ -48,7 +48,7 @@ T15039c.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         ex6 :: Dict (Coercible a b) -> () (bound at T15039c.hs:33:1)
 
 T15039c.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Coercible a b’
+    • Found extra-constraints wildcard standing for ‘Coercible a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible a b => Coercion a b
                at T15039c.hs:35:1-44
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
index 68882c391f..587b64126a 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
@@ -50,7 +50,8 @@ T15039d.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         ex6 :: Dict (Coercible @(*) a b) -> () (bound at T15039d.hs:33:1)
 
 T15039d.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Coercible @(*) a b’
+    • Found extra-constraints wildcard standing for
+        ‘Coercible @(*) a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible @(*) a b => Coercion @{*} a b
                at T15039d.hs:35:1-44
diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
index 5dc9b0797e..e9f875b6a3 100644
--- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
@@ -2,7 +2,7 @@ TYPE SIGNATURES
   bar :: forall {t} {w}. t -> (t -> w) -> w
   foo :: forall {a}. (Show a, Enum a) => a -> String
 Dependent modules: []
-Dependent packages: [base-4.14.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
+Dependent packages: [base-4.15.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
 
 WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_a’ standing for ‘a’
@@ -12,7 +12,7 @@ WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -
     • In the type signature: foo :: (Show _a, _) => _a -> _
 
 WarningWildcardInstantiations.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Enum a’
+    • Found extra-constraints wildcard standing for ‘Enum a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: (Show a, Enum a) => a -> String
                at WarningWildcardInstantiations.hs:6:1-21
diff --git a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr
index 6978418c46..823b1f9e5e 100644
--- a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr
@@ -1,6 +1,6 @@
 
 ExtraConstraintsWildcardInExpressionSignature.hs:5:20: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Eq a1’
+    • Found extra-constraints wildcard standing for ‘Eq a1’
       Where: ‘a1’ is a rigid type variable bound by
                the inferred type of <expression> :: Eq a1 => a1 -> a1 -> Bool
                at ExtraConstraintsWildcardInExpressionSignature.hs:5:20-25
diff --git a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr
index 3fc90ec240..496e1a7393 100644
--- a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr
@@ -1,6 +1,6 @@
 
 ExtraConstraintsWildcardNotEnabled.hs:4:10: error:
-    • Found type wildcard ‘_’ standing for ‘Show a’
+    • Found extra-constraints wildcard standing for ‘Show a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of show' :: Show a => a -> String
                at ExtraConstraintsWildcardNotEnabled.hs:4:1-25
diff --git a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
index 83663188fc..9e9505d7f0 100644
--- a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
@@ -8,7 +8,7 @@ InstantiatedNamedWildcardsInConstraints.hs:4:14: error:
     • In the type signature: foo :: (Enum _a, _) => _a -> (String, b)
 
 InstantiatedNamedWildcardsInConstraints.hs:4:18: error:
-    • Found type wildcard ‘_’ standing for ‘Show b’
+    • Found extra-constraints wildcard standing for ‘Show b’
       Where: ‘b’ is a rigid type variable bound by
                the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
                at InstantiatedNamedWildcardsInConstraints.hs:4:1-40
diff --git a/testsuite/tests/partial-sigs/should_fail/T10999.stderr b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
index b0697fe60b..356b068031 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10999.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
@@ -1,6 +1,6 @@
 
 T10999.hs:5:6: error:
-    • Found type wildcard ‘_’ standing for ‘Ord a’
+    • Found extra-constraints wildcard standing for ‘Ord a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of f :: Ord a => () -> Set.Set a
                at T10999.hs:6:1-28
diff --git a/testsuite/tests/partial-sigs/should_fail/T11515.stderr b/testsuite/tests/partial-sigs/should_fail/T11515.stderr
index 2870457500..df8da03208 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11515.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11515.stderr
@@ -1,5 +1,5 @@
 
 T11515.hs:7:20: error:
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘()’
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: foo :: (ShowSyn a, _) => a -> String
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
index a7e31fd8c9..827356a7ae 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
@@ -8,7 +8,7 @@ WildcardInstantiations.hs:5:14: error:
     • In the type signature: foo :: (Show _a, _) => _a -> _
 
 WildcardInstantiations.hs:5:18: error:
-    • Found type wildcard ‘_’ standing for ‘Enum a’
+    • Found extra-constraints wildcard standing for ‘Enum a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: (Show a, Enum a) => a -> String
                at WildcardInstantiations.hs:6:1-21
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index 0f5d0271b4..3496b04538 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -11,11 +11,9 @@ T14172.hs:6:46: error:
       In the type ‘(a -> f b) -> g a -> f (h _)’
 
 T14172.hs:7:19: error:
-    • Couldn't match type ‘a’ with ‘g'0 a’
-      Expected: (f'0 a -> f (f'0 b)) -> Compose f'0 g'0 a -> f (h a')
-        Actual: (Unwrapped (Compose f'0 g'0 a) -> f (Unwrapped (h a')))
-                -> Compose f'0 g'0 a -> f (h a')
-      ‘a’ is a rigid type variable bound by
+    • Couldn't match type ‘h’ with ‘Compose f'0 g'0’
+        arising from a use of ‘_Wrapping’
+      ‘h’ is a rigid type variable bound by
         the inferred type of
           traverseCompose :: (a -> f b) -> g a -> f (h a')
         at T14172.hs:6:1-47
diff --git a/testsuite/tests/roles/should_compile/Roles3.stderr b/testsuite/tests/roles/should_compile/Roles3.stderr
index bfc62cc196..c3bfb99faa 100644
--- a/testsuite/tests/roles/should_compile/Roles3.stderr
+++ b/testsuite/tests/roles/should_compile/Roles3.stderr
@@ -21,7 +21,7 @@ COERCION AXIOMS
   axiom Roles3.N:C3 :: C3 a b = a -> F3 b -> F3 b
   axiom Roles3.N:C4 :: C4 a b = a -> F4 b -> F4 b
 Dependent modules: []
-Dependent packages: [base-4.15.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
+Dependent packages: [base-4.16.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
 
 ==================== Typechecker ====================
 Roles3.$tcC4
@@ -53,12 +53,12 @@ $krep [InlPrag=[~]] = GHC.Types.KindRepVar 1
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp
       GHC.Types.$tc~ ((:) GHC.Types.krep$* ((:) $krep ((:) $krep [])))
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, [''])