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>

30 files changed, 419 insertions, 25 deletions

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’