Orient TyVar/TyVar equalities with deepest on the left

Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
want to orient them with the deepest-bound skolem on the left. As it
happens, we also want to do the same for Wanteds, but for a different
reason (more likely to be touchable).  Either way, deepest wins:
see TcUnify Note [Deeper level on the left].

This observation led me to some significant changes:

* A SkolemTv already had a TcLevel, but the level wasn't really being
  used.   Now it is!

* I updated added invariant (SkolInf) to TcType
  Note [TcLevel and untouchable type variables], documenting that
  the level number of all the ic_skols should be the same as the
  ic_tclvl of the implication

* FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
  zero, which messed the scheme up.   Now they get a level number the
  same way as all other TcTyVars, instead of being a special case.

* To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
  was previously done via their magic zero level) isTouchableMetaTyVar
  just tests for those two cases.

* TcUnify.swapOverTyVars is the crucial orientation function; see the
  new Note [TyVar/TyVar orientation].  I completely rewrote this function,
  and it's now much much easier to understand.

I ended up doing some related refactoring, of course

* I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
  a lot of useless work in the case where there are no skolems; I
  added a fast-patch

* Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
  the higher-order parameter to tcExpliciTKBndrsX.

* Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
  by analogy with TcUnify.checkConstraints.

* Inline TcUnify.buildImplication into its only call-site in
  TcUnify.checkConstraints

* TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
  simpler API

* Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
  nuke the latter, adding Note [No evidence bindings] to TcEvidence.

28 files changed, 189 insertions, 154 deletions

diff --git a/testsuite/tests/ado/T13242a.stderr b/testsuite/tests/ado/T13242a.stderr
index c3dbbba970..e03f471e8b 100644
--- a/testsuite/tests/ado/T13242a.stderr
+++ b/testsuite/tests/ado/T13242a.stderr
@@ -1,8 +1,7 @@
 
 T13242a.hs:10:5: error:
     • Couldn't match expected type ‘a0’ with actual type ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a’ is a rigid type variable bound by
         a pattern with constructor: A :: forall a. Eq a => a -> T,
         in a pattern binding in
              'do' block
@@ -28,7 +27,7 @@ T13242a.hs:13:11: error:
       These potential instances exist:
         instance Eq Ordering -- Defined in ‘GHC.Classes’
         instance Eq Integer
-          -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
+          -- Defined in ‘integer-gmp-1.0.2.0:GHC.Integer.Type’
         instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
         ...plus 22 others
         ...plus six instances involving out-of-scope types
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
index 3a8b90edce..3f5eb9825a 100644
--- a/testsuite/tests/dependent/should_fail/T14066d.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -1,14 +1,14 @@
 
 T14066d.hs:11:35: error:
-    • Couldn't match type ‘b’ with ‘b1’
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall b. b -> (Proxy Maybe, ())
-        at T14066d.hs:10:1-37
+    • Couldn't match type ‘b1’ with ‘b’
       ‘b1’ is a rigid type variable bound by
         a type expected by the context:
           forall c b1 (a :: c). (Proxy a, Proxy c, b1)
         at T14066d.hs:11:33-35
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall b. b -> (Proxy Maybe, ())
+        at T14066d.hs:10:1-37
       Expected type: (Proxy a, Proxy c, b1)
         Actual type: (Proxy a, Proxy c, b)
     • In the first argument of ‘g’, namely ‘y’
diff --git a/testsuite/tests/deriving/should_compile/T14578.stderr b/testsuite/tests/deriving/should_compile/T14578.stderr
index 63375aeae0..bdb6ca5296 100644
--- a/testsuite/tests/deriving/should_compile/T14578.stderr
+++ b/testsuite/tests/deriving/should_compile/T14578.stderr
@@ -108,15 +108,15 @@ Derived type family instances:
 
 
 ==================== Filling in method body ====================
-GHC.Base.Semigroup [T14578.App f[ssk:2] a[ssk:2]]
+GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]]
   GHC.Base.sconcat = GHC.Base.$dmsconcat
-                       @(T14578.App f[ssk:2] a[ssk:2])
+                       @(T14578.App f[ssk:1] a[ssk:1])
 
 
 
 ==================== Filling in method body ====================
-GHC.Base.Semigroup [T14578.App f[ssk:2] a[ssk:2]]
+GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]]
   GHC.Base.stimes = GHC.Base.$dmstimes
