Rework the handling of SkolemInfo

The main purpose of this patch is to attach a SkolemInfo directly to
each SkolemTv. This fixes the large number of bugs which have
accumulated over the years where we failed to report errors due to
having "no skolem info" for particular type variables. Now the origin of
each type varible is stored on the type variable we can always report
accurately where it cames from.

Fixes #20969 #20732 #20680 #19482 #20232 #19752 #10946
  #19760 #20063 #13499 #14040

The main changes of this patch are:

* SkolemTv now contains a SkolemInfo field which tells us how the
  SkolemTv was created. Used when reporting errors.

* Enforce invariants relating the SkolemInfoAnon and level of an implication (ic_info, ic_tclvl)
  to the SkolemInfo and level of the type variables in ic_skols.
    * All ic_skols are TcTyVars -- Check is currently disabled
    * All ic_skols are SkolemTv
    * The tv_lvl of the ic_skols agrees with the ic_tclvl
    * The ic_info agrees with the SkolInfo of the implication.

  These invariants are checked by a debug compiler by
  checkImplicationInvariants.

* Completely refactor kcCheckDeclHeader_sig which kept
  doing my head in. Plus, it wasn't right because it wasn't skolemising
  the binders as it decomposed the kind signature.

  The new story is described in Note [kcCheckDeclHeader_sig].  The code
  is considerably shorter than before (roughly 240 lines turns into 150
  lines).

  It still has the same awkward complexity around computing arity as
  before, but that is a language design issue.
  See Note [Arity inference in kcCheckDeclHeader_sig]

* I added new type synonyms MonoTcTyCon and PolyTcTyCon, and used
  them to be clear which TcTyCons have "finished" kinds etc, and
  which are monomorphic. See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]

* I renamed etaExpandAlgTyCon to splitTyConKind, becuase that's a
  better name, and it is very useful in kcCheckDeclHeader_sig, where
  eta-expansion isn't an issue.

* Kill off the nasty `ClassScopedTvEnv` entirely.

Co-authored-by: Simon Peyton Jones <simon.peytonjones@gmail.com>

75 files changed, 525 insertions, 91 deletions

diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
index 889d51b1cf..3f3c88a3e6 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.stderr
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -1,5 +1,5 @@
 
 T14066a.hs:14:3: warning:
     Type family instance equation is overlapped:
-      forall {c} {d} {x :: c} {y :: d}.
+      forall {c} {x :: c} {d} {y :: d}.
         Bar x y = Bool -- Defined at T14066a.hs:14:3
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index 3637dece24..f5aee5a1eb 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -1,5 +1,5 @@
 
-BadTelescope2.hs:9:8: error:
+BadTelescope2.hs:9:15: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr
index 02daf9d742..b5e4ce9c3a 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr
@@ -2,7 +2,7 @@
 BadTelescope5.hs:10:81: error:
     • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
       ‘k’ is a rigid type variable bound by
-        an explicit forall a k (b :: k) (c :: Proxy b) (d :: Proxy a)
+        the type signature for ‘bar’
         at BadTelescope5.hs:10:17
     • In the second argument of ‘SameKind’, namely ‘d’
       In the type signature:
diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr
index 3e3fa61a9b..6cdcf96369 100644
--- a/testsuite/tests/dependent/should_fail/T13780a.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780a.stderr
@@ -3,7 +3,7 @@ T13780a.hs:9:40: error:
     • Couldn't match kind ‘a’ with ‘Bool’
       Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
       ‘a’ is a rigid type variable bound by
-        the data constructor ‘SMkFoo’
+        a family instance declaration
         at T13780a.hs:9:20-31
     • In the second argument of ‘(~)’, namely ‘MkFoo’
       In the definition of data constructor ‘SMkFoo’
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
index 240108c296..20c82215ed 100644
--- a/testsuite/tests/dependent/should_fail/T14066.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -4,7 +4,7 @@ T14066.hs:15:59: error:
         because kind variable ‘k’ would escape its scope
       This (rigid, skolem) kind variable is bound by
         an explicit forall k (b :: k)
-        at T14066.hs:15:29-59
+        at T14066.hs:15:36-45
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature: g :: forall k (b :: k). SameKind a b
       In the expression:
diff --git a/testsuite/tests/dependent/should_fail/T16344a.stderr b/testsuite/tests/dependent/should_fail/T16344a.stderr
index 8325bf4169..ab3b991293 100644
--- a/testsuite/tests/dependent/should_fail/T16344a.stderr
+++ b/testsuite/tests/dependent/should_fail/T16344a.stderr
@@ -2,7 +2,7 @@
 T16344a.hs:11:36: error:
     • Expected a type, but ‘a’ has kind ‘ka’
       ‘ka’ is a rigid type variable bound by
-        the data constructor ‘MkT2’
+        the data type declaration for ‘T2’
         at T16344a.hs:11:9-10
     • In the second argument of ‘T2’, namely ‘a’
       In the type ‘(T2 Type a)’
diff --git a/testsuite/tests/dependent/should_fail/T16418.stderr b/testsuite/tests/dependent/should_fail/T16418.stderr
index fa2263abd3..a286d77805 100644
--- a/testsuite/tests/dependent/should_fail/T16418.stderr
+++ b/testsuite/tests/dependent/should_fail/T16418.stderr
@@ -1,5 +1,5 @@
 
-T16418.hs:9:6: error:
+T16418.hs:9:13: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
index d642d6201c..b8ccbdfc9f 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
@@ -4,6 +4,6 @@ TypeSkolEscape.hs:9:52: error:
         because kind variable ‘v’ would escape its scope
       This (rigid, skolem) kind variable is bound by
         an explicit forall (v :: RuntimeRep) (a :: TYPE v)
-        at TypeSkolEscape.hs:9:12-52
+        at TypeSkolEscape.hs:9:19-49
     • In the type ‘forall (v :: RuntimeRep) (a :: TYPE v). a’
       In the type declaration for ‘Bad’
diff --git a/testsuite/tests/deriving/should_compile/T14579.stderr b/testsuite/tests/deriving/should_compile/T14579.stderr
index 31545c6de7..7ba5c6a2f0 100644
--- a/testsuite/tests/deriving/should_compile/T14579.stderr
+++ b/testsuite/tests/deriving/should_compile/T14579.stderr
@@ -22,22 +22,18 @@ Derived class instances:
   instance forall a (x :: Data.Proxy.Proxy a).
            GHC.Classes.Eq a =>
            GHC.Classes.Eq (T14579.Wat x) where
-    (GHC.Classes.==) ::
-      T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool
-    (GHC.Classes./=) ::
-      T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool
+    (GHC.Classes.==) :: T14579.Wat x -> T14579.Wat x -> GHC.Types.Bool
+    (GHC.Classes./=) :: T14579.Wat x -> T14579.Wat x -> GHC.Types.Bool
     (GHC.Classes.==)
       = GHC.Prim.coerce
-          @(GHC.Maybe.Maybe a[sk:1]
-            -> GHC.Maybe.Maybe a[sk:1] -> GHC.Types.Bool)
-          @(T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool)
-          ((GHC.Classes.==) @(GHC.Maybe.Maybe a[sk:1]))
+          @(GHC.Maybe.Maybe a -> GHC.Maybe.Maybe a -> GHC.Types.Bool)
+          @(T14579.Wat x -> T14579.Wat x -> GHC.Types.Bool)
+          ((GHC.Classes.==) @(GHC.Maybe.Maybe a))
     (GHC.Classes./=)
       = GHC.Prim.coerce
