Improve error messages around kind mismatches.

Previously, when canonicalizing (or unifying, in uType) a
heterogeneous equality, we emitted a kind equality and used the
resulting coercion to cast one side of the heterogeneous equality.

While sound, this led to terrible error messages. (See the bugs
listed below.) The problem is that using the coercion built from
the emitted kind equality is a bit like a wanted rewriting a wanted.
The solution is to keep heterogeneous equalities as irreducible.

See Note [Equalities with incompatible kinds] in TcCanonical.

This commit also removes a highly suspicious switch to FM_SubstOnly
when flattening in the kinds of a type variable. I have no idea
why this was there, other than as a holdover from pre-TypeInType.
I've not left a Note because there is simply no reason I can conceive
of that the FM_SubstOnly should be there.

One challenge with this patch is that the emitted derived equalities
might get emitted several times: when a heterogeneous equality is
in an implication and then gets floated out from the implication,
the Derived is present both in and out of the implication. This
causes a duplicate error message. (Test case:
typecheck/should_fail/T7368) Solution: track the provenance of
Derived constraints and refuse to float out a constraint that has
an insoluble Derived.

Lastly, this labels one test (dependent/should_fail/RAE_T32a)
as expect_broken, because the problem is really #12919. The
different handling of constraints in this patch exposes the error.

This fixes bugs #11198, #12373, #13530, and #13610.

test cases:
typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}

31 files changed, 219 insertions, 120 deletions

