Use the eager unifier in the constraint solver

This patch continues the refactoring of the constraint solver
described in #23070.

The Big Deal in this patch is to call the regular, eager unifier from the
constraint solver, when we want to create new equalities. This
replaces the existing, unifyWanted which amounted to
yet-another-unifier, so it reduces duplication of a rather subtle
piece of technology. See

  * Note [The eager unifier] in GHC.Tc.Utils.Unify
  * GHC.Tc.Solver.Monad.wrapUnifierTcS

I did lots of other refactoring along the way

* I simplified the treatment of right hand sides that contain CoercionHoles.
  Now, a constraint that contains a hetero-kind CoercionHole is non-canonical,
  and cannot be used for rewriting or unification alike.  This required me
  to add the ch_hertero_kind flag to CoercionHole, with consequent knock-on
  effects. See wrinkle (2) of `Note [Equalities with incompatible kinds]` in
  GHC.Tc.Solver.Equality.

* I refactored the StopOrContinue type to add StartAgain, so that after a
  fundep improvement (for example) we can simply start the pipeline again.

* I got rid of the unpleasant (and inefficient) rewriterSetFromType/Co functions.
  With Richard I concluded that they are never needed.

* I discovered Wrinkle (W1) in Note [Wanteds rewrite Wanteds] in
  GHC.Tc.Types.Constraint, and therefore now prioritise non-rewritten equalities.

Quite a few error messages change, I think always for the better.

Compiler runtime stays about the same, with one outlier: a 17% improvement in T17836

Metric Decrease:
    T17836
    T18223

36 files changed, 273 insertions, 145 deletions

diff --git a/testsuite/tests/dependent/should_fail/T11471.hs b/testsuite/tests/dependent/should_fail/T11471.hs
index ae09ae07bb..f9bc764f88 100644
--- a/testsuite/tests/dependent/should_fail/T11471.hs
+++ b/testsuite/tests/dependent/should_fail/T11471.hs
@@ -4,12 +4,14 @@ module T11471 where
 
 import GHC.Exts
 import Data.Proxy
+import Data.Kind
 
 type family F a :: k
 
 type instance F Int = Int#
 
-f :: Proxy a -> F a -> F a
+f :: forall (a :: Type). Proxy a -> F a -> F a
+-- NB: Those calls to F are (F @Type a)
 f _ x = x
 
 bad = f (undefined :: Proxy Int#) 3#
diff --git a/testsuite/tests/dependent/should_fail/T11471.stderr b/testsuite/tests/dependent/should_fail/T11471.stderr
index 377d1da759..8adeb4b280 100644
--- a/testsuite/tests/dependent/should_fail/T11471.stderr
+++ b/testsuite/tests/dependent/should_fail/T11471.stderr
@@ -1,5 +1,5 @@
 
-T11471.hs:15:10: error: [GHC-18872]
+T11471.hs:17:10: error: [GHC-18872]
     • Couldn't match a lifted type with an unlifted type
       When matching types
         a :: *
@@ -9,4 +9,14 @@ T11471.hs:15:10: error: [GHC-18872]
     • 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)
+    • Relevant bindings include bad :: F a (bound at T11471.hs:17:1)
+
+T11471.hs:17:35: error: [GHC-18872]
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        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 a (bound at T11471.hs:17:1)
diff --git a/testsuite/tests/impredicative/icfp20-fail.stderr b/testsuite/tests/impredicative/icfp20-fail.stderr
index a2fb0cad24..35079396f0 100644
--- a/testsuite/tests/impredicative/icfp20-fail.stderr
+++ b/testsuite/tests/impredicative/icfp20-fail.stderr
@@ -1,7 +1,6 @@
 
 icfp20-fail.hs:20:10: error: [GHC-83865]
-    • Couldn't match type: forall a. a -> a
-                     with: b -> b
+    • Couldn't match type ‘SId’ with ‘b -> b’
       Expected: SId -> b -> b
         Actual: SId -> SId
     • In the expression: id
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index 3f88289e23..701006258a 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: [GHC-83865]
-    • Couldn't match type: A3 (x (A2 (FCon x) -> A3 (FCon x)))
-                     with: A3 (FCon x)
+    • Couldn't match type: A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                     with: A2 (FCon x)
       Expected: x (A2 (FCon x) -> A3 (FCon x))
                 -> A2 (FCon x) -> A3 (FCon x)
         Actual: x (A2 (FCon x) -> A3 (FCon x))
                 -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
                 -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