-          @(GHC.Maybe.Maybe a[sk:1]
-            -> GHC.Maybe.Maybe a[sk:1] -> GHC.Types.Bool)
-          @(T14579.Wat x[sk:1] -> T14579.Wat x[sk:1] -> GHC.Types.Bool)
-          ((GHC.Classes./=) @(GHC.Maybe.Maybe a[sk:1]))
+          @(GHC.Maybe.Maybe a -> GHC.Maybe.Maybe a -> GHC.Types.Bool)
+          @(T14579.Wat x -> T14579.Wat x -> GHC.Types.Bool)
+          ((GHC.Classes./=) @(GHC.Maybe.Maybe a))
   
 
 Derived type family instances:
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr
index 53fd60fd80..eb3d88f323 100644
--- a/testsuite/tests/indexed-types/should_compile/T15852.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr
@@ -3,10 +3,10 @@ TYPE CONSTRUCTORS
     roles nominal nominal nominal
 COERCION AXIOMS
   axiom T15852.D:R:DFProxyProxy0 ::
-    forall k1 (j :: k1) k2 (c :: k2).
-      DF (Proxy c) = T15852.R:DFProxyProxy k1 j k2 c
+    forall k1 k2 (c :: k1) (j :: k2).
+      DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 c j
 FAMILY INSTANCES
-  data instance forall {k1} {j :: k1} {k2} {c :: k2}.
+  data instance forall {k1} {k2} {c :: k1} {j :: k2}.
                   DF (Proxy c) -- Defined at T15852.hs:10:15
 Dependent modules: []
 Dependent packages: [base-4.16.0.0]
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr
index 7968dc3dda..198ec75797 100644
--- a/testsuite/tests/indexed-types/should_fail/T15870.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr
@@ -6,7 +6,7 @@ T15870.hs:32:34: error:
         a :: k
       Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
       ‘k’ is a rigid type variable bound by
-        a family instance declaration
+        the instance declaration
         at T15870.hs:(27,1)-(32,35)
     • In the second argument of ‘Get’, namely ‘g2’
       In the type ‘Get a g2’
diff --git a/testsuite/tests/partial-sigs/should_compile/T12033.stderr b/testsuite/tests/partial-sigs/should_compile/T12033.stderr
index 780fb9d41b..9f9fdd6a17 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12033.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12033.stderr
@@ -1,15 +1,15 @@
 
 T12033.hs:12:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘v -> t’
-      Where: ‘t’ is a rigid type variable bound by
+      Where: ‘v’ is a rigid type variable bound by
+               the type signature for:
+                 tripleStoreToRuleSet :: forall v. v -> v
+               at T12033.hs:6:1-30
+             ‘t’ is a rigid type variable bound by
                the inferred types of
                  makeTuple :: v -> t
                  makeExpression :: v -> t
                at T12033.hs:(11,4)-(13,39)
-             ‘v’ is a rigid type variable bound by
-               the type signature for:
-                 tripleStoreToRuleSet :: forall v. v -> v
-               at T12033.hs:6:1-30
     • In the type signature: makeExpression :: _
       In an equation for ‘tripleStoreToRuleSet’:
           tripleStoreToRuleSet getAtom
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 8e2d02e9b3..18f8439a7f 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -7,7 +7,7 @@ T14040a.hs:26:46: error:
       This (rigid, skolem) kind variable is bound by
         an explicit forall (z :: Type) (x :: z)
                            (xs :: WeirdList (WeirdList z))
-        at T14040a.hs:(25,19)-(27,41)
+        at T14040a.hs:25:26-77
     • In the second argument of ‘p’, namely ‘xs’
       In the type ‘Sing wl
                    -> (forall (y :: Type). p _ WeirdNil)
@@ -37,7 +37,7 @@ T14040a.hs:27:27: error:
       This (rigid, skolem) kind variable is bound by
         an explicit forall (z :: Type) (x :: z)
                            (xs :: WeirdList (WeirdList z))
-        at T14040a.hs:(25,19)-(27,41)
+        at T14040a.hs:25:26-77
     • In the second argument of ‘p’, namely ‘(WeirdCons x xs)’
       In the type ‘Sing wl
                    -> (forall (y :: Type). p _ WeirdNil)
diff --git a/testsuite/tests/patsyn/should_fail/T15694.stderr b/testsuite/tests/patsyn/should_fail/T15694.stderr
index 2c3421321c..e3827b28c1 100644
--- a/testsuite/tests/patsyn/should_fail/T15694.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15694.stderr
@@ -2,7 +2,6 @@
 T15694.hs:23:35: error:
     • Expected kind ‘k1 -> k0’, but ‘f a1’ has kind ‘ks’
       ‘ks’ is a rigid type variable bound by
-        an explicit forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks)
-                           (ks1 :: Type) k1 (a2 :: k1) (ctx1 :: Ctx ks1) a3
+        the type signature for ‘ASSO’
         at T15694.hs:19:30-31
     • In the first argument of ‘(~~)’, namely ‘f a1 a2’
diff --git a/testsuite/tests/polykinds/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr
index f96278a5e7..e061d41bce 100644
--- a/testsuite/tests/polykinds/T11142.stderr
+++ b/testsuite/tests/polykinds/T11142.stderr
@@ -4,7 +4,7 @@ T11142.hs:9:49: error:
         because kind variable ‘k’ would escape its scope
       This (rigid, skolem) kind variable is bound by
         an explicit forall k (a :: k)
-        at T11142.hs:9:19-49
+        at T11142.hs:9:26-35
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature:
         foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
diff --git a/testsuite/tests/polykinds/T15787.stderr b/testsuite/tests/polykinds/T15787.stderr
index 4ab01d58fc..c2c50af86a 100644
--- a/testsuite/tests/polykinds/T15787.stderr
+++ b/testsuite/tests/polykinds/T15787.stderr
@@ -2,7 +2,7 @@
 T15787.hs:16:14: error:
     • Expected a type, but ‘k’ has kind ‘ob1’
       ‘ob1’ is a rigid type variable bound by
-        the data constructor ‘Kl’
+        the type signature for ‘Kl’
         at T15787.hs:16:3-43
     • In the type ‘k’
       In the definition of data constructor ‘Kl’
diff --git a/testsuite/tests/polykinds/T16221a.stderr b/testsuite/tests/polykinds/T16221a.stderr
index 5945369a6c..06fb5e0af1 100644
--- a/testsuite/tests/polykinds/T16221a.stderr
+++ b/testsuite/tests/polykinds/T16221a.stderr
@@ -1,11 +1,11 @@
 
 T16221a.hs:6:49: error:
-    • Expected kind ‘k’, but ‘b’ has kind ‘k2’
-      ‘k2’ is a rigid type variable bound by
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
+      ‘k1’ is a rigid type variable bound by
         an explicit forall k (b :: k)
         at T16221a.hs:6:20
       ‘k’ is a rigid type variable bound by
