Use HsForAllTelescope to avoid inferred, visible foralls

Currently, `HsForAllTy` permits the combination of `ForallVis` and
`Inferred`, but you can't actually typecheck code that uses it
(e.g., `forall {a} ->`). This patch refactors `HsForAllTy` to use a
new `HsForAllTelescope` data type that makes a type-level distinction
between visible and invisible `forall`s such that visible `forall`s
do not track `Specificity`. That part of the patch is actually quite
small; the rest is simply changing consumers of `HsType` to
accommodate this new type.

Fixes #18235. Bumps the `haddock` submodule.

7 files changed, 94 insertions, 80 deletions

diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index 850e0722da..a4d2be7ac6 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -722,8 +722,7 @@ tcStandaloneDerivInstType ctxt
                   HsIB { hsib_ext = vars
                        , hsib_body
                            = L (getLoc deriv_ty_body) $
-                             HsForAllTy { hst_fvf = ForallInvis
-                                        , hst_bndrs = tvs
+                             HsForAllTy { hst_tele = mkHsForAllInvisTele tvs
                                         , hst_xforall = noExtField
                                         , hst_body  = rho }}
        let (tvs, _theta, cls, inst_tys) = tcSplitDFunTy dfun_ty
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index e6cad5f4f0..b99cc6365b 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -896,11 +896,10 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
   = tc_fun_type mode ty1 ty2 exp_kind
 
 --------- Foralls
-tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
-                                   , hst_body = ty }) exp_kind
-  = do { (tclvl, wanted, (inv_tv_bndrs, ty'))
-            <- pushLevelAndCaptureConstraints         $
-               bindExplicitTKBndrs_Skol_M mode hs_tvs $
+tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
+  = do { (tclvl, wanted, (tv_bndrs, ty'))
+            <- pushLevelAndCaptureConstraints      $
+               bindExplicitTKTele_Skol_M mode tele $
                  -- The _M variant passes on the mode from the type, to
                  -- any wildards in kind signatures on the forall'd variables
                  -- e.g.      f :: _ -> Int -> forall (a :: _). blah
@@ -909,31 +908,27 @@ tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
 
        -- Do not kind-generalise here!  See Note [Kind generalisation]
 
-       ; let skol_info = ForAllSkol (ppr forall) (sep (map ppr hs_tvs))
-             skol_tvs  = binderVars inv_tv_bndrs
+       ; let skol_info = ForAllSkol (ppr forall) $ sep $ case tele of
+                           HsForAllVis { hsf_vis_bndrs = hs_tvs } ->
+                             map ppr hs_tvs
+                           HsForAllInvis { hsf_invis_bndrs = hs_tvs } ->
+                             map ppr hs_tvs
+             tv_bndrs' = construct_bndrs tv_bndrs
+             skol_tvs  = binderVars tv_bndrs'
        ; implic <- buildTvImplication skol_info skol_tvs tclvl wanted
        ; emitImplication implic
              -- /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]
 
-       ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs
-       ; return (mkForAllTys tv_bndrs ty') }
+       ; return (mkForAllTys tv_bndrs' ty') }
   where
-    construct_bndr :: TcInvisTVBinder -> TcM TcTyVarBinder
-    construct_bndr (Bndr tv spec) = do { argf <- spec_to_argf spec
-                                       ; return $ mkTyVarBinder argf tv }
-
-    -- See Note [Variable Specificity and Forall Visibility]
-    spec_to_argf :: Specificity -> TcM ArgFlag
-    spec_to_argf SpecifiedSpec = case fvf of
-      ForallVis   -> return Required
-      ForallInvis -> return Specified
-    spec_to_argf InferredSpec  = case fvf of
-      ForallVis   -> do { addErrTc (hang (text "Unexpected inferred variable in visible forall binder:")
-                                         2 (ppr forall))
-                        ; return Required }
-      ForallInvis -> return Inferred
+    construct_bndrs :: Either [TcReqTVBinder] [TcInvisTVBinder]
+                    -> [TcTyVarBinder]
+    construct_bndrs (Left req_tv_bndrs) =
+      map (mkTyVarBinder Required . binderVar) req_tv_bndrs
+    construct_bndrs (Right inv_tv_bndrs) =
+      map tyVarSpecToBinder inv_tv_bndrs
 
 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
   | null (unLoc ctxt)
@@ -1068,21 +1063,21 @@ tc_hs_type mode ty@(HsWildCardTy _)        ek = tcAnonWildCardOcc mode ty ek
 {-
 Note [Variable Specificity and Forall Visibility]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A HsForAllTy contains a ForAllVisFlag to denote the visibility of the forall
-binder. Furthermore, each bound variable also has a Specificity. Together these
-determine the variable binders (ArgFlag) for each variable in the generated
-ForAllTy type.
+A HsForAllTy contains an HsForAllTelescope to denote the visibility of the forall
+binder. Furthermore, each invisible type variable binder also has a
+Specificity. Together, these determine the variable binders (ArgFlag) for each
+variable in the generated ForAllTy type.
 
 This table summarises this relation:
---------------------------------------------------------------------------
-| User-written type         ForAllVisFlag     Specificity        ArgFlag
-|-------------------------------------------------------------------------
-| f :: forall a. type       ForallInvis       SpecifiedSpec      Specified
-| f :: forall {a}. type     ForallInvis       InferredSpec       Inferred
-| f :: forall a -> type     ForallVis         SpecifiedSpec      Required
-| f :: forall {a} -> type   ForallVis         InferredSpec       /
+----------------------------------------------------------------------------
+| User-written type         HsForAllTelescope   Specificity        ArgFlag
+|---------------------------------------------------------------------------
+| f :: forall a. type       HsForAllInvis       SpecifiedSpec      Specified
+| f :: forall {a}. type     HsForAllInvis       InferredSpec       Inferred
+| f :: forall a -> type     HsForAllVis         SpecifiedSpec      Required
+| f :: forall {a} -> type   HsForAllVis         InferredSpec       /
 |   This last form is non-sensical and is thus rejected.
---------------------------------------------------------------------------
+----------------------------------------------------------------------------
 
 For more information regarding the interpretation of the resulting ArgFlag, see
 Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep".
@@ -2863,6 +2858,21 @@ cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar
 -- Explicit binders
 --------------------------------------
 
+-- | Skolemise the 'HsTyVarBndr's in an 'LHsForAllTelescope.
+-- Returns 'Left' for visible @forall@s and 'Right' for invisible @forall@s.
+bindExplicitTKTele_Skol_M
+    :: TcTyMode
+    -> HsForAllTelescope GhcRn
+    -> TcM a
+    -> TcM (Either [TcReqTVBinder] [TcInvisTVBinder], a)
+bindExplicitTKTele_Skol_M mode tele thing_inside = case tele of
+  HsForAllVis { hsf_vis_bndrs = bndrs } -> do
+    (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside
+    pure (Left req_tv_bndrs, thing)
+  HsForAllInvis { hsf_invis_bndrs = bndrs } -> do
+    (inv_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside
+    pure (Right inv_tv_bndrs, thing)
+
 bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
     :: (OutputableBndrFlag flag)
     => [LHsTyVarBndr flag GhcRn]
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 2ac2823fb5..df0c7d37f6 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -279,8 +279,8 @@ no_anon_wc lty = go lty
       HsRecTy _ flds                 -> gos $ map (cd_fld_type . unLoc) flds
       HsExplicitListTy _ _ tys       -> gos tys
       HsExplicitTupleTy _ tys        -> gos tys
-      HsForAllTy { hst_bndrs = bndrs
-                 , hst_body = ty } -> no_anon_wc_bndrs bndrs
+      HsForAllTy { hst_tele = tele
+                 , hst_body = ty } -> no_anon_wc_tele tele
                                         && go ty
       HsQualTy { hst_ctxt = L _ ctxt
                , hst_body = ty }  -> gos ctxt && go ty
@@ -293,8 +293,10 @@ no_anon_wc lty = go lty
 
     gos = all go
 
-no_anon_wc_bndrs :: [LHsTyVarBndr flag GhcRn] -> Bool
-no_anon_wc_bndrs ltvs = all (go . unLoc) ltvs
+no_anon_wc_tele :: HsForAllTelescope GhcRn -> Bool
+no_anon_wc_tele tele = case tele of
+  HsForAllVis   { hsf_vis_bndrs   = ltvs } -> all (go . unLoc) ltvs
+  HsForAllInvis { hsf_invis_bndrs = ltvs } -> all (go . unLoc) ltvs
   where
     go (UserTyVar _ _ _)      = True
     go (KindedTyVar _ _ _ ki) = no_anon_wc ki
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 3a4d0de24f..140299997a 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -2123,19 +2123,19 @@ reifyType ty@(CoercionTy {})= noTH (sLit "coercions in types") (ppr ty)
 
 reify_for_all :: TyCoRep.ArgFlag -> TyCoRep.Type -> TcM TH.Type
 -- Arg of reify_for_all is always ForAllTy or a predicate FunTy
-reify_for_all argf ty = do
-  tvbndrs' <- reifyTyVarBndrs tvbndrs
-  case argToForallVisFlag argf of
-    ForallVis   -> do phi' <- reifyType phi
-                      let tvs = map (() <$) tvbndrs'
-                      -- see Note [Specificity in HsForAllTy] in GHC.Hs.Type
-                      pure $ TH.ForallVisT tvs phi'
-    ForallInvis -> do let (cxt, tau) = tcSplitPhiTy phi
-                      cxt' <- reifyCxt cxt
-                      tau' <- reifyType tau
-                      pure $ TH.ForallT tvbndrs' cxt' tau'
-  where
-    (tvbndrs, phi) = tcSplitForAllTysSameVis argf ty
+reify_for_all argf ty
+  | isVisibleArgFlag argf
+  = do let (req_bndrs, phi) = tcSplitForAllTysReq ty
+       tvbndrs' <- reifyTyVarBndrs req_bndrs
+       phi' <- reifyType phi
+       pure $ TH.ForallVisT tvbndrs' phi'
+  | otherwise
+  = do let (inv_bndrs, phi) = tcSplitForAllTysInvis ty
+       tvbndrs' <- reifyTyVarBndrs inv_bndrs
+       let (cxt, tau) = tcSplitPhiTy phi
+       cxt' <- reifyCxt cxt
+       tau' <- reifyType tau
+       pure $ TH.ForallT tvbndrs' cxt' tau'
 
 reifyTyLit :: TyCoRep.TyLit -> TcM TH.TyLit
 reifyTyLit (NumTyLit n) = return (TH.NumTyLit n)
@@ -2177,10 +2177,6 @@ instance ReifyFlag Specificity TH.Specificity where
     reifyFlag SpecifiedSpec = TH.SpecifiedSpec
     reifyFlag InferredSpec  = TH.InferredSpec
 
-instance ReifyFlag ArgFlag TH.Specificity where
-    reifyFlag Required      = TH.SpecifiedSpec
-    reifyFlag (Invisible s) = reifyFlag s
-
 reifyTyVars :: [TyVar] -> TcM [TH.TyVarBndr ()]
 reifyTyVars = reifyTyVarBndrs . map mk_bndr
   where
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 0471b85666..f6e5b87f53 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2443,8 +2443,8 @@ getGhciStepIO = do
         ioM     = nlHsAppTy (nlHsTyVar ioTyConName) (nlHsTyVar a_tv)
 
         step_ty = noLoc $ HsForAllTy
-                     { hst_fvf = ForallInvis
-                     , hst_bndrs = [noLoc $ UserTyVar noExtField SpecifiedSpec (noLoc a_tv)]
+                     { hst_tele = mkHsForAllInvisTele
+                                  [noLoc $ UserTyVar noExtField SpecifiedSpec (noLoc a_tv)]
                      , hst_xforall = noExtField
                      , hst_body  = nlHsFunTy ghciM ioM }
 
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 6326152797..cc8ac8f737 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -543,14 +543,8 @@ tcInstTypeBndrs :: ([VarBndr TyVar Specificity] -> TcM (TCvSubst, [VarBndr TcTyV
                 -> TcM ([(Name, VarBndr TcTyVar Specificity)], TcThetaType, TcType) -- ^ Result
                      -- (type vars, preds (incl equalities), rho)
 tcInstTypeBndrs inst_tyvars id =
-  let (tyvars, rho) = splitForAllVarBndrs (idType id)
-      tyvars'       = map argf_to_spec tyvars
-  in tc_inst_internal inst_tyvars tyvars' rho
-  where
-    argf_to_spec :: VarBndr TyCoVar ArgFlag -> VarBndr TyCoVar Specificity
-    argf_to_spec (Bndr tv Required)      = Bndr tv SpecifiedSpec
-    -- see Note [Specificity in HsForAllTy] in GHC.Hs.Type
-    argf_to_spec (Bndr tv (Invisible s)) = Bndr tv s
+  let (tyvars, rho) = splitForAllTysInvis (idType id)
+  in tc_inst_internal inst_tyvars tyvars rho
 
 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type signature with skolem constants.
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index f92861f1d0..9cc1d79df9 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -21,8 +21,8 @@ module GHC.Tc.Utils.TcType (
   -- Types
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
   TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
-  TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcTyCon,
-  KnotTied,
+  TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder,
+  TcTyCon, KnotTied,
 
   ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
 
@@ -57,7 +57,8 @@ module GHC.Tc.Utils.TcType (
   -- These are important because they do not look through newtypes
   getTyVar,
   tcSplitForAllTy_maybe,
-  tcSplitForAllTys, tcSplitForAllTysSameVis,
+  tcSplitForAllTys, tcSplitSomeForAllTys,
+  tcSplitForAllTysReq, tcSplitForAllTysInvis,
   tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs,
   tcSplitPhiTy, tcSplitPredFunTy_maybe,
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
@@ -128,7 +129,7 @@ module GHC.Tc.Utils.TcType (
   --------------------------------
   -- Reexported from Type
   Type, PredType, ThetaType, TyCoBinder,
-  ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
+  ArgFlag(..), AnonArgFlag(..),
 
   mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
   mkSpecForAllTys, mkTyCoInvForAllTy,
@@ -340,6 +341,7 @@ type TcTyCoVar = Var    -- Either a TcTyVar or a CoVar
 
 type TcTyVarBinder     = TyVarBinder
 type TcInvisTVBinder   = InvisTVBinder
+type TcReqTVBinder     = ReqTVBinder
 type TcTyCon           = TyCon   -- these can be the TcTyCon constructor
 
 -- These types do not have boxy type variables in them
@@ -1212,14 +1214,25 @@ tcSplitForAllTys ty
   = ASSERT( all isTyVar (fst sty) ) sty
   where sty = splitForAllTys ty
 
--- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if
--- @'sameVis' argf supplied_argf@ is 'True', where @argf@ is the visibility
--- of the @ForAllTy@'s binder and @supplied_argf@ is the visibility provided
--- as an argument to this function.
--- All split tyvars are annotated with their argf.
-tcSplitForAllTysSameVis :: ArgFlag -> Type -> ([TyVarBinder], Type)
-tcSplitForAllTysSameVis supplied_argf ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty
-  where sty = splitForAllTysSameVis supplied_argf ty
+-- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@
+-- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
+-- @argf_pred@ is a predicate over visibilities provided as an argument to this
+-- function. All split tyvars are annotated with their @argf@.
+tcSplitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type)
+tcSplitSomeForAllTys argf_pred ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty
+  where sty = splitSomeForAllTys argf_pred ty
+
+-- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Required' type
+-- variable binders. All split tyvars are annotated with '()'.
+tcSplitForAllTysReq :: Type -> ([TcReqTVBinder], Type)
+tcSplitForAllTysReq ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty
+  where sty = splitForAllTysReq ty
+
+-- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Invisible' type
+-- variable binders. All split tyvars are annotated with their 'Specificity'.
+tcSplitForAllTysInvis :: Type -> ([TcInvisTVBinder], Type)
+tcSplitForAllTysInvis ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty
+  where sty = splitForAllTysInvis ty
 
 -- | Like 'tcSplitForAllTys', but splits off only named binders.
 tcSplitForAllVarBndrs :: Type -> ([TyVarBinder], Type)