-        NB: ‘A3’ is a non-injective type family
+      NB: ‘A2’ 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/T4254b.hs b/testsuite/tests/indexed-types/should_fail/T4254b.hs
index ffd117bc4c..44cdb5b602 100644
--- a/testsuite/tests/indexed-types/should_fail/T4254b.hs
+++ b/testsuite/tests/indexed-types/should_fail/T4254b.hs
@@ -11,3 +11,22 @@ fails :: forall a b. (a~Int,FD a b) => a -> Bool
 fails  = op
 -- Could fail: no proof that b~Bool
 -- But can also succeed; it's not a *wanted* constraint
+
+{- Interestingly, the ambiguity check for the type sig succeeds:
+
+[G] FD Int b
+[W] FD Int beta
+
+We get [W] beta~b; we unify immediately, and then solve.
+All before we interact the [W] FD Int beta with the
+top-level instances (which would give rise to [W] beta~Bool).
+
+One the other hand, from `fails = op` we get
+
+[G] FD Int b
+[W] FD Int Bool
+
+Interacting those two gives [W] b~Bool; bu this doesn't
+happen becase we now solve first.
+
+-}
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T4254b.stderr b/testsuite/tests/indexed-types/should_fail/T4254b.stderr
deleted file mode 100644
index 551978715c..0000000000
--- a/testsuite/tests/indexed-types/should_fail/T4254b.stderr
+++ /dev/null
@@ -1,20 +0,0 @@
-
-T4254b.hs:10:10: error: [GHC-25897]
-    • Couldn't match type ‘b’ with ‘Bool’
-        arising from a functional dependency between constraints:
-          ‘FD Int Bool’
-            arising from a type ambiguity check for
-            the type signature for ‘fails’ at T4254b.hs:10:10-48
-          ‘FD Int b’
-            arising from the type signature for:
-                           fails :: forall a b.
-                                    (a ~ Int, FD a b) =>
-                                    a -> Bool at T4254b.hs:10:10-48
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          fails :: forall a b. (a ~ Int, FD a b) => a -> Bool
-        at T4254b.hs:10:10-48
-    • In the ambiguity check for ‘fails’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature:
-        fails :: forall a b. (a ~ Int, FD a b) => a -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 43c8b26191..20e0084aa2 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,13 +1,13 @@
 
 T9662.hs:49:8: error: [GHC-25897]
