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>

4 files changed, 37 insertions, 15 deletions

diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index 7755d3370d..b989ade11a 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -733,8 +733,8 @@ tcAddDataFamConPlaceholders inst_decls thing_inside
       = concatMap (get_fi_cons . unLoc) fids
 
     get_fi_cons :: DataFamInstDecl GhcRn -> [Name]
-    get_fi_cons (DataFamInstDecl { dfid_eqn = HsIB { hsib_body =
-                  FamEqn { feqn_rhs = HsDataDefn { dd_cons = cons } }}})
+    get_fi_cons (DataFamInstDecl { dfid_eqn =
+                  FamEqn { feqn_rhs = HsDataDefn { dd_cons = cons } }})
       = map unLoc $ concatMap (getConNames . unLoc) cons
 
 
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
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index e42fe42799..0ff826bb96 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -1845,8 +1845,8 @@ It's distressingly delicate though:
   the visible type application fails in the monad (throws an exception).
   We must not discard the out-of-scope error.
 
-  Also GHC.Tc.Solver.emitFlatConstraints may fail having emitted some
-  constraints with skolem-escape problems.
+  Also GHC.Tc.Solver.simplifyAndEmitFlatConstraints may fail having
+  emitted some constraints with skolem-escape problems.
 
 * If we discard too /few/ constraints, we may get the misleading
   class constraints mentioned above.  But we may /also/ end up taking
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index c1202f02d7..b8e946ac11 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -927,13 +927,18 @@ checkTvConstraints skol_info skol_tvs thing_inside
 emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
                          -> TcLevel -> WantedConstraints -> TcM ()
 emitResidualTvConstraint skol_info skol_tvs tclvl wanted
-  | isEmptyWC wanted
-  = return ()
-
-  | otherwise
-  = do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
+  | not (isEmptyWC wanted) ||
+    checkTelescopeSkol skol_info
+  = -- checkTelescopeSkol: in this case, /always/ emit this implication
+    -- even if 'wanted' is empty. We need the implication so that we check
+    -- for a bad telescope. See Note [Skolem escape and forall-types] in
+    -- GHC.Tc.Gen.HsType
+    do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
        ; emitImplication implic }
 
+  | otherwise  -- Empty 'wanted', emit nothing
+  = return ()
+
 buildTvImplication :: SkolemInfo -> [TcTyVar]
                    -> TcLevel -> WantedConstraints -> TcM Implication
 buildTvImplication skol_info skol_tvs tclvl wanted