-        the data constructor ‘MkT2’
+        the data type declaration for ‘T2’
         at T16221a.hs:6:20
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type ‘(SameKind a b)’
diff --git a/testsuite/tests/polykinds/T16245a.stderr b/testsuite/tests/polykinds/T16245a.stderr
index 0023432858..c47e088434 100644
--- a/testsuite/tests/polykinds/T16245a.stderr
+++ b/testsuite/tests/polykinds/T16245a.stderr
@@ -2,10 +2,10 @@
 T16245a.hs:11:66: error:
     • Expected kind ‘k’, but ‘b’ has kind ‘k1’
       ‘k1’ is a rigid type variable bound by
-        the data constructor ‘MkT’
+        the newtype declaration for ‘T’
         at T16245a.hs:11:12
       ‘k’ is a rigid type variable bound by
-        the data constructor ‘MkT’
+        the newtype declaration for ‘T’
         at T16245a.hs:11:1-67
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type ‘(forall (b :: k). SameKind a b)’
diff --git a/testsuite/tests/polykinds/T16247.stderr b/testsuite/tests/polykinds/T16247.stderr
index 34a1319996..dc637bee4a 100644
--- a/testsuite/tests/polykinds/T16247.stderr
+++ b/testsuite/tests/polykinds/T16247.stderr
@@ -1,5 +1,5 @@
 
-T16247.hs:9:13: error:
+T16247.hs:9:20: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
diff --git a/testsuite/tests/polykinds/T16247a.stderr b/testsuite/tests/polykinds/T16247a.stderr
index ce75878f38..0205a74429 100644
--- a/testsuite/tests/polykinds/T16247a.stderr
+++ b/testsuite/tests/polykinds/T16247a.stderr
@@ -1,5 +1,5 @@
 
-T16247a.hs:21:21: error:
+T16247a.hs:21:28: error:
     • These kind and type variables: p k
       are out of dependency order. Perhaps try this ordering:
         k (p :: k)
diff --git a/testsuite/tests/polykinds/T16762.stderr b/testsuite/tests/polykinds/T16762.stderr
index 6335fa4c50..6793e5220e 100644
--- a/testsuite/tests/polykinds/T16762.stderr
+++ b/testsuite/tests/polykinds/T16762.stderr
@@ -1,5 +1,5 @@
 
-T16762.hs:11:3: error:
+T16762.hs:11:17: error:
     • These kind and type variables: a kx (b :: kx)
       are out of dependency order. Perhaps try this ordering:
         kx (a :: kx) (b :: kx)
diff --git a/testsuite/tests/polykinds/T16762c.stderr b/testsuite/tests/polykinds/T16762c.stderr
index 5be6fbb462..aa813f345b 100644
--- a/testsuite/tests/polykinds/T16762c.stderr
+++ b/testsuite/tests/polykinds/T16762c.stderr
@@ -1,5 +1,5 @@
 
-T16762c.hs:10:10: error:
+T16762c.hs:10:17: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr
index 69022b3a1a..2472fdcb34 100644
--- a/testsuite/tests/polykinds/T16902.stderr
+++ b/testsuite/tests/polykinds/T16902.stderr
@@ -2,7 +2,7 @@
 T16902.hs:12:10: error:
     • Expected a type, but found something with kind ‘a’
       ‘a’ is a rigid type variable bound by
-        the data constructor ‘MkF’
+        the type signature for ‘MkF’
         at T16902.hs:12:3-12
     • In the type ‘F a’
       In the definition of data constructor ‘MkF’
diff --git a/testsuite/tests/polykinds/T17963.stderr b/testsuite/tests/polykinds/T17963.stderr
index aa0e4d0d3e..94f730cb30 100644
--- a/testsuite/tests/polykinds/T17963.stderr
+++ b/testsuite/tests/polykinds/T17963.stderr
@@ -6,7 +6,7 @@ T17963.hs:15:23: error:
         ob :: TYPE rep
       ‘rep’ is a rigid type variable bound by
         the class declaration for ‘Category'’
-        at T17963.hs:13:27-29
+        at T17963.hs:14:18-35
     • In the first argument of ‘cat’, namely ‘a’
       In the type signature: id' :: forall a. cat a a
       In the class declaration for ‘Category'’
diff --git a/testsuite/tests/polykinds/T18451a.stderr b/testsuite/tests/polykinds/T18451a.stderr
index fbfd3ce288..b7ad0ee898 100644
--- a/testsuite/tests/polykinds/T18451a.stderr
+++ b/testsuite/tests/polykinds/T18451a.stderr
@@ -1,5 +1,5 @@
 
-T18451a.hs:10:8: error:
+T18451a.hs:10:15: error:
     • These kind and type variables: a b (c :: Const Type b)
       are out of dependency order. Perhaps try this ordering:
         (b :: k) (a :: Const (*) b) (c :: Const (*) b)
diff --git a/testsuite/tests/polykinds/T18451b.stderr b/testsuite/tests/polykinds/T18451b.stderr
index d12d9b382a..458d39105e 100644
--- a/testsuite/tests/polykinds/T18451b.stderr
+++ b/testsuite/tests/polykinds/T18451b.stderr
@@ -1,5 +1,5 @@
 
-T18451b.hs:10:8: error:
+T18451b.hs:10:15: error:
     • These kind and type variables: a b (c :: Const Type b)
       are out of dependency order. Perhaps try this ordering:
         (b :: k) (a :: Const (*) b) (c :: Const (*) b)
diff --git a/testsuite/tests/polykinds/TyVarTvKinds3.stderr b/testsuite/tests/polykinds/TyVarTvKinds3.stderr
index 872fe96684..a267c3dc82 100644
--- a/testsuite/tests/polykinds/TyVarTvKinds3.stderr
+++ b/testsuite/tests/polykinds/TyVarTvKinds3.stderr
@@ -2,10 +2,10 @@
 TyVarTvKinds3.hs:9:62: error:
     • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
       ‘k2’ is a rigid type variable bound by
-        an explicit forall k1 k2 (a :: k1) (b :: k2)
+        the type signature for ‘MkBad’
         at TyVarTvKinds3.hs:9:22-23
       ‘k1’ is a rigid type variable bound by
-        an explicit forall k1 k2 (a :: k1) (b :: k2)
+        the type signature for ‘MkBad’
         at TyVarTvKinds3.hs:9:19-20
     • In the second argument of ‘SameKind’, namely ‘b’
       In the first argument of ‘Bad’, namely ‘(SameKind a b)’
diff --git a/testsuite/tests/saks/should_compile/saks023.stdout b/testsuite/tests/saks/should_compile/saks023.stdout
index 051268aa78..c779a9c938 100644
--- a/testsuite/tests/saks/should_compile/saks023.stdout
+++ b/testsuite/tests/saks/should_compile/saks023.stdout
@@ -1 +1 @@
-T :: forall x -> Type
+T :: forall a -> Type
diff --git a/testsuite/tests/saks/should_compile/saks034.stdout b/testsuite/tests/saks/should_compile/saks034.stdout
index 9877dc5d39..48ccab7e25 100644
--- a/testsuite/tests/saks/should_compile/saks034.stdout
+++ b/testsuite/tests/saks/should_compile/saks034.stdout
@@ -1,2 +1,2 @@
-C :: j -> Constraint
-T :: forall j -> j -> Type
+C :: k -> Constraint
+T :: forall k -> k -> Type
diff --git a/testsuite/tests/saks/should_compile/saks035.stdout b/testsuite/tests/saks/should_compile/saks035.stdout
index e52a24b69a..37328e26a0 100644
--- a/testsuite/tests/saks/should_compile/saks035.stdout
+++ b/testsuite/tests/saks/should_compile/saks035.stdout
@@ -1,2 +1,2 @@
-C :: forall {k} (i :: k). Proxy i -> Constraint
+C :: forall {k} (z :: k). Proxy z -> Constraint
 F :: k -> Type