-                      @(T14578.App f[ssk:2] a[ssk:2])
+                      @(T14578.App f[ssk:1] a[ssk:1])
 
 
diff --git a/testsuite/tests/gadt/T15009.hs b/testsuite/tests/gadt/T15009.hs
new file mode 100644
index 0000000000..58e17af864
--- /dev/null
+++ b/testsuite/tests/gadt/T15009.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs #-}
+
+module T15009 where
+
+-- T2 is an ordinary H98 data type,
+-- and f2 should typecheck with no problem
+data T2 a where
+  MkT2 :: a -> T2 a
+
+f2 (MkT2 x) = not x
+
+-- T1 is a GADT, but the equality is really just a 'let'
+-- so f1 should also typecheck no problem
+data T1 a where
+  MkT1 :: b ~ a => b -> T1 a
+
+f1 (MkT1 x) = not x
+
+
+
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 4c8eb806a7..321d67e9e8 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -117,3 +117,4 @@ test('T12468', normal, compile_fail, [''])
 test('T14320', normal, compile, [''])
 test('T14719', normal, compile_fail, ['-fdiagnostics-show-caret'])
 test('T14808', normal, compile, [''])
+test('T15009', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
index fa19be483c..5b6863c740 100644
--- a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
+++ b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
@@ -1,11 +1,17 @@
 
 PushedInAsGivens.hs:10:31: error:
-    • Couldn't match expected type ‘a1’ with actual type ‘a’
-        because type variable ‘a1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Could not deduce: a1 ~ a
+      from the context: F Int ~ [a1]
+        bound by the type signature for:
+                   foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
+        at PushedInAsGivens.hs:9:13-44
+      ‘a1’ is a rigid type variable bound by
         the type signature for:
           foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
         at PushedInAsGivens.hs:9:13-44
+      ‘a’ is a rigid type variable bound by
+        the inferred type of bar :: a -> (a, Int)
+        at PushedInAsGivens.hs:(9,1)-(11,20)
     • In the expression: y
       In the first argument of ‘length’, namely ‘[x, y]’
       In the expression: length [x, y]
diff --git a/testsuite/tests/indexed-types/should_fail/T13784.stderr b/testsuite/tests/indexed-types/should_fail/T13784.stderr
index 79007badb3..ee4ec20b63 100644
--- a/testsuite/tests/indexed-types/should_fail/T13784.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13784.stderr
@@ -1,44 +1,38 @@
 
 T13784.hs:28:28: error:
-    • Could not deduce: as1 ~ (a1 : Divide a1 as1)
-      from the context: (a : as) ~ (a1 : as1)
-        bound by a pattern with constructor:
-                   :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
-                 in an equation for ‘divide’
-        at T13784.hs:28:13-19
-      ‘as1’ is a rigid type variable bound by
-        a pattern with constructor:
-          :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
-        in an equation for ‘divide’
-        at T13784.hs:28:13-19
+    • Couldn't match type ‘as’ with ‘a : Divide a as’
+      ‘as’ is a rigid type variable bound by
+        the instance declaration
+        at T13784.hs:24:10-30
       Expected type: Product (Divide a (a : as))
         Actual type: Product as1
     • In the expression: as
       In the expression: (a, as)
       In an equation for ‘divide’: divide (a :* as) = (a, as)
     • Relevant bindings include
-        as :: Product as1 (bound at T13784.hs:28:18)
-        a :: a1 (bound at T13784.hs:28:13)
+        divide :: Product (a : as) -> (a, Product (Divide a (a : as)))
+          (bound at T13784.hs:28:5)
 
 T13784.hs:32:24: error:
-    • Couldn't match type ‘Product (a1 : as0)’
-                     with ‘(b, Product (Divide b (a1 : as1)))’
+    • Couldn't match type ‘Product (a : as0)’
+                     with ‘(b, Product (Divide b (a : as)))’
       Expected type: (b, Product (Divide b (a : as)))
         Actual type: Product (a1 : as0)
     • In the expression: a :* divide as
       In an equation for ‘divide’: divide (a :* as) = a :* divide as
       In the instance declaration for ‘Divideable b (a : as)’
     • Relevant bindings include
-        as :: Product as1 (bound at T13784.hs:32:18)
-        a :: a1 (bound at T13784.hs:32:13)
         divide :: Product (a : as) -> (b, Product (Divide b (a : as)))
           (bound at T13784.hs:32:5)
 
 T13784.hs:32:29: error:
-    • Couldn't match expected type ‘Product as0’
-                  with actual type ‘(a0, Product (Divide a0 as1))’
+    • Couldn't match type ‘(a0, Product (Divide a0 as))’
+                     with ‘Product as0’
+      Expected type: Product as0
+        Actual type: (a0, Product (Divide a0 as1))
     • In the second argument of ‘(:*)’, namely ‘divide as’
       In the expression: a :* divide as
       In an equation for ‘divide’: divide (a :* as) = a :* divide as
     • Relevant bindings include
-        as :: Product as1 (bound at T13784.hs:32:18)
+        divide :: Product (a : as) -> (b, Product (Divide b (a : as)))
+          (bound at T13784.hs:32:5)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index cc0d0ca708..c0e0664a06 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,27 +1,29 @@
 
 T14040a.hs:21:18: error:
-    • Couldn't match type ‘k0’ with ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘a’ with ‘k0’
+      ‘a’ is a rigid type variable bound by
         the type signature for:
           elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
                                                                 x -> WeirdList x -> *).
                            Sing wl
                            -> (forall y. p k0 w0 'WeirdNil)
                            -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                               Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                           -> p k3 w3 wl
+                               Sing x
+                               -> Sing xs -> p (WeirdList k1) w1 xs -> p k1 w2 ('WeirdCons x xs))
+                           -> p k2 w3 wl
         at T14040a.hs:(21,18)-(28,23)
       Expected type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                     -> p k3 w3 wl
+                         Sing x
+                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
+                     -> p k2 w3 wl
         Actual type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                     -> p k3 w3 wl
+                         Sing x
+                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
+                     -> p k2 w3 wl
     • In the ambiguity check for ‘elimWeirdList’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
@@ -39,8 +41,10 @@ T14040a.hs:34:8: error:
                                        -> (forall y. p k0 w0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
                                            Sing x
-                                           -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                                       -> p k3 w3 wl’
+                                           -> Sing xs
+                                           -> p (WeirdList k1) w1 xs
+                                           -> p k1 w2 ('WeirdCons x xs))
+                                       -> p k2 w3 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr
index e822f6e596..3d2492e23d 100644
--- a/testsuite/tests/polykinds/T13555.stderr
+++ b/testsuite/tests/polykinds/T13555.stderr
@@ -1,8 +1,7 @@
 
 T13555.hs:25:14: error:
-    • Couldn't match type ‘k0’ with ‘k2’
-        because type variable ‘k2’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘k2’ with ‘k0’
+      ‘k2’ is a rigid type variable bound by
         the type signature for:
           crtInfo :: forall k2 (m :: k2).
                      Reflects m Int =>
diff --git a/testsuite/tests/polykinds/T14846.hs b/testsuite/tests/polykinds/T14846.hs
index ad17841daa..7b96e942f3 100644
--- a/testsuite/tests/polykinds/T14846.hs
+++ b/testsuite/tests/polykinds/T14846.hs
@@ -34,6 +34,6 @@ data Hom :: Cat k -> Cat (Struct cls) where
 class Category (cat::Cat ob) where
   i :: StructI xx a => ríki a a
 
-instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
-  i :: forall xx a. StructI xx a => Hom ríki a a
+instance Category riki => Category (Hom riki :: Cat (Struct cls)) where
+  i :: forall xx a. StructI xx a => Hom riki a a
   i = case struct :: AStruct (Structured a cls) of
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 828ddf6374..1bfa94218c 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -1,24 +1,24 @@
 
 T14846.hs:38:8: error:
-    • Couldn't match type ‘ríki1’ with ‘Hom ríki’
-      ‘ríki1’ is a rigid type variable bound by
+    • Couldn't match type ‘ríki’ with ‘Hom riki’
+      ‘ríki’ is a rigid type variable bound by
         the type signature for:
           i :: forall k5 (cls1 :: k5
-                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki1 :: Struct
-                                                                                              cls1
-                                                                                            -> Struct
-                                                                                                 cls1
-                                                                                            -> *).
+                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki :: Struct
+                                                                                             cls1
+                                                                                           -> Struct
+                                                                                                cls1
+                                                                                           -> *).
                StructI xx a =>
-               ríki1 a a
+               ríki a a
         at T14846.hs:38:8-48
-      Expected type: ríki1 a a
-        Actual type: Hom ríki a0 a0
+      Expected type: ríki a a
+        Actual type: Hom riki a0 a0
     • When checking that instance signature for ‘i’
         is more general than its signature in the class
         Instance sig: forall (xx :: k0) (a :: Struct cls0).
                       StructI xx a =>
-                      Hom ríki a a
+                      Hom riki a a
            Class sig: forall k1 (cls :: k1
                                         -> Constraint) k2 (xx :: k2) (a :: Struct
                                                                              cls) (ríki :: Struct
@@ -28,32 +28,7 @@ T14846.hs:38:8: error:
                                                                                            -> *).
                       StructI xx a =>
                       ríki a a
-      In the instance declaration for ‘Category (Hom ríki)’
-
-T14846.hs:39:12: error:
-    • Could not deduce (StructI xx1 (Structured a cls))
-        arising from a use of ‘struct’
-      from the context: Category ríki
-        bound by the instance declaration at T14846.hs:37:10-65
-      or from: StructI xx a
-        bound by the type signature for:
-                   i :: forall (xx :: k0) (a :: Struct cls0).
-                        StructI xx a =>
-                        Hom ríki a a
-        at T14846.hs:38:8-48
-      The type variable ‘xx1’ is ambiguous
-      Relevant bindings include
-        i :: Hom ríki a a (bound at T14846.hs:39:3)
-      These potential instance exist:
-        instance forall k (xx :: k) (cls :: k
-                                            -> Constraint) (structured :: Struct cls).
-                 (Structured xx cls ~ structured, cls xx) =>
-                 StructI xx structured
-          -- Defined at T14846.hs:28:10
-    • In the expression: struct :: AStruct (Structured a cls)
-      In the expression: case struct :: AStruct (Structured a cls) of
-      In an equation for ‘i’:
-          i = case struct :: AStruct (Structured a cls) of
+      In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:44: error:
     • Expected kind ‘Struct cls0 -> Constraint’,
@@ -62,4 +37,4 @@ T14846.hs:39:44: error:
       In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
       In an expression type signature: AStruct (Structured a cls)
     • Relevant bindings include
-        i :: Hom ríki a a (bound at T14846.hs:39:3)
+        i :: Hom riki a a (bound at T14846.hs:39:3)
diff --git a/testsuite/tests/polykinds/T7230.stderr b/testsuite/tests/polykinds/T7230.stderr
index 53b8bcd8c3..48781e8f7f 100644
--- a/testsuite/tests/polykinds/T7230.stderr
+++ b/testsuite/tests/polykinds/T7230.stderr
@@ -9,13 +9,13 @@ T7230.hs:48:32: error:
         at T7230.hs:47:1-68
       or from: xs ~ (x : xs1)
         bound by a pattern with constructor:
-                   SCons :: forall k (x :: k) (xs :: [k]).
+                   SCons :: forall a (x :: a) (xs :: [a]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘crash’
         at T7230.hs:48:8-27
       or from: xs1 ~ (x1 : xs2)
         bound by a pattern with constructor:
-                   SCons :: forall k (x :: k) (xs :: [k]).
+                   SCons :: forall a (x :: a) (xs :: [a]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘crash’
         at T7230.hs:48:17-26
diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr
index 52a4b21490..d368d055f0 100644
--- a/testsuite/tests/polykinds/T8566.stderr
+++ b/testsuite/tests/polykinds/T8566.stderr
@@ -1,12 +1,12 @@
 
 T8566.hs:32:9: error:
-    • Could not deduce (C ('AA (t1 (I a ps)) as) ps fs0)
+    • Could not deduce (C ('AA (t (I a ps)) as) ps fs0)
         arising from a use of ‘c’
       from the context: C ('AA (t (I a ps)) as) ps fs
         bound by the instance declaration at T8566.hs:30:10-67
       or from: 'AA t (a : as) ~ 'AA t1 as1
         bound by a pattern with constructor:
-                   A :: forall k (t :: k) (as :: [U *]) (r :: [*]). I ('AA t as) r,
+                   A :: forall v (t :: v) (as :: [U *]) (r :: [*]). I ('AA t as) r,
                  in an equation for ‘c’
         at T8566.hs:32:5
       The type variable ‘fs0’ is ambiguous
diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr
index a019b9e117..604cc1b7ec 100644
--- a/testsuite/tests/polykinds/T9222.stderr
+++ b/testsuite/tests/polykinds/T9222.stderr
@@ -8,7 +8,7 @@ T9222.hs:13:3: error:
           at T9222.hs:13:3-43
       ‘c’ is a rigid type variable bound by
         the type of the constructor ‘Want’:
-          forall k2 k3 (a :: (k2, k3)) (b :: k2) (c :: k3).
+          forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1).
           ((a ~ '(b, c)) => Proxy b) -> Want a
         at T9222.hs:13:3-43
     • In the ambiguity check for ‘Want’
diff --git a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr
index 6cc24fcaf6..e38c32b595 100644
--- a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr
+++ b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr
@@ -1,12 +1,14 @@
 
 ExPatFail.hs:12:15: error:
     • Couldn't match expected type ‘p’ with actual type ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a’ is a rigid type variable bound by
         a pattern with constructor:
           MkT :: forall a. Integral a => a -> Int -> T,
         in a pattern binding
         at ExPatFail.hs:12:11-17
+      ‘p’ is a rigid type variable bound by
+        the inferred type of f :: T -> p
+        at ExPatFail.hs:(12,1)-(13,10)
     • In the pattern: MkT y _
       In a pattern binding: MkT y _ = x
       In the expression: let MkT y _ = x in y
diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr
index 01b003fa3a..52f207d511 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9834.stderr
@@ -19,17 +19,17 @@ T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
           (bound at T9834.hs:23:3)
 
 T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘a’ with ‘a1’
+    • Couldn't match type ‘a1’ with ‘a’
+      ‘a1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall (q :: * -> *). Applicative q => Nat (Comp p q) (Comp p q)
+        at T9834.hs:23:10-19
       ‘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
-      ‘a1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall (q :: * -> *). Applicative q => Nat (Comp p q) (Comp p q)
-        at T9834.hs:23:10-19
       Expected type: Comp p q a1 -> Comp p q a1
         Actual type: Comp p q a -> Comp p q a
     • In the expression: wrapIdComp
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index 9c13f1791d..b2fe9abb4b 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -8,11 +8,13 @@ tc141.hs:11:12: error:
 
 tc141.hs:11:31: error:
     • Couldn't match expected type ‘a2’ with actual type ‘a’
-        because type variable ‘a2’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a2’ is a rigid type variable bound by
         an expression type signature:
           forall a2. a2
         at tc141.hs:11:34
+      ‘a’ is a rigid type variable bound by
+        the inferred type of f :: (a, a) -> (a1, a)
+        at tc141.hs:11:1-37
     • In the expression: q :: a
       In the expression: (q :: a, p)
       In the expression: let (p :: a, q :: a) = x in (q :: a, p)
@@ -36,11 +38,13 @@ tc141.hs:13:13: error:
 
 tc141.hs:15:18: error:
     • Couldn't match expected type ‘a2’ with actual type ‘p’
-        because type variable ‘a2’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a2’ is a rigid type variable bound by
         the type signature for:
           v :: forall a2. a2
         at tc141.hs:14:14-19
+      ‘p’ is a rigid type variable bound by
+        the inferred type of g :: a -> p -> a1
+        at tc141.hs:(13,1)-(16,13)
     • In the expression: b
       In an equation for ‘v’: v = b
       In the expression:
diff --git a/testsuite/tests/typecheck/should_fail/T14607.hs b/testsuite/tests/typecheck/should_fail/T14607.hs
index c05df0be25..86c738dc19 100644
--- a/testsuite/tests/typecheck/should_fail/T14607.hs
+++ b/testsuite/tests/typecheck/should_fail/T14607.hs
@@ -25,3 +25,10 @@ instance Mk a where
 -- At some point, this program was accepted. That's fine. But right now,
 -- it's rejected with a kind error, and we can't generally defer kind
 -- errors, so I'm saying that behavior is OK.
+
+-- Later (May 18) the kind error ended up being in an term-level
+-- implication constraint, which /does/ have an evidence binding
+-- So now the kind error can be deferred.
+-- Consequence of a fast-path for tcImplicitTKBndrsX I think.
+
+
diff --git a/testsuite/tests/typecheck/should_fail/T14607.stderr b/testsuite/tests/typecheck/should_fail/T14607.stderr
index 0a63e53030..740f89a0d4 100644
--- a/testsuite/tests/typecheck/should_fail/T14607.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14607.stderr
@@ -1,12 +1,21 @@
 
-T14607.hs:22:9: error:
+T14607.hs:22:9: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Expecting one more argument to ‘LamCons a  '()’
       Expected a type, but ‘LamCons a  '()’ has kind ‘() -> *’
     • In the type signature: mk :: LamCons a  '()
       In the instance declaration for ‘Mk a’
 
-T14607.hs:22:19: error:
+T14607.hs:22:19: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Expected a type, but ‘ '()’ has kind ‘()’
     • In the second argument of ‘LamCons’, namely ‘ '()’
       In the type signature: mk :: LamCons a  '()
       In the instance declaration for ‘Mk a’
+
+T14607.hs:23:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘LamCons a '()’
+                  with actual type ‘LamCons a0 a0 '()’
+    • In the expression: mk
+      In an equation for ‘mk’: mk = mk
+      In the instance declaration for ‘Mk a’
+    • Relevant bindings include
+        mk :: LamCons a '() (bound at T14607.hs:23:3)
diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr
index 77348c357a..d72b6d9a7a 100644
--- a/testsuite/tests/typecheck/should_fail/T7453.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7453.stderr
@@ -1,11 +1,13 @@
 
 T7453.hs:10:30: error:
     • Couldn't match expected type ‘t’ with actual type ‘p’
-        because type variable ‘t’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘t’ is a rigid type variable bound by
         the type signature for:
           z :: forall t. Id t
         at T7453.hs:8:11-19
+      ‘p’ is a rigid type variable bound by
+        the inferred type of cast1 :: p -> a
+        at T7453.hs:(7,1)-(10,30)
     • In the first argument of ‘Id’, namely ‘v’
       In the expression: Id v
       In an equation for ‘aux’: aux = Id v
@@ -17,11 +19,13 @@ T7453.hs:10:30: error:
 
 T7453.hs:16:33: error:
     • Couldn't match expected type ‘t1’ with actual type ‘p’
-        because type variable ‘t1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘t1’ is a rigid type variable bound by
         the type signature for:
           z :: forall t1. () -> t1
         at T7453.hs:14:11-22
+      ‘p’ is a rigid type variable bound by
+        the inferred type of cast2 :: p -> t
+        at T7453.hs:(13,1)-(16,33)
     • In the first argument of ‘const’, namely ‘v’
       In the expression: const v
       In an equation for ‘aux’: aux = const v
@@ -33,11 +37,13 @@ T7453.hs:16:33: error:
 
 T7453.hs:21:15: error:
     • Couldn't match expected type ‘t1’ with actual type ‘p’
-        because type variable ‘t1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘t1’ is a rigid type variable bound by
         the type signature for:
           z :: forall t1. t1
         at T7453.hs:20:11-16
+      ‘p’ is a rigid type variable bound by
+        the inferred type of cast3 :: p -> t
+        at T7453.hs:(19,1)-(22,33)
     • In the expression: v
       In an equation for ‘z’:
           z = v
diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr
index 4cf1cfaf67..7e01868526 100644
--- a/testsuite/tests/typecheck/should_fail/T7869.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7869.stderr
@@ -1,11 +1,13 @@
 
 T7869.hs:3:12: error:
-    • Couldn't match type ‘b’ with ‘b1’
-        because type variable ‘b1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘b1’ with ‘b’
+      ‘b1’ is a rigid type variable bound by
         an expression type signature:
           forall a1 b1. [a1] -> b1
         at T7869.hs:3:20-27
+      ‘b’ is a rigid type variable bound by
+        the inferred type of f :: [a] -> b
+        at T7869.hs:3:1-27
       Expected type: [a1] -> b1
         Actual type: [a] -> b
     • In the expression: f x
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 5a3e73313f..86099ea026 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -1,4 +1,4 @@
-
+4607
 test('tcfail001', normal, compile_fail, [''])
 test('tcfail002', normal, compile_fail, [''])
 test('tcfail003', normal, compile_fail, [''])
@@ -467,7 +467,7 @@ test('T14350', normal, compile_fail, [''])
 test('T14390', normal, compile_fail, [''])
 test('MissingExportList03', normal, compile_fail, [''])
 test('T14618', normal, compile_fail, [''])
-test('T14607', normal, compile_fail, [''])
+test('T14607', normal, compile, [''])
 test('T14605', normal, compile_fail, [''])
 test('T14761a', normal, compile_fail, [''])
 test('T14761b', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail068.stderr b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
index bb3f9ddb53..4318021213 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail068.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
@@ -23,48 +23,48 @@ tcfail068.hs:14:9: error:
           (bound at tcfail068.hs:12:1)
 
 tcfail068.hs:19:9: error:
-    • Couldn't match type ‘s’ with ‘s1’
+    • Couldn't match type ‘s1’ with ‘s’
+      ‘s1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall s1. GHC.ST.ST s1 (IndTree s a)
+        at tcfail068.hs:(18,9)-(21,19)
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itiap :: forall a s.
                    Constructed a =>
                    (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
         at tcfail068.hs:16:1-75
-      ‘s1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall s1. GHC.ST.ST s1 (IndTree s a)
-        at tcfail068.hs:(18,9)-(21,19)
       Expected type: GHC.ST.ST s1 (IndTree s a)
         Actual type: GHC.ST.ST s (IndTree s a)
     • In the first argument of ‘runST’, namely
         ‘(readSTArray arr i
-          >>= \ val -> writeSTArray arr i (f val) >> return arr)’
+            >>= \ val -> writeSTArray arr i (f val) >> return arr)’
       In the expression:
         runST
           (readSTArray arr i
-           >>= \ val -> writeSTArray arr i (f val) >> return arr)
+             >>= \ val -> writeSTArray arr i (f val) >> return arr)
       In an equation for ‘itiap’:
           itiap i f arr
             = runST
                 (readSTArray arr i
-                 >>= \ val -> writeSTArray arr i (f val) >> return arr)
+                   >>= \ val -> writeSTArray arr i (f val) >> return arr)
     • Relevant bindings include
         arr :: IndTree s a (bound at tcfail068.hs:17:11)
         itiap :: (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
           (bound at tcfail068.hs:17:1)
 
 tcfail068.hs:24:36: error:
-    • Couldn't match type ‘s’ with ‘s1’
+    • Couldn't match type ‘s1’ with ‘s’
+      ‘s1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall s1. GHC.ST.ST s1 (IndTree s a)
+        at tcfail068.hs:24:29-46
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itrap :: forall a s.
                    Constructed a =>
                    ((Int, Int), (Int, Int)) -> (a -> a) -> IndTree s a -> IndTree s a
         at tcfail068.hs:23:1-87
-      ‘s1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall s1. GHC.ST.ST s1 (IndTree s a)
-        at tcfail068.hs:24:29-46
       Expected type: GHC.ST.ST s1 (IndTree s a)
         Actual type: GHC.ST.ST s (IndTree s a)
     • In the first argument of ‘runST’, namely ‘(itrap' i k)’
@@ -91,7 +91,11 @@ tcfail068.hs:24:36: error:
           (bound at tcfail068.hs:24:1)
 
 tcfail068.hs:36:46: error:
-    • Couldn't match type ‘s’ with ‘s1’
+    • Couldn't match type ‘s1’ with ‘s’
+      ‘s1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall s1. GHC.ST.ST s1 (c, IndTree s b)
+        at tcfail068.hs:36:40-63
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itrapstate :: forall b a c s.
@@ -104,10 +108,6 @@ tcfail068.hs:36:46: error:
                         -> IndTree s b
                         -> (c, IndTree s b)
         at tcfail068.hs:(34,1)-(35,62)
-      ‘s1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall s1. GHC.ST.ST s1 (c, IndTree s b)
-        at tcfail068.hs:36:40-63
       Expected type: GHC.ST.ST s1 (c, IndTree s b)
         Actual type: GHC.ST.ST s (c, IndTree s b)
     • In the first argument of ‘runST’, namely ‘(itrapstate' i k s)’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail076.stderr b/testsuite/tests/typecheck/should_fail/tcfail076.stderr
index 546715aa4a..d4368a4cf5 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail076.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail076.stderr
@@ -1,14 +1,14 @@
 
 tcfail076.hs:18:82: error:
-    • Couldn't match type ‘res’ with ‘res1’
-      ‘res’ is a rigid type variable bound by
-        a type expected by the context:
-          forall res. (a -> m res) -> m res
-        at tcfail076.hs:18:28-96
+    • Couldn't match type ‘res1’ with ‘res’
       ‘res1’ is a rigid type variable bound by
         a type expected by the context:
           forall res1. (b -> m res1) -> m res1
         at tcfail076.hs:18:64-88
+      ‘res’ is a rigid type variable bound by
+        a type expected by the context:
+          forall res. (a -> m res) -> m res
+        at tcfail076.hs:18:28-96
       Expected type: m res1
         Actual type: m res
     • In the expression: cont a
diff --git a/testsuite/tests/typecheck/should_fail/tcfail099.stderr b/testsuite/tests/typecheck/should_fail/tcfail099.stderr
index bc30866ec2..a04920fb39 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail099.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail099.stderr
@@ -1,11 +1,13 @@
 
 tcfail099.hs:9:20: error:
     • Couldn't match expected type ‘a’ with actual type ‘p’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a’ is a rigid type variable bound by
         a pattern with constructor: C :: forall a. (a -> Int) -> DS,
         in an equation for ‘call’
         at tcfail099.hs:9:7-9
+      ‘p’ is a rigid type variable bound by
+        the inferred type of call :: DS -> p -> Int
+        at tcfail099.hs:9:1-22
     • In the first argument of ‘f’, namely ‘arg’
       In the expression: f arg
       In an equation for ‘call’: call (C f) arg = f arg
diff --git a/testsuite/tests/typecheck/should_fail/tcfail103.stderr b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
index ba0694b117..2192d8a7f6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail103.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
@@ -1,14 +1,14 @@
 
 tcfail103.hs:15:13: error:
-    • Couldn't match type ‘t’ with ‘s’
-      ‘t’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall t. ST t Int
-        at tcfail103.hs:10:1-12
+    • Couldn't match type ‘s’ with ‘t’
       ‘s’ is a rigid type variable bound by
         the type signature for:
           g :: forall s. ST s Int
         at tcfail103.hs:13:9-21
+      ‘t’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall t. ST t Int
+        at tcfail103.hs:10:1-12
       Expected type: ST s Int
         Actual type: ST t Int
     • In the expression: readSTRef v
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
index e8073887ac..724535145c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
@@ -7,11 +7,13 @@ tcfail174.hs:9:5: error:
       In an equation for ‘g’: g = Base id
 
 tcfail174.hs:16:14: error:
-    • Couldn't match type ‘a’ with ‘a1’
-        because type variable ‘a1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘a1’ with ‘a’
+      ‘a1’ is a rigid type variable bound by
         the type a -> a
         at tcfail174.hs:16:1-14
+      ‘a’ is a rigid type variable bound by
+        the inferred type of h1 :: Capture a
+        at tcfail174.hs:16:1-14
       Expected type: Capture (forall x. x -> a)
         Actual type: Capture (forall a. a -> a)
     • In the first argument of ‘Capture’, namely ‘g’
@@ -23,7 +25,8 @@ tcfail174.hs:16:14: error:
 tcfail174.hs:19:14: error:
     • Couldn't match type ‘a’ with ‘b’
       ‘a’ is a rigid type variable bound by
-        the type a -> a at tcfail174.hs:1:1
+        the type a -> a
+        at tcfail174.hs:1:1
       ‘b’ is a rigid type variable bound by
         the type signature for:
           h2 :: forall b. Capture b
diff --git a/testsuite/tests/typecheck/should_fail/tcfail198.stderr b/testsuite/tests/typecheck/should_fail/tcfail198.stderr
index e8c3852b1c..66c8438dc4 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail198.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail198.stderr
@@ -1,11 +1,13 @@
 
 tcfail198.hs:6:36: error:
     • Couldn't match expected type ‘a1’ with actual type ‘a’
-        because type variable ‘a1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a1’ is a rigid type variable bound by
         an expression type signature:
           forall a1. a1
         at tcfail198.hs:6:41
+      ‘a’ is a rigid type variable bound by
+        the inferred type of f3 :: [a] -> [a]
+        at tcfail198.hs:6:1-44
     • In the expression: x :: a
       In the second argument of ‘(++)’, namely ‘[x :: a]’
       In the expression: xs ++ [x :: a]