-    • Couldn't match type ‘n’ with ‘Int’
+    • Couldn't match type ‘k’ with ‘Int’
       Expected: Exp (((sh :. k) :. m) :. n)
                 -> Exp (((sh :. m) :. n) :. k)
         Actual: Exp
                   (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
                 -> Exp
                      (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
-      ‘n’ is a rigid type variable bound by
+      ‘k’ is a rigid type variable bound by
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 325fbc0614..62eac96e84 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -58,7 +58,7 @@ test('T3330a', normal, compile_fail, [''])
 test('T3330b', normal, compile_fail, [''])
 test('T3330c', normal, compile_fail, [''])
 test('T4179', normal, compile_fail, [''])
-test('T4254b', normal, compile_fail, [''])
+test('T4254b', normal, compile, [''])
 test('T2239', normal, compile, [''])
 test('T3440', expect_broken(19974), compile_fail, [''])
 test('T4485', normal, compile_fail, [''])
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index fc3c1e0c8b..5614422045 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,7 +1,7 @@
 
 T14040a.hs:26:46: error: [GHC-46956]
-    • Couldn't match kind ‘k0’ with ‘WeirdList z’
-      Expected kind ‘WeirdList k0’,
+    • Couldn't match kind ‘k1’ with ‘WeirdList z’
+      Expected kind ‘WeirdList k1’,
         but ‘xs’ has kind ‘WeirdList (WeirdList z)’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
@@ -25,8 +25,8 @@ T14040a.hs:26:46: error: [GHC-46956]
                                                                                            -> p _ wl
 
 T14040a.hs:27:27: error: [GHC-46956]
-    • Couldn't match kind ‘k1’ with ‘z’
-      Expected kind ‘WeirdList k1’,
+    • Couldn't match kind ‘k0’ with ‘z’
+      Expected kind ‘WeirdList k0’,
         but ‘WeirdCons x xs’ has kind ‘WeirdList z’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index fcad722d63..b9beb8c49c 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -1,7 +1,7 @@
 
 T14584.hs:57:41: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
     • Could not deduce ‘SingI a’ arising from a use of ‘sing’
-      from the context: (Action act, Monoid a, Good m1)
+      from the context: (Action act, Monoid a, Good m)
         bound by the instance declaration at T14584.hs:55:10-89
     • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
@@ -10,23 +10,11 @@ T14584.hs:57:41: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
       In the expression:
         act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
 
-T14584.hs:57:41: warning: [GHC-06200] [-Wdeferred-type-errors (in -Wdefault)]
-    • Cannot use equality for substitution: a0 ~ a
-      Doing so would be ill-kinded.
-    • In the second argument of ‘fromSing’, namely
-        ‘(sing @m @a :: Sing _)’
-      In the fourth argument of ‘act’, namely
-        ‘(fromSing @m (sing @m @a :: Sing _))’
-      In the expression:
-        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
-    • Relevant bindings include
-        monHom :: a -> a (bound at T14584.hs:57:3)
-
 T14584.hs:57:50: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce ‘m1 ~ *’
-      from the context: (Action act, Monoid a, Good m1)
+    • Could not deduce ‘m ~ *’
+      from the context: (Action act, Monoid a, Good m)
         bound by the instance declaration at T14584.hs:55:10-89
-      ‘m1’ is a rigid type variable bound by
+      ‘m’ is a rigid type variable bound by
         the instance declaration
         at T14584.hs:55:10-89
     • In the type ‘a’
@@ -36,9 +24,8 @@ T14584.hs:57:50: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
         ‘(fromSing @m (sing @m @a :: Sing _))’
 
 T14584.hs:57:60: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘a0 :: m’
-      Where: ‘a0’ is an ambiguous type variable
-             ‘m’ is a rigid type variable bound by
+    • Found type wildcard ‘_’ standing for ‘a :: m’
+      Where: ‘a’, ‘m’ are rigid type variables bound by
                the instance declaration
                at T14584.hs:55:10-89
     • In the first argument of ‘Sing’, namely ‘_’
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
index aabc6130e3..ebbc115864 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
@@ -1,7 +1,7 @@
 
 T14584a.hs:12:5: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘()’ with actual type ‘m -> m’
-    • Probable cause: ‘id’ is applied to too few arguments
+    • Probable cause: ‘id @m :: _’ is applied to too few arguments
       In the expression: id @m :: _
       In an equation for ‘f’: f = id @m :: _
 
@@ -16,7 +16,11 @@ T14584a.hs:12:9: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘f’: f = id @m :: _
 
 T14584a.hs:12:14: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘()’
+    • Found type wildcard ‘_’ standing for ‘m -> m’
+      Where: ‘m’, ‘k’ are rigid type variables bound by
+               the type signature for:
+                 f :: forall {k} (m :: k). ()
+               at T14584a.hs:11:1-17
     • In an expression type signature: _
       In the expression: id @m :: _
       In an equation for ‘f’: f = id @m :: _
@@ -32,3 +36,11 @@ T14584a.hs:15:17: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
       In the expression: id @m
       In an equation for ‘h’: h = id @m
     • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
+
+T14584a.hs:16:8: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
+    • Probable cause: ‘h’ is applied to too few arguments
+      In the expression: h
+      In the expression: let h = id @m in h
+      In an equation for ‘g’: g = let h = id @m in h
+    • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
diff --git a/testsuite/tests/polykinds/T11399.hs b/testsuite/tests/polykinds/T11399.hs
index 56f3c11ef7..ffa3848dc6 100644
--- a/testsuite/tests/polykinds/T11399.hs
+++ b/testsuite/tests/polykinds/T11399.hs
@@ -8,3 +8,7 @@ newtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)
 -- UhOh :: forall (k : * -> *). k * -> *
 
 instance Functor a => Functor (UhOh a) where
+
+{- Functor expects (* -> *)
+   (UhOh a) :: k * -> *
+-}
\ No newline at end of file
diff --git a/testsuite/tests/polykinds/T11399.stderr b/testsuite/tests/polykinds/T11399.stderr
index a3baab2378..d8a6c83ecb 100644
--- a/testsuite/tests/polykinds/T11399.stderr
+++ b/testsuite/tests/polykinds/T11399.stderr
@@ -1,9 +1,6 @@
 
-T11399.hs:10:32: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
-      When matching kinds
-        a :: * -> *
-        TYPE :: GHC.Types.RuntimeRep -> *
+T11399.hs:10:32: error: [GHC-83865]
+    • Couldn't match kind ‘*’ with ‘GHC.Types.LiftedRep’
       Expected kind ‘* -> *’, but ‘UhOh a’ has kind ‘a (*) -> *’
     • In the first argument of ‘Functor’, namely ‘(UhOh a)’
       In the instance declaration for ‘Functor (UhOh a)’
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index 45ff51c259..df3868fb6c 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -12,9 +12,11 @@ T14172.hs:7:46: error: [GHC-88464]
         traverseCompose :: (a -> f b) -> g a -> f (h _)
 
 T14172.hs:8:19: error: [GHC-25897]
-    • 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
+    • Couldn't match type ‘a’ with ‘g'1 a'0’
+      Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a')
+        Actual: (Unwrapped (Compose f'0 g'1 a'0) -> f (Unwrapped (h a')))
+                -> Compose f'0 g'1 a'0 -> f (h a')
+      ‘a’ is a rigid type variable bound by
         the inferred type of
           traverseCompose :: (a -> f b) -> g a -> f (h a')
         at T14172.hs:7:1-47
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 2959f7669a..5b8ca76084 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -5,8 +5,8 @@ T14846.hs:38:8: error: [GHC-25897]
         Actual: Hom riki a a
       ‘ríki’ is a rigid type variable bound by
         the type signature for:
-          i :: forall {k4} {k5} {cls2 :: k5 -> Constraint} (xx :: k4)
-                      (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *).
+          i :: forall {k4} {k5} {cls1 :: k5 -> Constraint} (xx :: k4)
+                      (a :: Struct cls1) (ríki :: Struct cls1 -> Struct cls1 -> *).
                StructI xx a =>
                ríki a a
         at T14846.hs:38:8-48
@@ -23,8 +23,8 @@ T14846.hs:38:8: error: [GHC-25897]
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:44: error: [GHC-25897]
-    • Couldn't match kind ‘k3’ with ‘Struct cls2’
-      Expected kind ‘Struct cls2 -> Constraint’,
+    • Couldn't match kind ‘k3’ with ‘Struct cls1’
+      Expected kind ‘Struct cls1 -> Constraint’,
         but ‘cls’ has kind ‘k3 -> Constraint’
       ‘k3’ is a rigid type variable bound by
         the instance declaration
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index 3ee1032c0a..f89e54a249 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,12 +1,12 @@
 
 T9017.hs:8:7: error: [GHC-25897]
-    • Couldn't match kind ‘k2’ with ‘*’
+    • Couldn't match kind ‘k1’ with ‘*’
       When matching types
-        a0 :: * -> * -> *
-        a :: k1 -> k2 -> *
+        b0 :: *
+        b :: k1
       Expected: a b (m b)
         Actual: a0 b0 (m0 b0)
-      ‘k2’ is a rigid type variable bound by
+      ‘k1’ is a rigid type variable bound by
         the type signature for:
           foo :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1)
                         (m :: k1 -> k2).