diff --git a/testsuite/tests/dependent/should_fail/T11471.hs b/testsuite/tests/dependent/should_fail/T11471.hs
index 19025db22b..ae09ae07bb 100644
--- a/testsuite/tests/dependent/should_fail/T11471.hs
+++ b/testsuite/tests/dependent/should_fail/T11471.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies #-}
+{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies, AllowAmbiguousTypes #-}
 
 module T11471 where
 
diff --git a/testsuite/tests/dependent/should_fail/T11471.stderr b/testsuite/tests/dependent/should_fail/T11471.stderr
index 80c5fc606c..640ae6c754 100644
--- a/testsuite/tests/dependent/should_fail/T11471.stderr
+++ b/testsuite/tests/dependent/should_fail/T11471.stderr
@@ -1,19 +1,22 @@
 
 T11471.hs:15:10: error:
     • Couldn't match a lifted type with an unlifted type
-      Expected type: Proxy Int#
+      When matching types
+        a :: *
+        Int# :: TYPE 'IntRep
+      Expected type: Proxy a
         Actual type: Proxy Int#
-      Use -fprint-explicit-kinds to see the kind arguments
     • In the first argument of ‘f’, namely ‘(undefined :: Proxy Int#)’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
 
 T11471.hs:15:35: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
-        F Int# :: *
+        F a :: *
         Int# :: TYPE 'IntRep
     • In the second argument of ‘f’, namely ‘3#’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
-    • Relevant bindings include bad :: F Int# (bound at T11471.hs:15:1)
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index c648f9ed1d..af3efc6716 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,5 +1,5 @@
 test('DepFail1', normal, compile_fail, [''])
-test('RAE_T32a', normal, compile_fail, [''])
+test('RAE_T32a', expect_broken(12919), compile_fail, [''])
 test('TypeSkolEscape', normal, compile_fail, [''])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index ea9033ac6c..bb179975fb 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,15 +1,15 @@
 
 gadt7.hs:16:38: error:
     • Couldn't match expected type ‘p1’ with actual type ‘p’
-        ‘p1’ is untouchable
+        ‘p’ is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with constructor: K :: T Int,
                    in a case alternative
           at gadt7.hs:16:33
-      ‘p1’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
       ‘p’ is a rigid type variable bound by
         the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1
diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout
index 2e86b42713..5d478ae04e 100644
--- a/testsuite/tests/ghci.debugger/scripts/break012.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout
@@ -1,14 +1,14 @@
 Stopped in Main.g, break012.hs:5:10-18
-_result :: (p, a1 -> a1, (), a -> a -> a) = _
-a :: p = _
-b :: a2 -> a2 = _
+_result :: (a1, a2 -> a2, (), a -> a -> a) = _
+a :: a1 = _
+b :: a3 -> a3 = _
 c :: () = _
 d :: a -> a -> a = _
-a :: p
-b :: a2 -> a2
+a :: a1
+b :: a3 -> a3
 c :: ()
 d :: a -> a -> a
-a = (_t1::p)
-b = (_t2::a2 -> a2)
+a = (_t1::a1)
+b = (_t2::a3 -> a3)
 c = (_t3::())
 d = (_t4::a -> a -> a)
diff --git a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
index 5bc6aca64c..f2ea8b2668 100644
--- a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
@@ -1,12 +1,12 @@
 
 ExtraTcsUntch.hs:23:18: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[p]’
+    • Couldn't match expected type ‘F Int’ with actual type ‘[x]’
     • In the first argument of ‘h’, namely ‘[x]’
       In the expression: h [x]
       In an equation for ‘g1’: g1 _ = h [x]
     • Relevant bindings include
-        x :: p (bound at ExtraTcsUntch.hs:21:3)
-        f :: p -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+        x :: x (bound at ExtraTcsUntch.hs:21:3)
+        f :: x -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
 ExtraTcsUntch.hs:25:38: error:
     • Couldn't match expected type ‘F Int’ with actual type ‘[[a0]]’
diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr
index e303e54f74..21af0d868a 100644
--- a/testsuite/tests/indexed-types/should_fail/T5934.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr
@@ -5,16 +5,3 @@ T5934.hs:12:7: error:
         GHC doesn't yet support impredicative polymorphism
     • In the expression: 0
       In an equation for ‘run’: run = 0
-
-T5934.hs:12:7: error:
-    • Ambiguous type variable ‘a0’ arising from the literal ‘0’
-      prevents the constraint ‘(Num a0)’ from being solved.
-      Probable fix: use a type annotation to specify what ‘a0’ should be.
-      These potential instances exist:
-        instance Num Integer -- Defined in ‘GHC.Num’
-        instance Num Double -- Defined in ‘GHC.Float’
-        instance Num Float -- Defined in ‘GHC.Float’
-        ...plus two others
-        (use -fprint-potential-instances to see them all)
-    • In the expression: 0
-      In an equation for ‘run’: run = 0
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 4b551558a1..0a1b83ad9e 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -29,3 +29,59 @@ T12593.hs:12:40: error:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:47: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+        k2 :: *
+    • In the first argument of ‘p’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:49: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
+                     with ‘*’
+      When matching kinds
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k3 :: *
+    • In the second argument of ‘p’, namely ‘d’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:56: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+        k0 :: *
+    • In the first argument of ‘q’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:58: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
+                     with ‘*’
+      When matching kinds
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k1 :: *
+    • In the second argument of ‘q’, namely ‘d’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr
index eaea0335cf..e822f6e596 100644
--- a/testsuite/tests/polykinds/T13555.stderr
+++ b/testsuite/tests/polykinds/T13555.stderr
@@ -9,26 +9,7 @@ T13555.hs:25:14: error:
                      TaggedT m Maybe (CRTInfo (GF fp d))
         at T13555.hs:25:14-79
       Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
-        Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
-    • When checking that instance signature for ‘crtInfo’
-        is more general than its signature in the class
-        Instance sig: forall (m :: k0).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-           Class sig: forall k2 (m :: k2).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
-
-T13555.hs:25:14: error:
-    • Could not deduce (Reflects m Int)
-      from the context: Reflects m Int
-        bound by the type signature for:
-                   crtInfo :: forall k2 (m :: k2).
-                              Reflects m Int =>
-                              TaggedT m Maybe (CRTInfo (GF fp d))
-        at T13555.hs:25:14-79
-      The type variable ‘k0’ is ambiguous
+        Actual type: TaggedT m0 Maybe (CRTInfo (GF fp d))
     • When checking that instance signature for ‘crtInfo’
         is more general than its signature in the class
         Instance sig: forall (m :: k0).
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index a198657754..6c4eec47f2 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -1,16 +1,16 @@
 
 T7438.hs:6:14: error:
     • Couldn't match expected type ‘p1’ with actual type ‘p’
-        ‘p1’ is untouchable
+        ‘p’ is untouchable
           inside the constraints: b ~ a
           bound by a pattern with constructor:
                      Nil :: forall k (a :: k). Thrist a a,
                    in an equation for ‘go’
           at T7438.hs:6:4-6
-      ‘p1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
       ‘p’ is a rigid type variable bound by
         the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr
index 1e7818c5ef..0794442edc 100644
--- a/testsuite/tests/polykinds/T8566.stderr
+++ b/testsuite/tests/polykinds/T8566.stderr
@@ -1,6 +1,6 @@
 
 T8566.hs:32:9: error:
-    • Could not deduce (C ('AA (t (I a ps)) as) ps fs0)
+    • Could not deduce (C ('AA (t1 (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
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index 79a9a4617f..d9483c8490 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,12 +1,16 @@
 
 T9017.hs:8:7: error:
-    • Couldn't match kind ‘k’ with ‘*’
-      ‘k’ is a rigid type variable bound by
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
         the type signature for:
           foo :: forall k k1 (a :: k -> k1 -> *) (b :: k) (m :: k -> k1).
                  a b (m b)
         at T9017.hs:7:1-16
-      When matching the kind of ‘a’
+      When matching types
+        a1 :: * -> * -> *
+        a :: k -> k1 -> *
+      Expected type: a b (m b)
+        Actual type: a1 a0 (m0 a0)
     • In the expression: arr return
       In an equation for ‘foo’: foo = arr return
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T12373.hs b/testsuite/tests/typecheck/should_fail/T12373.hs
new file mode 100644
index 0000000000..3f23779b82
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12373.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE MagicHash, ScopedTypeVariables, UnboxedTuples #-}
+
+module T12373 where
+
+import GHC.MVar
+import GHC.Prim
+import GHC.Types
+
+main :: IO ()
+main = IO (\rw -> newMVar# rw) >> return ()
diff --git a/testsuite/tests/typecheck/should_fail/T12373.stderr b/testsuite/tests/typecheck/should_fail/T12373.stderr
new file mode 100644
index 0000000000..45852b8ea6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12373.stderr
@@ -0,0 +1,8 @@
+
+T12373.hs:10:19: error:
+    • Couldn't match a lifted type with an unlifted type
+      Expected type: (# State# RealWorld, a1 #)
+        Actual type: (# State# RealWorld, MVar# RealWorld a0 #)
+    • In the expression: newMVar# rw
+      In the first argument of ‘IO’, namely ‘(\ rw -> newMVar# rw)’
+      In the first argument of ‘(>>)’, namely ‘IO (\ rw -> newMVar# rw)’
diff --git a/testsuite/tests/typecheck/should_fail/T13530.hs b/testsuite/tests/typecheck/should_fail/T13530.hs
new file mode 100644
index 0000000000..9f95e497f2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13530.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE MagicHash, UnboxedTuples #-}
+
+module T13530 where
+
+import GHC.Exts
+
+g :: Int -> (# Int#, a #)
+g (I# y) = (# y, undefined #)
+
+f :: Int -> (# Int#, Int# #)
+f x = g x
diff --git a/testsuite/tests/typecheck/should_fail/T13530.stderr b/testsuite/tests/typecheck/should_fail/T13530.stderr
new file mode 100644
index 0000000000..8760bcb417
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13530.stderr
@@ -0,0 +1,7 @@
+
+T13530.hs:11:7: error:
+    • Couldn't match a lifted type with an unlifted type
+      Expected type: (# Int#, Int# #)
+        Actual type: (# Int#, a0 #)
+    • In the expression: g x
+      In an equation for ‘f’: f x = g x
diff --git a/testsuite/tests/typecheck/should_fail/T13610.hs b/testsuite/tests/typecheck/should_fail/T13610.hs
new file mode 100644
index 0000000000..371c3388e9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13610.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE MagicHash #-}
+
+module T13610 where
+
+import GHC.Prim
+import GHC.Types
+
+main = do
+    let primDouble = 0.42## :: Double#
+    let double = 0.42 :: Double
+    IO (\s -> mkWeakNoFinalizer# double () s)
diff --git a/testsuite/tests/typecheck/should_fail/T13610.stderr b/testsuite/tests/typecheck/should_fail/T13610.stderr
new file mode 100644
index 0000000000..0755ce9371
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13610.stderr
@@ -0,0 +1,14 @@
+
+T13610.hs:11:15: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        a :: *
+        Weak# () :: TYPE 'UnliftedRep
+      Expected type: (# State# RealWorld, a #)
+        Actual type: (# State# RealWorld, Weak# () #)
+    • In the expression: mkWeakNoFinalizer# double () s
+      In the first argument of ‘IO’, namely
+        ‘(\ s -> mkWeakNoFinalizer# double () s)’
+      In a stmt of a 'do' block:
+        IO (\ s -> mkWeakNoFinalizer# double () s)
+    • Relevant bindings include main :: IO a (bound at T13610.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T5691.stderr b/testsuite/tests/typecheck/should_fail/T5691.stderr
index ad5c7e452f..9d4e587166 100644
--- a/testsuite/tests/typecheck/should_fail/T5691.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5691.stderr
@@ -1,12 +1,12 @@
 
-T5691.hs:14:9: error:
+T5691.hs:15:24: error:
     • Couldn't match type ‘p’ with ‘PrintRuleInterp’
       Expected type: PrintRuleInterp a
         Actual type: p a
-    • When checking that the pattern signature: p a
-        fits the type of its context: PrintRuleInterp a
-      In the pattern: f :: p a
-      In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f
+    • In the first argument of ‘printRule_’, namely ‘f’
+      In the second argument of ‘($)’, namely ‘printRule_ f’
+      In the expression: MkPRI $ printRule_ f
+    • Relevant bindings include f :: p a (bound at T5691.hs:14:9)
 
 T5691.hs:24:10: error:
     • No instance for (Alternative RecDecParser)
diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr
index f187aee61c..660ef98f26 100644
--- a/testsuite/tests/typecheck/should_fail/T7368.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368.stderr
@@ -1,7 +1,11 @@
 
 T7368.hs:3:10: error:
     • Couldn't match kind ‘*’ with ‘* -> *’
-      When matching the kind of ‘Maybe’
+      When matching types
+        b0 :: *
+        Maybe :: * -> *
+      Expected type: a0 -> b0
+        Actual type: c0 Maybe
     • In the first argument of ‘b’, namely ‘(l Nothing)’
       In the expression: b (l Nothing)
       In an equation for ‘f’: f = b (l Nothing)
diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr
index e55aab0e62..16c8326afe 100644
--- a/testsuite/tests/typecheck/should_fail/T7368a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr
@@ -5,7 +5,7 @@ T7368a.hs:8:6: error:
         f :: * -> *
         Bad :: (* -> *) -> *
       Expected type: f (Bad f)
-        Actual type: Bad (Bad f)
+        Actual type: Bad w0
     • In the pattern: Bad x
       In an equation for ‘fun’: fun (Bad x) = True
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr
index 518d6fad05..77348c357a 100644
--- a/testsuite/tests/typecheck/should_fail/T7453.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7453.stderr
@@ -1,56 +1,32 @@
 
-T7453.hs:9:15: error:
-    • Couldn't match type ‘p’ with ‘t’
+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
         the type signature for:
           z :: forall t. Id t
         at T7453.hs:8:11-19
-      Expected type: Id t
-        Actual type: Id p
-    • In the expression: aux
-      In an equation for ‘z’:
-          z = aux
-            where
-                aux = Id v
-      In an equation for ‘cast1’:
-          cast1 v
-            = runId z
-            where
-                z :: Id t
-                z = aux
-                  where
-                      aux = Id v
+    • In the first argument of ‘Id’, namely ‘v’
+      In the expression: Id v
+      In an equation for ‘aux’: aux = Id v
     • Relevant bindings include
-        aux :: Id p (bound at T7453.hs:10:21)
+        aux :: Id t (bound at T7453.hs:10:21)
         z :: Id t (bound at T7453.hs:9:11)
         v :: p (bound at T7453.hs:7:7)
         cast1 :: p -> a (bound at T7453.hs:7:1)
 
-T7453.hs:15:15: error:
-    • Couldn't match type ‘p’ with ‘t1’
+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
         the type signature for:
           z :: forall t1. () -> t1
         at T7453.hs:14:11-22
-      Expected type: () -> t1
-        Actual type: () -> p
-    • In the expression: aux
-      In an equation for ‘z’:
-          z = aux
-            where
-                aux = const v
-      In an equation for ‘cast2’:
-          cast2 v
-            = z ()
-            where
-                z :: () -> t
-                z = aux
-                  where
-                      aux = const v
+    • In the first argument of ‘const’, namely ‘v’
+      In the expression: const v
+      In an equation for ‘aux’: aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> p (bound at T7453.hs:16:21)
+        aux :: b -> t1 (bound at T7453.hs:16:21)
         z :: () -> t1 (bound at T7453.hs:15:11)
         v :: p (bound at T7453.hs:13:7)
         cast2 :: p -> t (bound at T7453.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7696.stderr b/testsuite/tests/typecheck/should_fail/T7696.stderr
index eef19a5cfc..41f2296797 100644
--- a/testsuite/tests/typecheck/should_fail/T7696.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7696.stderr
@@ -1,7 +1,7 @@
 
 T7696.hs:7:6: error:
-    • Couldn't match type ‘() a0’ with ‘()’
+    • Couldn't match type ‘m0 a0’ with ‘()’
       Expected type: ((), w ())
-        Actual type: (() a0, w ())
+        Actual type: (m0 a0, t0 m0)
     • In the expression: f1
       In an equation for ‘f2’: f2 = f1
diff --git a/testsuite/tests/typecheck/should_fail/T8262.stderr b/testsuite/tests/typecheck/should_fail/T8262.stderr
index d52ee31a31..fb0d17aef5 100644
--- a/testsuite/tests/typecheck/should_fail/T8262.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8262.stderr
@@ -1,7 +1,11 @@
 
 T8262.hs:5:15: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘GHC.Prim.Int#’
+      When matching types
+        a :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
     • In the first argument of ‘Just’, namely ‘(1#)’
       In the expression: Just (1#)
       In an equation for ‘foo’: foo x = Just (1#)
+    • Relevant bindings include
+        foo :: p -> Maybe a (bound at T8262.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T8603.hs b/testsuite/tests/typecheck/should_fail/T8603.hs
index 90c1db3ad6..d17f246209 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.hs
+++ b/testsuite/tests/typecheck/should_fail/T8603.hs
@@ -10,6 +10,10 @@ newtype RV a = RV { getPDF :: [(Rational,a)] } deriving (Show, Eq)
 instance Functor RV where
   fmap f = RV . map (\(x,y) -> (x, f y)) . getPDF
 
+instance Applicative RV where
+  pure = return
+  (<*>) = ap
+
 instance Monad RV where
   return x = RV [(1,x)]
   rv >>= f = RV $
@@ -29,4 +33,4 @@ testRVState1
   = do prize <- lift uniform [1,2,3]
        return False
 
--- lift :: (MonadTrans t, Monad m) => m a -> t m a
\ No newline at end of file
+-- lift :: (MonadTrans t, Monad m) => m a -> t m a
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index d87bd635c4..d22d13f92b 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -1,19 +1,14 @@
 
-T8603.hs:13:10: error:
-    • No instance for (Applicative RV)
-        arising from the superclasses of an instance declaration
-    • In the instance declaration for ‘Monad RV’
-
-T8603.hs:29:17: error:
+T8603.hs:33:17: error:
     • Couldn't match type ‘RV a1’ with ‘StateT s RV a0’
       Expected type: [Integer] -> StateT s RV a0
-        Actual type: (->) ((->) [a1]) (RV a1)
+        Actual type: t0 ((->) [a1]) (RV a1)
     • The function ‘lift’ is applied to two arguments,
-      but its type ‘([a1] -> RV a1) -> (->) ((->) [a1]) (RV a1)’
+      but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’
       has only one
       In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
       In the expression:
         do prize <- lift uniform [1, 2, ....]
            return False
     • Relevant bindings include
-        testRVState1 :: RVState s Bool (bound at T8603.hs:28:1)
+        testRVState1 :: RVState s Bool (bound at T8603.hs:32:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 254e04b55d..06789ed71e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -446,3 +446,6 @@ test('T13677', normal, compile_fail, [''])
 test('T13821A', expect_broken(13821), run_command, ['$MAKE -s --no-print-directory T13821A'])
 test('T13821B', expect_broken(13821), backpack_typecheck_fail, [''])
 test('T13983', normal, compile_fail, [''])
+test('T13530', normal, compile_fail, [''])
+test('T12373', normal, compile_fail, [''])
+test('T13610', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail090.stderr b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
index 662d7da804..efb81e8ee6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail090.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
@@ -1,6 +1,8 @@
 
 tcfail090.hs:11:9: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘ByteArray#’
+      When matching types
+        a0 :: *
+        ByteArray# :: TYPE 'UnliftedRep
     • In the expression: my_undefined
       In an equation for ‘die’: die _ = my_undefined
diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
index a6fbc86c49..29a1576ddb 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
@@ -1,7 +1,11 @@
 
 tcfail122.hs:8:9: error:
-    • Couldn't match kind ‘*’ with ‘* -> *’
-      When matching the kind of ‘a’
+    • Couldn't match kind ‘* -> *’ with ‘*’
+      When matching types
+        c0 :: (* -> *) -> *
+        a :: * -> *
+      Expected type: a b
+        Actual type: c0 d0
     • In the expression:
           undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d
       In the expression:
diff --git a/testsuite/tests/typecheck/should_fail/tcfail123.stderr b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
index 8f5f0a0afe..ad512e102e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail123.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
@@ -1,7 +1,18 @@
 
 tcfail123.hs:11:9: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘GHC.Prim.Int#’
+      When matching types
+        p0 :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
+    • In the first argument of ‘f’, namely ‘3#’
+      In the expression: f 3#
+      In an equation for ‘h’: h v = f 3#
+
+tcfail123.hs:11:9: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        p0 :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
     • In the first argument of ‘f’, namely ‘3#’
       In the expression: f 3#
       In an equation for ‘h’: h v = f 3#
diff --git a/testsuite/tests/typecheck/should_fail/tcfail200.stderr b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
index 407265ee9d..fdd0e3c073 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail200.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
@@ -1,7 +1,11 @@
 
 tcfail200.hs:5:15: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘GHC.Prim.Int#’
+      When matching types
+        a1 :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
     • In the expression: 1#
       In the expression: (1#, 'c')
       In an equation for ‘x’: x = (1#, 'c')
+    • Relevant bindings include
+        x :: (a1, Char) (bound at tcfail200.hs:5:9)