diff --git a/testsuite/tests/saks/should_fail/T16758.stderr b/testsuite/tests/saks/should_fail/T16758.stderr
index f74241a706..066a4f106a 100644
--- a/testsuite/tests/saks/should_fail/T16758.stderr
+++ b/testsuite/tests/saks/should_fail/T16758.stderr
@@ -3,6 +3,6 @@ T16758.hs:14:8: error:
     • Couldn't match expected kind ‘Int’ with actual kind ‘a’
       ‘a’ is a rigid type variable bound by
         the class declaration for ‘C’
-        at T16758.hs:12:19
+        at T16758.hs:13:9
     • In the type signature: f :: C a => a -> Int
       In the class declaration for ‘C’
diff --git a/testsuite/tests/saks/should_fail/T20916.hs b/testsuite/tests/saks/should_fail/T20916.hs
new file mode 100644
index 0000000000..f62aa4caab
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/T20916.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-}
+
+module T20916 where
+
+import Data.Kind
+
+type T3 :: k -> k -> Type
+data T3 (a :: p) (b :: q) = MkT
+-- Should fail because p and q are bound the same kind variable
diff --git a/testsuite/tests/saks/should_fail/T20916.stderr b/testsuite/tests/saks/should_fail/T20916.stderr
new file mode 100644
index 0000000000..aeef4ca438
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/T20916.stderr
@@ -0,0 +1,4 @@
+
+T20916.hs:8:10: error:
+    • Different names for the same type variable: ‘p’ and ‘q’
+    • In the data type declaration for ‘T3’
diff --git a/testsuite/tests/saks/should_fail/all.T b/testsuite/tests/saks/should_fail/all.T
index 7e2194a21f..98345aa2ca 100644
--- a/testsuite/tests/saks/should_fail/all.T
+++ b/testsuite/tests/saks/should_fail/all.T
@@ -24,6 +24,7 @@ test('saks_fail022', normal, compile_fail, [''])
 test('saks_fail023', normal, compile_fail, [''])
 test('saks_fail024', normal, compile_fail, [''])
 test('saks_fail025', normal, compile_fail, [''])
+test('saks_fail026', normal, compile_fail, [''])
 test('T16722', normal, compile_fail, [''])
 test('T16727a', normal, compile_fail, [''])
 test('T16727b', normal, compile_fail, [''])
@@ -33,3 +34,4 @@ test('T16756b', normal, compile_fail, [''])
 test('T16758', normal, compile_fail, [''])
 test('T18863a', normal, compile_fail, [''])
 test('T18863b', normal, compile_fail, [''])
+test('T20916', normal, compile_fail, [''])
diff --git a/testsuite/tests/saks/should_fail/saks_fail009.hs b/testsuite/tests/saks/should_fail/saks_fail009.hs
index 317c0e7644..21394ada56 100644
--- a/testsuite/tests/saks/should_fail/saks_fail009.hs
+++ b/testsuite/tests/saks/should_fail/saks_fail009.hs
@@ -5,5 +5,5 @@ module SAKS_Fail009 where
 
 import Data.Kind (Type)
 
-type T :: forall k -> k -> Type
+type T :: forall j -> j -> Type
 data T (k :: Type -> Type) (a :: k)
diff --git a/testsuite/tests/saks/should_fail/saks_fail009.stderr b/testsuite/tests/saks/should_fail/saks_fail009.stderr
index 8ce43f6d5d..22b66b421b 100644
--- a/testsuite/tests/saks/should_fail/saks_fail009.stderr
+++ b/testsuite/tests/saks/should_fail/saks_fail009.stderr
@@ -1,4 +1,5 @@
 
 saks_fail009.hs:9:1: error:
-    • Expected kind ‘* -> *’, but ‘k’ has kind ‘*’
+    • Expecting one more argument to ‘k’
+      Expected a type, but ‘k’ has kind ‘* -> *’
     • In the data type declaration for ‘T’
diff --git a/testsuite/tests/saks/should_fail/saks_fail019.hs b/testsuite/tests/saks/should_fail/saks_fail019.hs
index 51cdd54ca2..ddd20d099c 100644
--- a/testsuite/tests/saks/should_fail/saks_fail019.hs
+++ b/testsuite/tests/saks/should_fail/saks_fail019.hs
@@ -6,6 +6,6 @@ module SAKS_Fail019 where
 import Data.Kind (Type)
 
 type T :: Type -> Type -> Type
-data T a :: a -> Type
+data T x :: x -> Type
   -- Should not panic with:
-  --   GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer
+  --   GHC internal error: ‘x’ is not in scope during type checking, but it passed the renamer
diff --git a/testsuite/tests/saks/should_fail/saks_fail019.stderr b/testsuite/tests/saks/should_fail/saks_fail019.stderr
index b34a7e1905..a824ab118c 100644
--- a/testsuite/tests/saks/should_fail/saks_fail019.stderr
+++ b/testsuite/tests/saks/should_fail/saks_fail019.stderr
@@ -1,9 +1,9 @@
 
 saks_fail019.hs:9:1: error:
-    • Couldn't match kind ‘a’ with ‘*’
-      Expected: a -> *
+    • Couldn't match kind ‘x’ with ‘*’
+      Expected: x -> *
         Actual: * -> *
-      ‘a’ is a rigid type variable bound by
+      ‘x’ is a rigid type variable bound by
         the data type declaration for ‘T’
         at saks_fail019.hs:9:8
     • In the data type declaration for ‘T’
diff --git a/testsuite/tests/saks/should_fail/saks_fail021.stderr b/testsuite/tests/saks/should_fail/saks_fail021.stderr
index 6128aff165..fa20ccc826 100644
--- a/testsuite/tests/saks/should_fail/saks_fail021.stderr
+++ b/testsuite/tests/saks/should_fail/saks_fail021.stderr
@@ -1,4 +1,4 @@
 
 saks_fail021.hs:10:1: error:
-    • Expected kind ‘k’, but ‘a’ has kind ‘*’
+    • Expected a type, but ‘a’ has kind ‘k’
     • In the class declaration for ‘C’
diff --git a/testsuite/tests/saks/should_fail/saks_fail022.stderr b/testsuite/tests/saks/should_fail/saks_fail022.stderr
index e0cc222344..0591eced95 100644
--- a/testsuite/tests/saks/should_fail/saks_fail022.stderr
+++ b/testsuite/tests/saks/should_fail/saks_fail022.stderr
@@ -1,4 +1,4 @@
 
 saks_fail022.hs:10:1: error:
-    • Expected kind ‘k’, but ‘a’ has kind ‘(x, y)’
+    • Expected kind ‘(x, y)’, but ‘a’ has kind ‘k’
     • In the class declaration for ‘C’
diff --git a/testsuite/tests/saks/should_fail/saks_fail023.stderr b/testsuite/tests/saks/should_fail/saks_fail023.stderr
index 3af24c7abb..36144f6d9d 100644
--- a/testsuite/tests/saks/should_fail/saks_fail023.stderr
+++ b/testsuite/tests/saks/should_fail/saks_fail023.stderr
@@ -1,4 +1,4 @@
 
 saks_fail023.hs:10:1: error:
