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>

13 files changed, 17 insertions, 17 deletions

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)’