diff --git a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
index 51a57fe27d..25a1fc1b6d 100644
--- a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
+++ b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
@@ -17,7 +17,7 @@ RepPolyRecordUpdate.hs:13:9: error: [GHC-55287]
     • The record update at field ‘fld’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE rep0
+        a :: TYPE rep0
       Cannot unify ‘rep’ with the type variable ‘rep0’
       because it is not a concrete ‘RuntimeRep’.
     • In a record update at field ‘fld’,
diff --git a/testsuite/tests/rep-poly/T13929.stderr b/testsuite/tests/rep-poly/T13929.stderr
index 837c1d4501..1789a7fdcb 100644
--- a/testsuite/tests/rep-poly/T13929.stderr
+++ b/testsuite/tests/rep-poly/T13929.stderr
@@ -3,7 +3,7 @@ T13929.hs:29:24: error: [GHC-55287]
     • The tuple argument in first position
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE k00
+        GUnboxed f rf :: TYPE k00
       Cannot unify ‘rf’ with the type variable ‘k00’
       because it is not a concrete ‘RuntimeRep’.
     • In the expression: (# gunbox x, gunbox y #)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
index 966e19bec7..c5e44796e1 100644
--- a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
+++ b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
@@ -1,7 +1,7 @@
 
 T14040.hs:27:46: error: [GHC-46956]
-    • Couldn't match kind ‘k0’ with ‘WeirdList z’
-      Expected kind ‘WeirdList k0’,
+    • Couldn't match kind ‘k1’ with ‘WeirdList z’
+      Expected kind ‘WeirdList k1’,
         but ‘xs’ has kind ‘WeirdList (WeirdList z)’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
@@ -25,8 +25,8 @@ T14040.hs:27:46: error: [GHC-46956]
                                                                                            -> p _ wl
 
 T14040.hs:28:27: error: [GHC-46956]
-    • Couldn't match kind ‘k1’ with ‘z’
-      Expected kind ‘WeirdList k1’,
+    • Couldn't match kind ‘k0’ with ‘z’
+      Expected kind ‘WeirdList k0’,
         but ‘WeirdCons x xs’ has kind ‘WeirdList z’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
diff --git a/testsuite/tests/typecheck/should_compile/T13651.stderr b/testsuite/tests/typecheck/should_compile/T13651.stderr
index 235d579739..a64d36e6ca 100644
--- a/testsuite/tests/typecheck/should_compile/T13651.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13651.stderr
@@ -1,6 +1,6 @@
 
 T13651.hs:12:8: error: [GHC-25897]
-    • Could not deduce ‘cs ~ Bar (Foo h) (Foo s)’
+    • Could not deduce ‘cr ~ Bar h (Foo r)’
       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:
@@ -8,7 +8,7 @@ T13651.hs:12:8: error: [GHC-25897]
                           (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
                           Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
         at T13651.hs:(12,8)-(14,65)
-      ‘cs’ is a rigid type variable bound by
+      ‘cr’ is a rigid type variable bound by
         the type signature for:
           foo :: forall cr cu h r u cs s.
                  (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
diff --git a/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr b/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
index 9ab5b25eac..3b4968c941 100644
--- a/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
+++ b/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
@@ -1,20 +1,20 @@
 
 AmbigFDs.hs:10:8: error: [GHC-25897]
-    • Couldn't match type ‘b1’ with ‘b2’
+    • Couldn't match type ‘b2’ with ‘b1’
         arising from a functional dependency between constraints:
-          ‘C a b2’
+          ‘C a b1’
             arising from a type ambiguity check for
             the type signature for ‘foo’ at AmbigFDs.hs:10:8-35
-          ‘C a b1’
+          ‘C a b2’
             arising from the type signature for:
                            foo :: forall a b1 b2.
                                   (C a b1, C a b2) =>
                                   a -> Int at AmbigFDs.hs:10:8-35
-      ‘b1’ is a rigid type variable bound by
+      ‘b2’ is a rigid type variable bound by
         the type signature for:
           foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int
         at AmbigFDs.hs:10:8-35
-      ‘b2’ is a rigid type variable bound by
+      ‘b1’ is a rigid type variable bound by
         the type signature for:
           foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int
         at AmbigFDs.hs:10:8-35
diff --git a/testsuite/tests/typecheck/should_fail/T16204c.stderr b/testsuite/tests/typecheck/should_fail/T16204c.stderr
index df0e1675b7..c91a2cc060 100644
--- a/testsuite/tests/typecheck/should_fail/T16204c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16204c.stderr
@@ -2,7 +2,7 @@
 T16204c.hs:16:8: error: [GHC-83865]
     • Couldn't match type ‘Rep’ with ‘*’
       Expected: Sing @(*) a
-        Actual: Sing @Rep a0
+        Actual: Sing @Rep a
     • In the first argument of ‘id’, namely ‘sTo’
       In the expression: id sTo
       In an equation for ‘x’: x = id sTo
diff --git a/testsuite/tests/typecheck/should_fail/T16512a.stderr b/testsuite/tests/typecheck/should_fail/T16512a.stderr
index e89900b083..be297ee6d9 100644
--- a/testsuite/tests/typecheck/should_fail/T16512a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16512a.stderr
@@ -1,20 +1,18 @@
 
 T16512a.hs:41:25: error: [GHC-25897]
-    • Couldn't match type ‘as’ with ‘a : as’
+    • Couldn't match type ‘b’ with ‘a -> b’
       Expected: AST (ListVariadic (a : as) b)
         Actual: AST (ListVariadic as (a -> b))
-      ‘as’ is a rigid type variable bound by
-        a pattern with constructor:
-          AnApplication :: forall (as :: [*]) b.
-                           AST (ListVariadic as b) -> ASTs as -> AnApplication b,
-        in a case alternative
-        at T16512a.hs:40:9-26
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          unapply :: forall b. AST b -> AnApplication b
+        at T16512a.hs:37:1-35
     • 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/T16946.stderr b/testsuite/tests/typecheck/should_fail/T16946.stderr
index c26e4fb339..19fe2a0b12 100644
--- a/testsuite/tests/typecheck/should_fail/T16946.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16946.stderr
@@ -1,16 +1,15 @@
 
 T16946.hs:11:9: error: [GHC-71451]
     • Cannot generalise type; skolem ‘k’ would escape its scope
-      if I tried to quantify (y0 :: k) in this type:
+      if I tried to quantify (x0 :: k) in this type:
         forall k (c :: k -> k -> *)
                (m :: forall (x :: k) (y :: k). c x y -> * -> *) a.
         CatMonad @k c m =>
-        a -> m @y0 @y0 (Id @{k} @y0 c) a
+        a -> m @x0 @x0 (Id @{k} @x0 c) a
       (Indeed, I sometimes struggle even printing this correctly,
        due to its ill-scoped nature.)
     • In the type signature:
         boom :: forall k
                        (c :: k -> k -> Type)
                        (m :: forall (x :: k) (y :: k). c x y -> Type -> Type)
-                       a.
-                CatMonad c m => a -> m (Id c) a
+                       a. CatMonad c m => a -> m (Id c) a
diff --git a/testsuite/tests/typecheck/should_fail/T17139.hs b/testsuite/tests/typecheck/should_fail/T17139.hs
index b4025588dd..4869e9559d 100644
--- a/testsuite/tests/typecheck/should_fail/T17139.hs
+++ b/testsuite/tests/typecheck/should_fail/T17139.hs
@@ -13,3 +13,46 @@ type family TypeFam f fun where
 
 lift :: (a -> b) -> TypeFam f (a -> b)
 lift f = \x -> _ (f <*> x)
+
+
+{-
+x              :: alpha
+body of lambda :: beta
+
+[W] TypeFam f (a->b) ~ (alpha -> beta)
+-->
+[W] (f a -> TypeFam f b) ~ (alpha -> beta)
+-->
+ alpha := f a
+ beta  := TypeFam f b
+
+(<*>) :: Applicative g => g (p -> q) -> g p -> g q
+
+f <*> x
+
+arg1
+  (a->b) ~ g0 (p0->q0)
+  g0 := ((->) a)
+  (p0 -> q0) ~ b   <---------
+arg2
+  alpha ~ g0 p0
+  g0 ~ f          <----------
+  p0 := a
+res
+  g0 q0
+
+Finish with
+ [W] f ~ (->) a
+ [W] b ~ (a -> q0)
+ --> rewrite b
+ [W] (a -> q0) ~ a -> (
+
+_ :: g0 q0 -> beta
+  :: (a -> q0) -> TypeFam f b
+  :: (a -> q0) -> TypeFam ((->) a) (a -> q0)
+  :: (a -> q0) -> (a->a) -> TypeFam (-> a) q0
+
+BUT we would get different error messages if we did
+   g0 := f
+and then encountered [W] g0 ~ ((->) a)
+-}
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_fail/T17139.stderr b/testsuite/tests/typecheck/should_fail/T17139.stderr
index f8ab95f5f8..1c253297d9 100644
--- a/testsuite/tests/typecheck/should_fail/T17139.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17139.stderr
@@ -1,8 +1,8 @@
 
 T17139.hs:15:16: error: [GHC-88464]
-    • Found hole: _ :: (a -> b0) -> f a -> TypeFam f b0
+    • Found hole: _ :: (a -> b0) -> (a -> a) -> TypeFam ((->) a) b0
       Where: ‘b0’ is an ambiguous type variable
-             ‘a’, ‘f’ are rigid type variables bound by
+             ‘a’ is a rigid type variable bound by
                the type signature for:
                  lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b)
                at T17139.hs:14:1-38
diff --git a/testsuite/tests/typecheck/should_fail/T18851c.stderr b/testsuite/tests/typecheck/should_fail/T18851c.stderr
index 58c15d1b77..ebe5f8621d 100644
--- a/testsuite/tests/typecheck/should_fail/T18851c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T18851c.stderr
@@ -2,13 +2,13 @@
 T18851c.hs:25:27: error: [GHC-25897]
     • Could not deduce ‘n2 ~ n1’
         arising from reasoning about an injective type family using constraints:
-          ‘Plus1 n2 ~ n’
-            arising from a type equality
-              VSucc (Plus1 n2) ~ VSucc n at T18851c.hs:25:27-33
           ‘Plus1 n1 ~ n’
+            arising from a type equality
+              VSucc (Plus1 n1) ~ VSucc n at T18851c.hs:25:27-33
+          ‘Plus1 n2 ~ n’
             arising from a pattern with constructor:
                            VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
-                         in an equation for ‘foo’ at T18851c.hs:25:6-12
+                         in an equation for ‘foo’ at T18851c.hs:25:16-22
       from the context: n ~ Plus1 n1
         bound by a pattern with constructor:
                    VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
diff --git a/testsuite/tests/typecheck/should_fail/T22707.hs b/testsuite/tests/typecheck/should_fail/T22707.hs
index 35b0817ec2..38606d57c0 100644
--- a/testsuite/tests/typecheck/should_fail/T22707.hs
+++ b/testsuite/tests/typecheck/should_fail/T22707.hs
@@ -3,11 +3,48 @@ module T22707 where
 newtype Cont o i a = Cont {runCont ::(a -> i) -> o }
 
 t1:: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
-t1 c = Cont $ \ati1tti2 -> (runCont c) (ati1tti2 $ \a -> evalCont (t1 c) >>== \ati1 -> return ati1 a )
+t1 c = Cont $ \ati1tti2 -> (runCont c) (ati1tti2 $ \xa -> evalCont (t1 c) >>== \ati1 -> return ati1 xa )
+
+
+{-  This is a complicated and confused program.
+    We end up unifying
+        m0 p0 q0 b0 ~ (->) LiftedRep LiftedRep t1 t2
+    which unifies q0~LiftedRep, and m0 with the (polymorphically-kinded)
+      (->) LiftedRep
+    Getting a decent error message out of this mess is a challenge!
+
+  runCont :: Cont oo ii aa -> ((aa -> ii) -> oo)
+  (>>==)  :: forall k (m:k->k->*->*) (p:k) (q:k) a.
+             PMonad m => m p q a -> (a -> m q r b) -> m p r b
+
+  c :: Cont (i2 -> o) i1 a
+  Result type: Cont o i2 (a -> i1)
+  Arg of cont: ((a->i1) -> i2) -> o
+  ati1tti2 :: (a->i1) -> i2
+  runCont c :: (a -> i1) -> i2 -> o
+  xa :: a -> i1
+  t1 c :: Cont o i2 (a -> i1)
+  evalCont (t1 c) :: o
+  (>>==) @k0,m0,p0,q0,a0,r0) (evalCont (t1 c))
+     [W] o ~ m0 p0 q0 a0
+  ati1 :: a10
+  return @m10 @a10 ati1 xa :: a11
+    [W] m10 a10 ~ (a -> i1) -> a11
+    => [W] m10 ~ (->) @LiftedRep @LiftedRep (a -> i1) 
+       [W] a10 ~ a11
+  Result of (\ati1 -> ..)
+    (>>==) @m0,p0,q0,a0) (evalCont (t1 c)) (\ati1 -> ..) :: m0 p0 r0 b0
+    [W] a11 ~ m0 q0 r0 b0
+  Result of (>>==) call
+    [W] i1 ~ m0 p0 r0 b0
+-}
 
 evalCont:: Cont o a a -> o
 evalCont c = (runCont c)id
 
+instance Functor (Cont p p) where
+instance Applicative (Cont p p) where
+
 instance Monad (Cont p p) where
   return a = Cont ($ a)
   (>>=) = (>>==)
diff --git a/testsuite/tests/typecheck/should_fail/T22707.stderr b/testsuite/tests/typecheck/should_fail/T22707.stderr
index 0620e5996f..92ebbf6c00 100644
--- a/testsuite/tests/typecheck/should_fail/T22707.stderr
+++ b/testsuite/tests/typecheck/should_fail/T22707.stderr
@@ -1,16 +1,46 @@
 
-T22707.hs:6:37: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
-      When matching types
-        p0 :: *
-        GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
-      Expected: Cont o i1 a
-        Actual: Cont (i2 -> o) i1 a
-    • In the first argument of ‘runCont’, namely ‘c’
-      In the expression:
-        (runCont c)
-          (ati1tti2 $ \ a -> evalCont (t1 c) >>== \ ati1 -> return ati1 a)
+T22707.hs:6:59: error: [GHC-25897]
+    • Couldn't match expected type ‘i1’
+                  with actual type ‘m0 GHC.Types.LiftedRep GHC.Types.LiftedRep b0’
+      ‘i1’ is a rigid type variable bound by
+        the type signature for:
+          t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
+        at T22707.hs:5:1-47
+    • In the expression: evalCont (t1 c) >>== \ ati1 -> return ati1 xa
       In the second argument of ‘($)’, namely
-        ‘\ ati1tti2
-           -> (runCont c)
-                (ati1tti2 $ \ a -> evalCont (t1 c) >>== \ ati1 -> ...)’
+        ‘\ xa -> evalCont (t1 c) >>== \ ati1 -> return ati1 xa’
+      In the second argument of ‘runCont’, namely
+        ‘(ati1tti2
+            $ \ xa -> evalCont (t1 c) >>== \ ati1 -> return ati1 xa)’
+    • Relevant bindings include
+        ati1tti2 :: (a -> i1) -> i2 (bound at T22707.hs:6:16)
+        c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4)
+        t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
+          (bound at T22707.hs:6:1)
+
+T22707.hs:6:72: error: [GHC-25897]
+    • Couldn't match type ‘o’
+                     with ‘m0
+                             GHC.Types.LiftedRep
+                             GHC.Types.LiftedRep
+                             (m0 GHC.Types.LiftedRep GHC.Types.LiftedRep b0)’
+      Expected: Cont
+                  ((a -> i1)
+                   -> m0
+                        GHC.Types.LiftedRep
+                        GHC.Types.LiftedRep
+                        (m0 GHC.Types.LiftedRep GHC.Types.LiftedRep b0))
+                  i1
+                  a
+        Actual: Cont (i2 -> o) i1 a
+      ‘o’ is a rigid type variable bound by
+        the type signature for:
+          t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
+        at T22707.hs:5:1-47
+    • In the first argument of ‘t1’, namely ‘c’
+      In the first argument of ‘evalCont’, namely ‘(t1 c)’
+      In the first argument of ‘(>>==)’, namely ‘evalCont (t1 c)’
+    • Relevant bindings include
+        c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4)
+        t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
+          (bound at T22707.hs:6:1)
diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index cba7dda734..0482cc63ba 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -1,9 +1,7 @@
 
