Replace HsImplicitBndrs with HsOuterTyVarBndrswip/T16762

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, 23 insertions, 6 deletions

diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 5416e29692..debbbe1341 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -492,7 +492,7 @@ tcInstTypeBndrs id
 
 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type signature with skolem constants.
--- We could give them fresh names, but no need to do so
+-- This freshens the names, but no need to do so
 tcSkolDFunType dfun
   = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
        ; return (map snd tv_prs, theta, tau) }
@@ -524,13 +524,18 @@ tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
 
 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
+-- This version freshens the names and creates "super skolems";
+-- see comments around superSkolemTv.
 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
 
 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
+-- This version freshens the names and creates "super skolems";
+-- see comments around superSkolemTv.
 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
 
-tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
+tcInstSkolTyVarsPushLevel :: Bool  -- True <=> make "super skolem"
+                          -> TCvSubst -> [TyVar]
                           -> TcM (TCvSubst, [TcTyVar])
 -- Skolemise one level deeper, hence pushTcLevel
 -- See Note [Skolemising type variables]
@@ -599,10 +604,22 @@ a) Level allocation. We generally skolemise /before/ calling
 b) The [TyVar] should be ordered (kind vars first)
    See Note [Kind substitution when instantiating]
 
-c) It's a complete freshening operation: the skolems have a fresh
-   unique, and a location from the monad
-
-d) The resulting skolems are
+c) Clone the variable to give a fresh unique.  This is essential.
+   Consider (tc160)
+       type Foo x = forall a. a -> x
+   And typecheck the expression
+       (e :: Foo (Foo ())
+   We will skolemise the signature, but after expanding synonyms it
+   looks like
+        forall a. a -> forall a. a -> x
+   We don't want to make two big-lambdas with the same unique!
+
+d) We retain locations. Because the location of the variable is the correct
+   location to report in errors (e.g. in the signature). We don't want the
+   location to change to the body of the function, which does *not* explicitly
+   bind the variable.
+
+e) The resulting skolems are
         non-overlappable for tcInstSkolTyVars,
    but overlappable for tcInstSuperSkolTyVars
    See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example