-    • Expected kind ‘k’, but ‘a’ has kind ‘*’
+    • Expected a type, but ‘a’ has kind ‘k’
     • In the class declaration for ‘C’
diff --git a/testsuite/tests/saks/should_fail/saks_fail026.hs b/testsuite/tests/saks/should_fail/saks_fail026.hs
new file mode 100644
index 0000000000..1d47a06d6e
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/saks_fail026.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module SAKS_Fail026 where
+
+import Data.Kind (Type)
+
+type F3 :: forall kx. kx -> Type
+type family F3 (b :: Type) where
diff --git a/testsuite/tests/saks/should_fail/saks_fail026.stderr b/testsuite/tests/saks/should_fail/saks_fail026.stderr
new file mode 100644
index 0000000000..ceeeaa01c7
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/saks_fail026.stderr
@@ -0,0 +1,7 @@
+
+saks_fail026.hs:8:1: error:
+    • Expected kind ‘kx’, but ‘b’ has kind ‘*’
+      ‘kx’ is a rigid type variable bound by
+        the type family declaration for ‘F3’
+        at saks_fail026.hs:7:19-20
+    • In the type family declaration for ‘F3’
diff --git a/testsuite/tests/th/T10946.stderr b/testsuite/tests/th/T10946.stderr
new file mode 100644
index 0000000000..a5b6ebe16c
--- /dev/null
+++ b/testsuite/tests/th/T10946.stderr
@@ -0,0 +1,14 @@
+
+T10946.hs:8:13: error:
+    • Found hole: _ :: a
+      Where: ‘a’ is a rigid type variable bound by
+               the type signature for:
+                 m :: forall a. a -> a
+               at T10946.hs:7:1-11
+    • In the Template Haskell quotation [|| _ ||]
+      In the expression: [|| _ ||]
+      In the Template Haskell splice $$([|| _ ||])
+    • Relevant bindings include
+        x :: a (bound at T10946.hs:8:3)
+        m :: a -> a (bound at T10946.hs:8:1)
+      Valid hole fits include x :: a (bound at T10946.hs:8:3)
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 2f304ddc55..1e9ece046a 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -340,7 +340,7 @@ test('T10828a', normal, compile_fail, ['-v0'])
 test('T10828b', normal, compile_fail, ['-v0'])
 test('T10891', normal, compile, ['-v0'])
 test('T10945', normal, compile_fail, ['-v0'])
-test('T10946', expect_broken(10946), compile, ['-v0'])
+test('T10946', normal, compile_fail, ['-v0'])
 test('T10734', normal, compile_and_run, ['-v0'])
 test('T10819', [], multimod_compile,
      ['T10819.hs', '-v0 ' + config.ghc_th_way_flags])