-T3950.hs:16:13: error: [GHC-18872]
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching types
-        w :: (* -> * -> *) -> *
-        Sealed :: (* -> *) -> *
+T3950.hs:16:13: error: [GHC-83865]
+    • Couldn't match type: Id p0 x0
+                     with: Id p
       Expected: w (Id p)
         Actual: Sealed (Id p0 x0)
     • In the first argument of ‘Just’, namely ‘rp'’
diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr
index 1485c88084..26f1c251e2 100644
--- a/testsuite/tests/typecheck/should_fail/T7368.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368.stderr
@@ -1,6 +1,6 @@
 
 T7368.hs:3:10: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘* -> *’
+    • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
         b0 :: *
         Maybe :: * -> *
diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr
index 7f9c97bce7..e60aaf8c39 100644
--- a/testsuite/tests/typecheck/should_fail/T7368a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr
@@ -1,9 +1,9 @@
 
 T7368a.hs:8:6: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘* -> *’
+    • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
-        f :: * -> *
-        Bad :: (* -> *) -> *
+        w0 :: * -> *
+        Bad f :: *
       Expected: f (Bad f)
         Actual: Bad w0
     • In the pattern: Bad x
diff --git a/testsuite/tests/typecheck/should_fail/T7696.stderr b/testsuite/tests/typecheck/should_fail/T7696.stderr
index 92f6be0211..aea284c74b 100644
--- a/testsuite/tests/typecheck/should_fail/T7696.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7696.stderr
@@ -1,12 +1,7 @@
 
