Replace HsImplicitBndrs with HsOuterTyVarBndrs

This refactors the GHC AST to remove `HsImplicitBndrs` and replace it with
`HsOuterTyVarBndrs`, a type which records whether the outermost quantification
in a type is explicit (i.e., with an outermost, invisible `forall`) or
implicit. As a result of this refactoring, it is now evident in the AST where
the `forall`-or-nothing rule applies: it's all the places that use
`HsOuterTyVarBndrs`. See the revamped `Note [forall-or-nothing rule]` in
`GHC.Hs.Type` (previously in `GHC.Rename.HsType`).

Moreover, the places where `ScopedTypeVariables` brings lexically scoped type
variables into scope are a subset of the places that adhere to the
`forall`-or-nothing rule, so this also makes places that interact with
`ScopedTypeVariables` easier to find. See the revamped
`Note [Lexically scoped type variables]` in `GHC.Hs.Type` (previously in
`GHC.Tc.Gen.Sig`).

`HsOuterTyVarBndrs` are used in type signatures (see `HsOuterSigTyVarBndrs`)
and type family equations (see `HsOuterFamEqnTyVarBndrs`). The main difference
between the former and the latter is that the former cares about specificity
but the latter does not.

There are a number of knock-on consequences:

* There is now a dedicated `HsSigType` type, which is the combination of
  `HsOuterSigTyVarBndrs` and `HsType`. `LHsSigType` is now an alias for an
  `XRec` of `HsSigType`.
* Working out the details led us to a substantial refactoring of
  the handling of explicit (user-written) and implicit type-variable
  bindings in `GHC.Tc.Gen.HsType`.

  Instead of a confusing family of higher order functions, we now
  have a local data type, `SkolemInfo`, that controls how these
  binders are kind-checked.

  It remains very fiddly, not fully satisfying. But it's better
  than it was.

Fixes #16762. Bumps the Haddock submodule.

Co-authored-by: Simon Peyton Jones <simonpj@microsoft.com>
Co-authored-by: Richard Eisenberg <rae@richarde.dev>
Co-authored-by: Zubin Duggal <zubin@cmi.ac.in>

16 files changed, 82 insertions, 13 deletions

diff --git a/testsuite/tests/polykinds/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr
index 780bbdc63f..f96278a5e7 100644
--- a/testsuite/tests/polykinds/T11142.stderr
+++ b/testsuite/tests/polykinds/T11142.stderr
@@ -3,7 +3,7 @@ T11142.hs:9:49: error:
     • Expected kind ‘k’, but ‘b’ has kind ‘k0’
         because kind variable ‘k’ would escape its scope
       This (rigid, skolem) kind variable is bound by
-        ‘forall k (a :: k). SameKind a b’
+        an explicit forall k (a :: k)
         at T11142.hs:9:19-49
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature:
diff --git a/testsuite/tests/polykinds/T11516.stderr b/testsuite/tests/polykinds/T11516.stderr
index 5f8083309c..0bee63f2b3 100644
--- a/testsuite/tests/polykinds/T11516.stderr
+++ b/testsuite/tests/polykinds/T11516.stderr
@@ -1,5 +1,5 @@
 
 T11516.hs:12:16: error:
-    • Expected kind ‘i0 -> i0 -> *’, but ‘()’ has kind ‘*’
+    • Expected kind ‘i -> i -> *’, but ‘()’ has kind ‘*’
     • In the first argument of ‘Varpi’, namely ‘()’
       In the instance declaration for ‘Varpi (->) (->) (Either f)’
diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr
index 156f8490e8..90a5826266 100644
--- a/testsuite/tests/polykinds/T11520.stderr
+++ b/testsuite/tests/polykinds/T11520.stderr
@@ -1,9 +1,9 @@
 
 T11520.hs:15:77: error:
-    • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’
-      ‘k’ is a rigid type variable bound by
-        the instance declaration
-        at T11520.hs:(15,1)-(16,23)
+    • Expected kind ‘k2 -> k1’, but ‘g’ has kind ‘k4’
+      ‘k4’ is a rigid type variable bound by
+        an instance declaration
+        at T11520.hs:15:10-78
     • In the second argument of ‘Compose’, namely ‘g’
       In the first argument of ‘Typeable’, namely ‘(Compose f g)’
       In the instance declaration for ‘Typeable (Compose f g)’
diff --git a/testsuite/tests/polykinds/T15787.stderr b/testsuite/tests/polykinds/T15787.stderr
index 7241e2f7fb..b22e6c7b5b 100644
--- a/testsuite/tests/polykinds/T15787.stderr
+++ b/testsuite/tests/polykinds/T15787.stderr
@@ -1,7 +1,7 @@
 
 T15787.hs:15:14: error:
-    • Expected a type, but ‘k’ has kind ‘ob’
-      ‘ob’ is a rigid type variable bound by
+    • Expected a type, but ‘k’ has kind ‘ob1’
+      ‘ob1’ is a rigid type variable bound by
         the data constructor ‘Kl’
         at T15787.hs:15:3-43
     • In the type ‘k’
diff --git a/testsuite/tests/polykinds/T16221a.stderr b/testsuite/tests/polykinds/T16221a.stderr
index 7b550b6c8f..5aa099b0f1 100644
--- a/testsuite/tests/polykinds/T16221a.stderr
+++ b/testsuite/tests/polykinds/T16221a.stderr
@@ -2,7 +2,7 @@
 T16221a.hs:6:49: error:
     • Expected kind ‘k’, but ‘b’ has kind ‘k1’
       ‘k1’ is a rigid type variable bound by
-        the data constructor ‘MkT2’
+        an explicit forall k (b :: k)
         at T16221a.hs:6:20
       ‘k’ is a rigid type variable bound by
         the data constructor ‘MkT2’
diff --git a/testsuite/tests/polykinds/T16762.hs b/testsuite/tests/polykinds/T16762.hs
new file mode 100644
index 0000000000..720f8f5725
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs, DataKinds, PolyKinds, ExplicitForAll #-}
+
+module BadTelescope2 where
+
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+-- This declaration made GHC 8.10 produce a Core Lint error
+data T a b where
+  MkT :: forall a kx (b :: kx). SameKind a b -> T a b
diff --git a/testsuite/tests/polykinds/T16762.stderr b/testsuite/tests/polykinds/T16762.stderr
new file mode 100644
index 0000000000..6335fa4c50
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762.stderr
@@ -0,0 +1,7 @@
+
+T16762.hs:11:3: error:
+    • These kind and type variables: a kx (b :: kx)
+      are out of dependency order. Perhaps try this ordering:
+        kx (a :: kx) (b :: kx)
+    • In the definition of data constructor ‘MkT’
+      In the data declaration for ‘T’
diff --git a/testsuite/tests/polykinds/T16762a.hs b/testsuite/tests/polykinds/T16762a.hs
new file mode 100644
index 0000000000..4f56c8b3e9
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, GADTs, DataKinds, PolyKinds, ExplicitForAll #-}
+
+module T16762a where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+
+type family F a
+
+-- This should jolly well be rejected!
+type instance forall a k (b::k). F (SameKind a b) = Int
diff --git a/testsuite/tests/polykinds/T16762a.stderr b/testsuite/tests/polykinds/T16762a.stderr
new file mode 100644
index 0000000000..0a96f77d82
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762a.stderr
@@ -0,0 +1,6 @@
+
+T16762a.hs:12:22: error:
+    • These kind and type variables: a k (b :: k)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k)
+    • In the type instance declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T16762b.hs b/testsuite/tests/polykinds/T16762b.hs
new file mode 100644
index 0000000000..cad6bff33f
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762b.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+module T16762b where
+
+import Data.Kind
+
+type T :: forall k. Type
+data T
diff --git a/testsuite/tests/polykinds/T16762b.stderr b/testsuite/tests/polykinds/T16762b.stderr
new file mode 100644
index 0000000000..ffb29b70dc
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762b.stderr
@@ -0,0 +1,4 @@
+
+T16762b.hs:7:11: error:
+    Illegal kind: forall k. Type
+    Did you mean to enable PolyKinds?
diff --git a/testsuite/tests/polykinds/T16762c.hs b/testsuite/tests/polykinds/T16762c.hs
new file mode 100644
index 0000000000..c74c30ee47
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762c.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies, GADTs, DataKinds, PolyKinds, ExplicitForAll #-}
+
+module Foo where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+
+-- Bad telescope
+data T = forall a k (b::k). MkT (SameKind a b)
diff --git a/testsuite/tests/polykinds/T16762c.stderr b/testsuite/tests/polykinds/T16762c.stderr
new file mode 100644
index 0000000000..5be6fbb462
--- /dev/null
+++ b/testsuite/tests/polykinds/T16762c.stderr
@@ -0,0 +1,7 @@
+
+T16762c.hs:10:10: error:
+    • These kind and type variables: a k (b :: k)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k)
+    • In the definition of data constructor ‘MkT’
+      In the data declaration for ‘T’
diff --git a/testsuite/tests/polykinds/T7278.stderr b/testsuite/tests/polykinds/T7278.stderr
index 5f4ff6d18f..93b0e9aa3d 100644
--- a/testsuite/tests/polykinds/T7278.stderr
+++ b/testsuite/tests/polykinds/T7278.stderr
@@ -1,7 +1,7 @@
 
 T7278.hs:9:43: error:
-    • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’
-      ‘k’ is a rigid type variable bound by
+    • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k1’
+      ‘k1’ is a rigid type variable bound by
         the type signature for ‘f’
         at T7278.hs:9:1-49
     • In the type signature:
diff --git a/testsuite/tests/polykinds/TyVarTvKinds3.stderr b/testsuite/tests/polykinds/TyVarTvKinds3.stderr
index b0b7924444..872fe96684 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
-        the data constructor ‘MkBad’
+        an explicit forall k1 k2 (a :: k1) (b :: k2)
         at TyVarTvKinds3.hs:9:22-23
       ‘k1’ is a rigid type variable bound by
-        the data constructor ‘MkBad’
+        an explicit forall k1 k2 (a :: k1) (b :: k2)
         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/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 009172537b..a509dfd665 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -216,6 +216,10 @@ test('T16245', normal, compile_fail, [''])
 test('T16245a', normal, compile_fail, [''])
 test('T16342', normal, compile, [''])
 test('T16263', normal, compile_fail, [''])
+test('T16762', normal, compile_fail, [''])
+test('T16762a', normal, compile_fail, [''])
+test('T16762b', normal, compile_fail, [''])
+test('T16762c', normal, compile_fail, [''])
 test('T16902', normal, compile_fail, [''])
 test('CuskFam', normal, compile, [''])
 test('T17841', normal, compile_fail, [''])