diff --git a/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem.hs b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem.hs
new file mode 100644
index 0000000000..f8f1fbb130
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs, DataKinds, PolyKinds #-}
+
+module KcConDeclSkolem where
+
+import Data.Kind
+import Data.Proxy
+
+data G a where
+  D :: Proxy (a :: k) -> Proxy (b :: k) -> G (a b)
diff --git a/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem.stderr b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem.stderr
new file mode 100644
index 0000000000..ca5e590e72
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem.stderr
@@ -0,0 +1,6 @@
+
+KcConDeclSkolem.hs:9:15: error:
+    • Expected kind ‘k’, but ‘a’ has kind ‘k -> k0’
+    • In the first argument of ‘Proxy’, namely ‘(a :: k)’
+      In the type ‘Proxy (a :: k)’
+      In the definition of data constructor ‘D’
diff --git a/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem2.hs b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem2.hs
new file mode 100644
index 0000000000..cb0c7ddf79
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem2.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE GADTs, DataKinds, PolyKinds #-}
+
+module KcConDeclSkolem2 where
+
+import Data.Kind
+import Data.Proxy
+
+data D a = MkD (a a)
diff --git a/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem2.stderr b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem2.stderr
new file mode 100644
index 0000000000..b9d4d6d95f
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/KcConDeclSkolem2.stderr
@@ -0,0 +1,6 @@
+
+KcConDeclSkolem2.hs:8:19: error:
+    • Expected kind ‘k0’, but ‘a’ has kind ‘k0 -> *’
+    • In the first argument of ‘a’, namely ‘a’
+      In the type ‘(a a)’
+      In the definition of data constructor ‘MkD’
diff --git a/testsuite/tests/typecheck/no_skolem_info/T10946_sk.stderr b/testsuite/tests/typecheck/no_skolem_info/T10946_sk.stderr
new file mode 100644
index 0000000000..d9ddf33946
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T10946_sk.stderr
@@ -0,0 +1,14 @@
+
+T10946_sk.hs:6:13: error:
+    • Found hole: _ :: a
+      Where: ‘a’ is a rigid type variable bound by
+               the type signature for:
+                 m :: forall a. a -> a
+               at T10946_sk.hs:5:1-11
+    • In the Template Haskell quotation [|| _ ||]
+      In the expression: [|| _ ||]
+      In the Template Haskell splice $$([|| _ ||])
+    • Relevant bindings include
+        x :: a (bound at T10946_sk.hs:6:3)
+        m :: a -> a (bound at T10946_sk.hs:6:1)
+      Valid hole fits include x :: a (bound at T10946_sk.hs:6:3)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T13499.hs b/testsuite/tests/typecheck/no_skolem_info/T13499.hs
new file mode 100644
index 0000000000..50d02f6e95
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T13499.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE StaticPointers #-}
+
+import Data.Typeable (Typeable)
+import GHC.StaticPtr (StaticPtr)
+
+f :: Typeable a => StaticPtr (a -> a)
+f = static (\a -> _)
+
+main :: IO ()
+main = return ()
diff --git a/testsuite/tests/typecheck/no_skolem_info/T13499.stderr b/testsuite/tests/typecheck/no_skolem_info/T13499.stderr
new file mode 100644
index 0000000000..dbf5ba521b
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T13499.stderr
@@ -0,0 +1,14 @@
+
+T13499.hs:7:19: error:
+    • Found hole: _ :: a
+      Where: ‘a’ is a rigid type variable bound by
+               the type signature for:
+                 f :: forall a. Typeable a => StaticPtr (a -> a)
+               at T13499.hs:6:1-37
+    • In the body of a static form: (\ a -> _)
+      In the expression: static (\ a -> _)
+      In an equation for ‘f’: f = static (\ a -> _)
+    • Relevant bindings include
+        a :: a (bound at T13499.hs:7:14)
+        f :: StaticPtr (a -> a) (bound at T13499.hs:7:1)
+      Valid hole fits include a :: a (bound at T13499.hs:7:14)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040.hs b/testsuite/tests/typecheck/no_skolem_info/T14040.hs
new file mode 100644
index 0000000000..202c4600b2
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T14040.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14040 where
+
+import Data.Kind
+
+data family Sing (a :: k)
+
+data WeirdList :: Type -> Type where
+  WeirdNil  :: WeirdList a
+  WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
+
+data instance Sing (z :: WeirdList a) where
+  SWeirdNil  :: Sing WeirdNil
+  SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
+
+elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
+                        (p :: forall (x :: Type). x -> WeirdList x -> Type).
+                 Sing wl
+              -> (forall (y :: Type). p _ WeirdNil)
+              -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
+                    Sing x -> Sing xs -> p _ xs
+                  -> p _ (WeirdCons x xs))
+              -> p _ wl
+elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
+elimWeirdList (SWeirdCons (x :: Sing (x :: z))
+                          (xs :: Sing (xs :: WeirdList (WeirdList z))))
+              pWeirdNil pWeirdCons
+  = pWeirdCons @z @x @xs x xs
+      (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
new file mode 100644
index 0000000000..fb4cc3f897
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr
@@ -0,0 +1,60 @@
+
+T14040.hs:26:46: error:
+    • 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
+      an explicit forall (z :: Type) (x :: z)
+                         (xs :: WeirdList (WeirdList z))
+      at T14040.hs:25:26-77
+    • In the second argument of ‘p’, namely ‘xs’
+      In the type ‘Sing wl
+                   -> (forall (y :: Type). p _ WeirdNil)
+                      -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
+                          Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
+                         -> p _ wl’
+      In the type signature:
+        elimWeirdList :: forall (a :: Type)
+                                (wl :: WeirdList a)
+                                (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl
+                                                                                     -> (forall (y :: Type).
+                                                                                         p _ WeirdNil)
+                                                                                        -> (forall (z :: Type)
+                                                                                                   (x :: z)
+                                                                                                   (xs :: WeirdList (WeirdList z)).
+                                                                                            Sing x
+                                                                                            -> Sing xs
+                                                                                               -> p _ xs
+                                                                                                  -> p _ (WeirdCons x xs))
+                                                                                           -> p _ wl
+
+T14040.hs:27:27: error:
+    • 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
+      an explicit forall (z :: Type) (x :: z)
+                         (xs :: WeirdList (WeirdList z))
+      at T14040.hs:25:26-77
+    • In the second argument of ‘p’, namely ‘(WeirdCons x xs)’
+      In the type ‘Sing wl
+                   -> (forall (y :: Type). p _ WeirdNil)
+                      -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
+                          Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
+                         -> p _ wl’
+      In the type signature:
+        elimWeirdList :: forall (a :: Type)
+                                (wl :: WeirdList a)
+                                (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl
+                                                                                     -> (forall (y :: Type).
+                                                                                         p _ WeirdNil)
+                                                                                        -> (forall (z :: Type)
+                                                                                                   (x :: z)
+                                                                                                   (xs :: WeirdList (WeirdList z)).
+                                                                                            Sing x
+                                                                                            -> Sing xs
+                                                                                               -> p _ xs
+                                                                                                  -> p _ (WeirdCons x xs))
+                                                                                           -> p _ wl
diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040A.hs b/testsuite/tests/typecheck/no_skolem_info/T14040A.hs
new file mode 100644
index 0000000000..183a894398
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T14040A.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+newtype S (f :: k1 -> k2)
+  = MkS (forall t. Proxy t -> Proxy (f t))
+
+foo :: forall (a :: Type)
+              (f :: forall (x :: a). Proxy x -> Type).
+       S f -> ()
+foo (MkS (sF :: _)) = ()
diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040A.stderr b/testsuite/tests/typecheck/no_skolem_info/T14040A.stderr
new file mode 100644
index 0000000000..fca04623b0
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T14040A.stderr
@@ -0,0 +1,11 @@
+
+T14040A.hs:12:8: error:
+    • Cannot generalise type; skolem ‘a’ would escape its scope
+      if I tried to quantify (x0 :: a) in this type:
+        forall a (f :: forall (x :: a). Proxy @{a} x -> *).
+        S @(Proxy @{a} x0) @(*) (f @x0) -> ()
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature:
+        foo :: forall (a :: Type)
+                      (f :: forall (x :: a). Proxy x -> Type). S f -> ()
diff --git a/testsuite/tests/typecheck/no_skolem_info/T19482.stderr b/testsuite/tests/typecheck/no_skolem_info/T19482.stderr
new file mode 100644
index 0000000000..0c4b35f505
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T19482.stderr
@@ -0,0 +1,9 @@
+
+T19482.hs:11:25: error:
+    • Expected kind ‘[r]’, but ‘s’ has kind ‘r’
+      ‘r’ is a rigid type variable bound by
+        the instance declaration
+        at T19482.hs:10:10-35
+    • In the type ‘s’
+      In the expression: testF @r @s
+      In an equation for ‘bugList’: bugList = testF @r @s
diff --git a/testsuite/tests/typecheck/no_skolem_info/T19752.stderr b/testsuite/tests/typecheck/no_skolem_info/T19752.stderr
new file mode 100644
index 0000000000..9f0bc741da
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T19752.stderr
@@ -0,0 +1,22 @@
+
+T19752.hs:12:10: error:
+    • Could not deduce (F b0 ~ a)
+      from the context: F b ~ a
+        bound by the type signature for:
+                   f :: forall b. (F b ~ a) => a
+        at T19752.hs:12:10-23
+      Expected: forall b. (F b ~ a) => a
+        Actual: forall b. (F b ~ a) => a
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          g :: forall a. a
+        at T19752.hs:9:1-16
+    • In the ambiguity check for ‘f’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature: f :: (F b ~ a) => a
+      In an equation for ‘g’:
+          g = f
+            where
+                f :: (F b ~ a) => a
+                f = undefined
+    • Relevant bindings include g :: a (bound at T19752.hs:10:1)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T19760.stderr b/testsuite/tests/typecheck/no_skolem_info/T19760.stderr
new file mode 100644
index 0000000000..cb5f7e2d16
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T19760.stderr
@@ -0,0 +1,19 @@
+
+T19760.hs:11:41: error:
+    • Couldn't match kind ‘a'’ with ‘a’
+      Expected kind ‘Maybe a’, but ‘m'’ has kind ‘Maybe a'’
+      ‘a'’ is a rigid type variable bound by
+        the type signature for ‘go’
+        at T19760.hs:11:18-19
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a (p :: Maybe a -> *) (m :: Maybe a). p m
+        at T19760.hs:8:1-56
+    • In the first argument of ‘p’, namely ‘m'’
+      In the type signature: go :: forall a' (m' :: Maybe a'). p m'
+      In an equation for ‘f’:
+          f = go
+            where
+                go :: forall a' (m' :: Maybe a'). p m'
+                go = undefined
+    • Relevant bindings include f :: p m (bound at T19760.hs:9:1)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20063.stderr b/testsuite/tests/typecheck/no_skolem_info/T20063.stderr
new file mode 100644
index 0000000000..bb3b2c04b6
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20063.stderr
@@ -0,0 +1,27 @@
+
+T20063.hs:25:21: error:
+    • Could not deduce (ctx4 ~ (ctx0 :*& l0))
+      from the context: (ctx1 ~ 'Extend ctx7, ctx2 ~ 'Extend ctx8)
+        bound by a pattern with constructor:
+                   U :: forall {k} (ctx1 :: Context) (ctx2 :: Context) (l :: k).
+                        Rn ctx1 ctx2 -> Rn (ctx1 :*& l) (ctx2 :*& l),
+                 in an equation for ‘rnRename’
+        at T20063.hs:25:11-13
+      Expected: Idx ctx4
+        Actual: Idx (ctx0 :*& l0)
+      ‘ctx4’ is a rigid type variable bound by
+        the type signature for:
+          rnRename :: forall (ctx1 :: Context) (ctx2 :: Context)
+                             (ctx3 :: Context) (ctx4 :: Context).
+                      Rn ctx1 ctx2 -> Idx ctx3 -> Idx ctx4
+        at T20063.hs:24:1-48
+    • In the expression: T _
+      In an equation for ‘rnRename’: rnRename (U _) _ = T _
+    • Relevant bindings include
+        rnRename :: Rn ctx1 ctx2 -> Idx ctx3 -> Idx ctx4
+          (bound at T20063.hs:25:1)
+
+T20063.hs:26:17: error:
+    • The constructor ‘T’ should have 1 argument, but has been given none
+    • In the pattern: T
+      In an equation for ‘rnRename’: rnRename _ T = undefined
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20232.hs b/testsuite/tests/typecheck/no_skolem_info/T20232.hs
new file mode 100644
index 0000000000..b9268ebbfb
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20232.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE LinearTypes #-}
+module T20232 where
+
+data C a = forall p. C (a %p -> a)
+
+f :: C a -> a %1 -> a
+f b x = case b of C h -> h x
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20232.stderr b/testsuite/tests/typecheck/no_skolem_info/T20232.stderr
new file mode 100644
index 0000000000..047db6bd96
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20232.stderr
@@ -0,0 +1,9 @@
+
+T20232.hs:7:5: error:
+    • Couldn't match type ‘p’ with ‘'One’
+        arising from multiplicity of ‘x’
+      ‘p’ is a rigid type variable bound by
+        a pattern with constructor: C :: forall a. (a -> a) -> C a,
+        in a case alternative
+        at T20232.hs:7:19-21
+    • In an equation for ‘f’: f b x = case b of C h -> h x
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20680.hs b/testsuite/tests/typecheck/no_skolem_info/T20680.hs
new file mode 100644
index 0000000000..c7f5c6838a
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20680.hs
@@ -0,0 +1,26 @@
+{-# language
+    DerivingStrategies
+  , DerivingVia
+  , GeneralisedNewtypeDeriving
+  , StandaloneDeriving
+#-}
+
+module T20690 (main) where
+
+import GHC.Exts (TYPE)
+import GHC.Generics (Rec1)
+import Data.Kind (Type)
+
+main :: IO ()
+main = pure ()
+
+class FunctorL (f :: Type -> TYPE r) where
+  fmapL :: (a -> b) -> (f a -> f b)
+
+newtype Base1 f a = Base1 { getBase1 :: f a }
+  deriving newtype (Functor)
+
+instance Functor f => FunctorL (Base1 f) where
+  fmapL = fmap
+
+deriving via (Base1 (Rec1 f)) instance FunctorL (Rec1 f)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20680.stderr b/testsuite/tests/typecheck/no_skolem_info/T20680.stderr
new file mode 100644
index 0000000000..c6a2d42bd4
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20680.stderr
@@ -0,0 +1,9 @@
+
+T20680.hs:26:50: error:
+    • Couldn't match kind ‘k’ with ‘*’
+      Expected kind ‘* -> *’, but ‘Rec1 f’ has kind ‘k -> *’
+      ‘k’ is a rigid type variable bound by
+        the deriving clause for ‘Base1 (Rec1 f)’
+        at T20680.hs:26:14-29
+    • In the first argument of ‘FunctorL’, namely ‘(Rec1 f)’
+      In the stand-alone deriving instance for ‘FunctorL (Rec1 f)’
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20969.hs b/testsuite/tests/typecheck/no_skolem_info/T20969.hs
new file mode 100644
index 0000000000..0746187b80
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20969.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
+module T20969 where
+
+import Data.Sequence.Internal
+import qualified Language.Haskell.TH.Syntax as TH
+
+import T20969A
+
+glumber :: forall a. Num a => a -> Seq a
+glumber x = $$(sequenceCode (fromList [TH.liftTyped _ :: TH.Code TH.Q a, [||x||]]))
+
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20969.stderr b/testsuite/tests/typecheck/no_skolem_info/T20969.stderr
new file mode 100644
index 0000000000..2a5646b354
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20969.stderr
@@ -0,0 +1,23 @@
+
+T20969.hs:10:40: error:
+    • No instance for (TH.Lift a) arising from a use of ‘TH.liftTyped’
+    • In the expression: TH.liftTyped _ :: TH.Code TH.Q a
+      In the first argument of ‘fromList’, namely
+        ‘[TH.liftTyped _ :: TH.Code TH.Q a, [|| x ||]]’
+      In the first argument of ‘sequenceCode’, namely
+        ‘(fromList [TH.liftTyped _ :: TH.Code TH.Q a, [|| x ||]])’
+
+T20969.hs:10:53: error:
+    • Found hole: _ :: a
+      Where: ‘a’ is a rigid type variable bound by
+               the type signature for:
+                 glumber :: forall a. Num a => a -> Seq a
+               at T20969.hs:9:1-40
+    • In the first argument of ‘TH.liftTyped’, namely ‘_’
+      In the expression: TH.liftTyped _ :: TH.Code TH.Q a
+      In the first argument of ‘fromList’, namely
+        ‘[TH.liftTyped _ :: TH.Code TH.Q a, [|| x ||]]’
+    • Relevant bindings include
+        x :: a (bound at T20969.hs:10:9)
+        glumber :: a -> Seq a (bound at T20969.hs:10:1)
+      Valid hole fits include x :: a (bound at T20969.hs:10:9)
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20969A.hs b/testsuite/tests/typecheck/no_skolem_info/T20969A.hs
new file mode 100644
index 0000000000..bd660c41be
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T20969A.hs
@@ -0,0 +1,32 @@
+{-# language TemplateHaskellQuotes #-}
+module T20969A where
+import Data.Sequence.Internal
+import qualified Language.Haskell.TH.Syntax as TH
+
+class Functor t => SequenceCode t where
+  traverseCode :: TH.Quote m => (a -> TH.Code m b) -> t a -> TH.Code m (t b)
+  traverseCode f = sequenceCode . fmap f
+  sequenceCode :: TH.Quote m => t (TH.Code m a) -> TH.Code m (t a)
+  sequenceCode = traverseCode id
+
+instance SequenceCode Seq where
+  sequenceCode (Seq t) = [|| Seq $$(traverseCode sequenceCode t) ||]
+
+instance SequenceCode Elem where
+  sequenceCode (Elem t) = [|| Elem $$t ||]
+
+instance SequenceCode FingerTree where
+  sequenceCode (Deep s pr m sf) =
+    [|| Deep s $$(sequenceCode pr) $$(traverseCode sequenceCode m) $$(sequenceCode sf) ||]
+  sequenceCode (Single a) = [|| Single $$a ||]
+  sequenceCode EmptyT = [|| EmptyT ||]
+
+instance SequenceCode Digit where
+  sequenceCode (One a) = [|| One $$a ||]
+  sequenceCode (Two a b) = [|| Two $$a $$b ||]
+  sequenceCode (Three a b c) = [|| Three $$a $$b $$c ||]
+  sequenceCode (Four a b c d) = [|| Four $$a $$b $$c $$d ||]
+
+instance SequenceCode Node where
+  sequenceCode (Node2 s x y) = [|| Node2 s $$x $$y ||]
+  sequenceCode (Node3 s x y z) = [|| Node3 s $$x $$y $$z ||]
diff --git a/testsuite/tests/typecheck/no_skolem_info/all.T b/testsuite/tests/typecheck/no_skolem_info/all.T
index 80b4db6a1b..5c5defc90e 100644
--- a/testsuite/tests/typecheck/no_skolem_info/all.T
+++ b/testsuite/tests/typecheck/no_skolem_info/all.T
@@ -1,5 +1,13 @@
-test('T19752', [expect_broken(19752), grep_errmsg('of unknown origin')], compile_fail, [''])
-test('T20063', [expect_broken(20063), grep_errmsg('of unknown origin')], compile_fail, [''])
-test('T19760', [expect_broken(19760), grep_errmsg('of unknown origin')], compile_fail, [''])
-test('T19482', [expect_broken(19482), grep_errmsg('of unknown origin')], compile_fail, [''])
-test('T10946_sk', [expect_broken(10946), grep_errmsg('of unknown origin')], compile_fail, [''])
+test('T19752', normal, compile_fail, [''])
+test('T20063', normal, compile_fail, [''])
+test('T19760', normal, compile_fail, [''])
+test('T19482', normal, compile_fail, [''])
+test('T10946_sk', normal, compile_fail, [''])
+test('T20680', normal, compile_fail, [''])
+test('KcConDeclSkolem', normal, compile_fail, [''])
+test('KcConDeclSkolem2', normal, compile_fail, [''])
+test('T20232', normal, compile_fail, [''])
+test('T20969', normal, multimod_compile_fail, ['T20969', '-v0'])
+test('T14040A', normal, compile_fail, [''])
+test('T14040', normal, compile_fail, [''])
+test('T13499', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T20732.hs b/testsuite/tests/typecheck/should_compile/T20732.hs
new file mode 100644
index 0000000000..8f4d126607
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20732.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE PolyKinds, GADTs #-}
+
+module T20732 where
+
+data T (a :: k1) k2 (x :: k2) = MkT (S a k2 x)
+data S (b :: k3) k4 (y :: k4) = MkS (T b k4 y)
diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr
index 2c410de0f2..6ad8956ecc 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9834.stderr
@@ -33,7 +33,9 @@ T9834.hs:23:23: warning: [-Wdeferred-type-errors (in -Wdefault)]
       ‘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)
+                  (forall (q1 :: * -> *).
+                   Applicative q1 =>
+                   Comp p q1 a -> Comp p q1 a)
                   -> p a
         at T9834.hs:22:11-74
     • In the first argument of ‘wrapIdComp’, namely ‘f’
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b77d78e882..ef13910c41 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -809,3 +809,4 @@ test('T20873b', [extra_files(['T20873b_aux.hs'])], multimod_compile, ['T20873b',
 test('StaticPtrTypeFamily', normal, compile, [''])
 test('T20946', normal, compile, [''])
 test('T20996', normal, compile, [''])
+test('T20732', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T14904a.stderr b/testsuite/tests/typecheck/should_fail/T14904a.stderr
index 0de9206867..089e7bedeb 100644
--- a/testsuite/tests/typecheck/should_fail/T14904a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14904a.stderr
@@ -1,9 +1,9 @@
 
 T14904a.hs:10:6: error:
-    • Expected kind ‘forall (a :: k). g a’, but ‘f’ has kind ‘k1’
-      Cannot equate type variable ‘k1’
-      with a kind involving polytypes: forall (a :: k). g a
-      ‘k1’ is a rigid type variable bound by
+    • Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k’
+      Cannot equate type variable ‘k’
+      with a kind involving polytypes: forall (a :: k1). g a
+      ‘k’ is a rigid type variable bound by
         a family instance declaration
         at T14904a.hs:10:3-30
     • In the first argument of ‘F’, namely ‘(f :: forall a. g a)’
diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr
index c1d751bee2..aabc868844 100644
--- a/testsuite/tests/typecheck/should_fail/T15629.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15629.stderr
@@ -6,21 +6,21 @@ T15629.hs:26:31: error:
                                                            (F x ab) (F x z)
                                                          -> *’
       ‘z’ is a rigid type variable bound by
-        an explicit forall z ab
+        the type signature for ‘g’
         at T15629.hs:26:17
       ‘ab’ is a rigid type variable bound by
-        an explicit forall z ab
+        the type signature for ‘g’
         at T15629.hs:26:19-20
     • In the first argument of ‘Proxy’, namely
         ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’
       In the type signature:
-        g :: forall z ab.
-             Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+        g :: forall z ab. Proxy ((Comp (F1Sym :: x
+                                                 ~> F x z) F2Sym) :: F x ab ~> F x ab)
       In an equation for ‘f’:
           f _
             = ()
             where
                 g ::
-                  forall z ab.
-                  Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+                  forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab
+                                                                            ~> F x ab)
                 g = sg Proxy Proxy
diff --git a/testsuite/tests/typecheck/should_fail/T15799.stderr b/testsuite/tests/typecheck/should_fail/T15799.stderr
index 161cfe026a..af44e0a8ed 100644
--- a/testsuite/tests/typecheck/should_fail/T15799.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15799.stderr
@@ -1,9 +1,5 @@
 
 T15799.hs:46:62: error:
-    Expected a constraint, but ‘UnOp b <= a’ has kind ‘*’
-
-T15799.hs:46:67: error:
     • Couldn't match kind ‘TypeLits.Natural’ with ‘Op Nat’
-      Expected kind ‘Op (Op Nat)’, but ‘b’ has kind ‘Op Nat’
-    • In the first argument of ‘UnOp’, namely ‘b’
-      In the first argument of ‘(<=)’, namely ‘UnOp b’
+      Expected kind ‘Op Nat’, but ‘UnOp b’ has kind ‘Nat’
+    • In the first argument of ‘(<=)’, namely ‘UnOp b’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
index df7865f8d4..86f65024af 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
@@ -3,7 +3,7 @@ UnliftedNewtypesUnassociatedFamilyFail.hs:21:30: error:
     • Couldn't match kind ‘t’ with ‘'IntRep’
       Expected a type, but ‘Int#’ has kind ‘TYPE 'IntRep’
       ‘t’ is a rigid type variable bound by
-        the data constructor ‘MkDF1a’
+        a family instance declaration
         at UnliftedNewtypesUnassociatedFamilyFail.hs:21:1-33
     • In the type ‘Int#’
       In the definition of data constructor ‘MkDF1a’
@@ -13,7 +13,7 @@ UnliftedNewtypesUnassociatedFamilyFail.hs:22:30: error:
     • Couldn't match kind ‘t’ with ‘'WordRep’
       Expected a type, but ‘Word#’ has kind ‘TYPE 'WordRep’
       ‘t’ is a rigid type variable bound by
-        the data constructor ‘MkDF2a’
+        a family instance declaration
         at UnliftedNewtypesUnassociatedFamilyFail.hs:22:1-34
     • In the type ‘Word#’
       In the definition of data constructor ‘MkDF2a’
@@ -25,7 +25,7 @@ UnliftedNewtypesUnassociatedFamilyFail.hs:23:30: error:
         but ‘(# Int#, Word# #)’ has kind ‘TYPE
                                             ('TupleRep '[ 'IntRep, 'WordRep])’
       ‘t’ is a rigid type variable bound by
-        the data constructor ‘MkDF3a’
+        a family instance declaration
         at UnliftedNewtypesUnassociatedFamilyFail.hs:23:1-46
     • In the type ‘(# Int#, Word# #)’
       In the definition of data constructor ‘MkDF3a’