-T7696.hs:9:6: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘* -> *’
-      When matching types
-        t0 :: (* -> *) -> *
-        w :: * -> *
+T7696.hs:9:6: error: [GHC-83865]
+    • Couldn't match type ‘m0 a0’ with ‘()’
       Expected: ((), w ())
         Actual: (m0 a0, t0 m0)
     • In the expression: f1
       In an equation for ‘f2’: f2 = f1
-    • Relevant bindings include
-        f2 :: ((), w ()) (bound at T7696.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr
index d8532ea365..f6aa8d0bfc 100644
--- a/testsuite/tests/typecheck/should_fail/T7869.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7869.stderr
@@ -1,16 +1,18 @@
 
 T7869.hs:3:12: error: [GHC-25897]
-    • Couldn't match type ‘b1’ with ‘b’
+    • Couldn't match type ‘a1’ with ‘a’
       Expected: [a1] -> b1
         Actual: [a] -> b
-      ‘b1’ is a rigid type variable bound by
+      ‘a1’ 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
+      ‘a’ is a rigid type variable bound by
         the inferred type of f :: [a] -> b
         at T7869.hs:3:1-27
     • In the expression: f x
       In the expression: (\ x -> f x) :: [a] -> b
       In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
+    • Relevant bindings include
+        x :: [a1] (bound at T7869.hs:3:7)
+        f :: [a] -> b (bound at T7869.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index fcb1b8828b..3eb958919f 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -2,14 +2,28 @@
 T8603.hs:33:17: error: [GHC-18872]
     • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
-        m0 :: * -> *
+        (->) [a1] :: * -> *
         [a2] :: *
       Expected: [a2] -> StateT s RV a0
-        Actual: t0 m0 (StateT s RV a0)
+        Actual: t0 ((->) [a1]) (StateT s RV a0)
     • The function ‘lift’ is applied to two value arguments,
-        but its type ‘m0 (StateT s RV a0) -> t0 m0 (StateT s RV a0)’
+        but its type ‘([a1] -> StateT s RV a0)
+                      -> t0 ((->) [a1]) (StateT s RV a0)’
         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
+
+T8603.hs:33:22: error: [GHC-83865]
+    • Couldn't match type: RV a1
+                     with: StateT s RV a0
+      Expected: [a1] -> StateT s RV a0
+        Actual: [a1] -> RV a1
+    • In the first argument of ‘lift’, namely ‘uniform’
+      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:32:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
index 58bb3d2389..84437750a1 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
@@ -1,9 +1,9 @@
 
 tcfail122.hs:9:9: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘* -> *’
+    • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
-        c0 :: (* -> *) -> *
-        a :: * -> *
+        d0 :: * -> *
+        b :: *
       Expected: a b
         Actual: c0 d0
     • In the expression: