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>

1 files changed, 26 insertions, 16 deletions

diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index be667ec3a6..8e2d02e9b3 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -5,8 +5,8 @@ T14040a.hs:26:46: error:
         but ‘xs’ has kind ‘WeirdList (WeirdList z)’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
-        ‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
-         Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
+        an explicit forall (z :: Type) (x :: z)
+                           (xs :: WeirdList (WeirdList z))
         at T14040a.hs:(25,19)-(27,41)
     • In the second argument of ‘p’, namely ‘xs’
       In the type ‘Sing wl
@@ -17,12 +17,17 @@ T14040a.hs:26:46: error:
       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
+                                (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
 
 T14040a.hs:27:27: error:
     • Couldn't match kind ‘k0’ with ‘z’
@@ -30,8 +35,8 @@ T14040a.hs:27:27: error:
         but ‘WeirdCons x xs’ has kind ‘WeirdList z’
         because kind variable ‘z’ would escape its scope
       This (rigid, skolem) kind variable is bound by
-        ‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
-         Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
+        an explicit forall (z :: Type) (x :: z)
+                           (xs :: WeirdList (WeirdList z))
         at T14040a.hs:(25,19)-(27,41)
     • In the second argument of ‘p’, namely ‘(WeirdCons x xs)’
       In the type ‘Sing wl
@@ -42,9 +47,14 @@ T14040a.hs:27:27: error:
       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
+                                (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