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.

23 files changed, 355 insertions, 293 deletions

diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 188e2a9b3b..684854045e 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -34,7 +34,7 @@ module GHC.Core.TyCo.Rep (
         KindOrType, Kind,
         KnotTied,
         PredType, ThetaType,      -- Synonyms
-        ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
+        ArgFlag(..), AnonArgFlag(..),
 
         -- * Coercions
         Coercion(..),
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 57e570cd79..a183308526 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -15,7 +15,7 @@ module GHC.Core.Type (
         -- $type_classification
 
         -- $representation_types
-        TyThing(..), Type, ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
+        TyThing(..), Type, ArgFlag(..), AnonArgFlag(..),
         Specificity(..),
         KindOrType, PredType, ThetaType,
         Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder,
@@ -44,7 +44,8 @@ module GHC.Core.Type (
         mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInfForAllTy, mkInfForAllTys,
-        splitForAllTys, splitForAllTysSameVis,
+        splitForAllTys, splitSomeForAllTys,
+        splitForAllTysReq, splitForAllTysInvis,
         splitForAllVarBndrs,
         splitForAllTy_maybe, splitForAllTy,
         splitForAllTy_ty_maybe, splitForAllTy_co_maybe,
@@ -271,7 +272,7 @@ import GHC.Data.List.SetOps
 import GHC.Types.Unique ( nonDetCmpUnique )
 
 import GHC.Data.Maybe   ( orElse )
-import Data.Maybe       ( isJust )
+import Data.Maybe       ( isJust, mapMaybe )
 import Control.Monad    ( guard )
 
 -- $type_classification
@@ -1576,19 +1577,47 @@ splitForAllTys ty = split ty ty []
     split _       (ForAllTy (Bndr tv _) ty)    tvs = split ty ty (tv:tvs)
     split orig_ty _                            tvs = (reverse tvs, orig_ty)
 
--- | Like 'splitForAllTys', 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.
--- Furthermore, each returned tyvar is annotated with its argf.
-splitForAllTysSameVis :: ArgFlag -> Type -> ([TyCoVarBinder], Type)
-splitForAllTysSameVis supplied_argf ty = split ty ty []
+-- | Like 'splitForAllTys', 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. Furthermore, each returned tyvar is annotated with its @argf@.
+splitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type)
+splitSomeForAllTys argf_pred ty = split ty ty []
   where
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
-    split _       (ForAllTy (Bndr tv argf) ty) tvs
-      | argf `sameVis` supplied_argf               = split ty ty ((Bndr tv argf):tvs)
+    split _       (ForAllTy tvb@(Bndr _ argf) ty) tvs
+      | argf_pred argf                             = split ty ty (tvb:tvs)
     split orig_ty _                            tvs = (reverse tvs, orig_ty)
 
+-- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Required' type
+-- variable binders. Furthermore, each returned tyvar is annotated with '()'.
+splitForAllTysReq :: Type -> ([ReqTVBinder], Type)
+splitForAllTysReq ty =
+  let (all_bndrs, body) = splitSomeForAllTys isVisibleArgFlag ty
+      req_bndrs         = mapMaybe mk_req_bndr_maybe all_bndrs in
+  ASSERT( req_bndrs `equalLength` all_bndrs )
+  (req_bndrs, body)
+  where
+    mk_req_bndr_maybe :: TyCoVarBinder -> Maybe ReqTVBinder
+    mk_req_bndr_maybe (Bndr tv argf) = case argf of
+      Required    -> Just $ Bndr tv ()
+      Invisible _ -> Nothing
+
+-- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Invisible' type
+-- variable binders. Furthermore, each returned tyvar is annotated with its
+-- 'Specificity'.
+splitForAllTysInvis :: Type -> ([InvisTVBinder], Type)
+splitForAllTysInvis ty =
+  let (all_bndrs, body) = splitSomeForAllTys isInvisibleArgFlag ty
+      inv_bndrs         = mapMaybe mk_inv_bndr_maybe all_bndrs in
+  ASSERT( inv_bndrs `equalLength` all_bndrs )
+  (inv_bndrs, body)
+  where
+    mk_inv_bndr_maybe :: TyCoVarBinder -> Maybe InvisTVBinder
+    mk_inv_bndr_maybe (Bndr tv argf) = case argf of
+      Invisible s -> Just $ Bndr tv s
+      Required    -> Nothing
+
 -- | Like splitForAllTys, but split only for tyvars.
 -- This always succeeds, even if it returns only an empty list. Note that the
 -- result type returned may have free variables that were bound by a forall.
diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index f800d934b6..fe5eaa84e7 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/compiler/GHC/Hs/Decls.hs
@@ -1639,7 +1639,9 @@ pprConDecl (ConDeclH98 { con_name = L _ con
                        , con_mb_cxt = mcxt
                        , con_args = args
                        , con_doc = doc })
-  = sep [ppr_mbDoc doc, pprHsForAll ForallInvis ex_tvs cxt, ppr_details args]
+  = sep [ ppr_mbDoc doc
+        , pprHsForAll (mkHsForAllInvisTele ex_tvs) cxt
+        , ppr_details args ]
   where
     ppr_details (InfixCon t1 t2) = hsep [ppr t1, pprInfixOcc con, ppr t2]
     ppr_details (PrefixCon tys)  = hsep (pprPrefixOcc con
@@ -1652,7 +1654,7 @@ pprConDecl (ConDeclGADT { con_names = cons, con_qvars = qvars
                         , con_mb_cxt = mcxt, con_args = args
                         , con_res_ty = res_ty, con_doc = doc })
   = ppr_mbDoc doc <+> ppr_con_names cons <+> dcolon
-    <+> (sep [pprHsForAll ForallInvis qvars cxt,
+    <+> (sep [pprHsForAll (mkHsForAllInvisTele qvars) cxt,
               ppr_arrow_chain (get_args args ++ [ppr res_ty]) ])
   where
     get_args (PrefixCon args) = map ppr args
@@ -1938,7 +1940,7 @@ pprHsFamInstLHS :: (OutputableBndrId p)
    -> LHsContext (GhcPass p)
    -> SDoc
 pprHsFamInstLHS thing bndrs typats fixity mb_ctxt
-   = hsep [ pprHsExplicitForAll ForallInvis bndrs
+   = hsep [ pprHsExplicitForAll bndrs
           , pprLHsContext mb_ctxt
           , pp_pats typats ]
    where
diff --git a/compiler/GHC/Hs/Extension.hs b/compiler/GHC/Hs/Extension.hs
index 02106ab060..a667f92892 100644
--- a/compiler/GHC/Hs/Extension.hs
+++ b/compiler/GHC/Hs/Extension.hs
@@ -716,6 +716,12 @@ type family XXType           x
 
 -- ---------------------------------------------------------------------
 
+type family XHsForAllVis        x
+type family XHsForAllInvis      x
+type family XXHsForAllTelescope x
+
+-- ---------------------------------------------------------------------
+
 type family XUserTyVar   x
 type family XKindedTyVar x
 type family XXTyVarBndr  x
diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs
index 99d627965d..e49406d484 100644
--- a/compiler/GHC/Hs/Instances.hs
+++ b/compiler/GHC/Hs/Instances.hs
@@ -400,6 +400,11 @@ deriving instance Data (HsPatSigType GhcPs)
 deriving instance Data (HsPatSigType GhcRn)
 deriving instance Data (HsPatSigType GhcTc)
 
+-- deriving instance (DataIdLR p p) => Data (HsForAllTelescope p)
+deriving instance Data (HsForAllTelescope GhcPs)
+deriving instance Data (HsForAllTelescope GhcRn)
+deriving instance Data (HsForAllTelescope GhcTc)
+
 -- deriving instance (DataIdLR p p) => Data (HsTyVarBndr p)
 deriving instance (Data flag) => Data (HsTyVarBndr flag GhcPs)
 deriving instance (Data flag) => Data (HsTyVarBndr flag GhcRn)
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index 9d08a370c9..d09de98950 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -9,6 +9,7 @@ GHC.Hs.Type: Abstract syntax: user-defined types
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
@@ -19,7 +20,7 @@ GHC.Hs.Type: Abstract syntax: user-defined types
 
 module GHC.Hs.Type (
         HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind,
-        HsTyVarBndr(..), LHsTyVarBndr, ForallVisFlag(..),
+        HsForAllTelescope(..), HsTyVarBndr(..), LHsTyVarBndr,
         LHsQTyVars(..),
         HsImplicitBndrs(..),
         HsWildCardBndrs(..),
@@ -51,6 +52,7 @@ module GHC.Hs.Type (
 
         mkHsImplicitBndrs, mkHsWildCardBndrs, mkHsPatSigType, hsImplicitBody,
         mkEmptyImplicitBndrs, mkEmptyWildCardBndrs,
+        mkHsForAllVisTele, mkHsForAllInvisTele,
         mkHsQTvs, hsQTvExplicit, emptyLHsQTvs,
         isHsKindedTyVar, hsTvbAllKinded, isLHsForAllTy,
         hsScopedTvs, hsWcScopedTvs, dropWildCards,
@@ -163,7 +165,7 @@ is a bit complicated.  Here's how it works.
   These constructors represent what the user wrote, no more
   and no less.
 
-* The ForallVisFlag field of HsForAllTy represents whether a forall is
+* The ForAllTelescope field of HsForAllTy represents whether a forall is
   invisible (e.g., forall a b. {...}, with a dot) or visible
   (e.g., forall a b -> {...}, with an arrow).
 
@@ -329,6 +331,28 @@ type LHsKind pass = Located (HsKind pass)
 --             LHsQTyVars
 --  The explicitly-quantified binders in a data/type declaration
 
+-- | The type variable binders in an 'HsForAllTy'.
+-- See also @Note [Variable Specificity and Forall Visibility]@ in
+-- "GHC.Tc.Gen.HsType".
+data HsForAllTelescope pass
+  = HsForAllVis -- ^ A visible @forall@ (e.g., @forall a -> {...}@).
+                --   These do not have any notion of specificity, so we use
+                --   '()' as a placeholder value.
+    { hsf_xvis      :: XHsForAllVis pass
+    , hsf_vis_bndrs :: [LHsTyVarBndr () pass]
+    }
+  | HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c -> {...}@),
+                  --   where each binder has a 'Specificity'.
+    { hsf_xinvis       :: XHsForAllInvis pass
+    , hsf_invis_bndrs  :: [LHsTyVarBndr Specificity pass]
+    }
+  | XHsForAllTelescope !(XXHsForAllTelescope pass)
+
+type instance XHsForAllVis   (GhcPass _) = NoExtField
+type instance XHsForAllInvis (GhcPass _) = NoExtField
+
+type instance XXHsForAllTelescope (GhcPass _) = NoExtCon
+
 -- | Located Haskell Type Variable Binder
 type LHsTyVarBndr flag pass = Located (HsTyVarBndr flag pass)
                          -- See Note [HsType binders]
@@ -352,6 +376,16 @@ type instance XHsQTvs GhcTc = HsQTvsRn
 
 type instance XXLHsQTyVars  (GhcPass _) = NoExtCon
 
+mkHsForAllVisTele ::
+  [LHsTyVarBndr () (GhcPass p)] -> HsForAllTelescope (GhcPass p)
+mkHsForAllVisTele vis_bndrs =
+  HsForAllVis { hsf_xvis = noExtField, hsf_vis_bndrs = vis_bndrs }
+
+mkHsForAllInvisTele ::
+  [LHsTyVarBndr Specificity (GhcPass p)] -> HsForAllTelescope (GhcPass p)
+mkHsForAllInvisTele invis_bndrs =
+  HsForAllInvis { hsf_xinvis = noExtField, hsf_invis_bndrs = invis_bndrs }
+
 mkHsQTvs :: [LHsTyVarBndr () GhcPs] -> LHsQTyVars GhcPs
 mkHsQTvs tvs = HsQTvs { hsq_ext = noExtField, hsq_explicit = tvs }
 
@@ -475,7 +509,7 @@ E.g. For a signature like
    f :: forall (a::k). blah
 we get
    HsIB { hsib_vars = [k]
-        , hsib_body = HsForAllTy { hst_bndrs = [(a::*)]
+        , hsib_body = HsForAllTy { hst_tele = HsForAllInvis [(a::*)]
                                  , hst_body = blah }
 The implicit kind variable 'k' is bound by the HsIB;
 the explicitly forall'd tyvar 'a' is bound by the HsForAllTy
@@ -643,30 +677,12 @@ instance NamedThing (HsTyVarBndr flag GhcRn) where
   getName (UserTyVar _ _ v) = unLoc v
   getName (KindedTyVar _ _ v _) = unLoc v
 
-{- Note [Specificity in HsForAllTy]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-All type variables in a `HsForAllTy` type are annotated with their
-`Specificity`. The meaning of this `Specificity` depends on the visibility of
-the binder `hst_fvf`:
-
-* In an invisible forall type, the `Specificity` denotes whether type variables
-  are `Specified` (`forall a. ...`) or `Inferred` (`forall {a}. ...`). For more
-  information, see Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
-  in GHC.Core.TyCo.Rep.
-
-* In a visible forall type, the `Specificity` has no particular meaning. We
-  uphold the convention that all visible forall types use `Specified` binders.
--}
-
 -- | Haskell Type
 data HsType pass
   = HsForAllTy   -- See Note [HsType binders]
       { hst_xforall :: XForAllTy pass
-      , hst_fvf     :: ForallVisFlag -- Is this `forall a -> {...}` or
-                                     --         `forall a. {...}`?
-      , hst_bndrs   :: [LHsTyVarBndr Specificity pass]
+      , hst_tele    :: HsForAllTelescope pass
                                      -- Explicit, user-supplied 'forall a {b} c'
-                                     -- see Note [Specificity in HsForAllTy]
       , hst_body    :: LHsType pass  -- body type
       }
       -- ^ - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnForall',
@@ -1076,8 +1092,8 @@ hsWcScopedTvs sig_ty
   , HsIB { hsib_ext = vars
          , hsib_body = sig_ty2 } <- sig_ty1
   = case sig_ty2 of
-      L _ (HsForAllTy { hst_fvf = ForallInvis -- See Note [hsScopedTvs vis_flag]
-                      , hst_bndrs = tvs }) ->
+      L _ (HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }}) ->
+                                   -- See Note [hsScopedTvs vis_flag]
         vars ++ nwcs ++ hsLTyVarNames tvs
       _                                    -> nwcs
 
@@ -1086,8 +1102,8 @@ hsScopedTvs :: LHsSigType GhcRn -> [Name]
 hsScopedTvs sig_ty
   | HsIB { hsib_ext = vars
          , hsib_body = sig_ty2 } <- sig_ty
-  , L _ (HsForAllTy { hst_fvf = ForallInvis -- See Note [hsScopedTvs vis_flag]
-                    , hst_bndrs = tvs }) <- sig_ty2
+  , L _ (HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }})
+      <- sig_ty2                 -- See Note [hsScopedTvs vis_flag]
   = vars ++ hsLTyVarNames tvs
   | otherwise
   = []
@@ -1134,9 +1150,10 @@ The conclusion of these discussions can be summarized as follows:
   >     vfn :: forall x y -> tau(x,y)
   >     vfn x y = \a b -> ...         -- bad!
 
-We cement this design by pattern-matching on ForallInvis in hsScopedTvs:
+We cement this design by pattern-matching on HsForAllInvis in hsScopedTvs:
 
-    hsScopedTvs (HsForAllTy { hst_fvf = ForallInvis, ... }) = ...
+    hsScopedTvs (HsForAllTy { hst_tele = HsForAllInvis { hst_bndrs = ... }
+                            , ... }) = ...
 
 At the moment, GHC does not support visible 'forall' in terms. Nevertheless,
 it is still possible to write erroneous programs that use visible 'forall's in
@@ -1145,12 +1162,12 @@ terms, such as this example:
     x :: forall a -> a -> a
     x = x
 
-If we do not pattern-match on ForallInvis in hsScopedTvs, then `a` would
+If we do not pattern-match on HsForAllInvis in hsScopedTvs, then `a` would
 erroneously be brought into scope over the body of `x` when renaming it.
 Although the typechecker would later reject this (see `GHC.Tc.Validity.vdqAllowed`),
 it is still possible for this to wreak havoc in the renamer before it gets to
 that point (see #17687 for an example of this).
-Bottom line: nip problems in the bud by matching on ForallInvis from the start.
+Bottom line: nip problems in the bud by matching on HsForAllInvis from the start.
 -}
 
 ---------------------
@@ -1380,7 +1397,8 @@ splitLHsGADTPrefixTy ty
   where
     -- NB: We do not use splitLHsForAllTyInvis below, since that looks through
     -- parentheses...
-    split_forall (L _ (HsForAllTy { hst_fvf = ForallInvis, hst_bndrs = bndrs
+    split_forall (L _ (HsForAllTy { hst_tele =
+                                      HsForAllInvis { hsf_invis_bndrs = bndrs }
                                   , hst_body = rho }))
       = (Just bndrs, rho)
     split_forall sigma
@@ -1410,8 +1428,8 @@ splitLHsForAllTyInvis :: LHsType pass -> ([LHsTyVarBndr Specificity pass], LHsTy
 splitLHsForAllTyInvis lty@(L _ ty) =
   case ty of
     HsParTy _ ty' -> splitLHsForAllTyInvis ty'
-    HsForAllTy { hst_fvf = fvf', hst_bndrs = tvs', hst_body = body' }
-      |  fvf' == ForallInvis
+    HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs' }
+               , hst_body = body' }
       -> (tvs', body')
     _ -> ([], lty)
 
@@ -1577,6 +1595,13 @@ instance OutputableBndrId p
        => Outputable (LHsQTyVars (GhcPass p)) where
     ppr (HsQTvs { hsq_explicit = tvs }) = interppSP tvs
 
+instance OutputableBndrId p
+       => Outputable (HsForAllTelescope (GhcPass p)) where
+    ppr (HsForAllVis { hsf_vis_bndrs = bndrs }) =
+      text "HsForAllVis:" <+> ppr bndrs
+    ppr (HsForAllInvis { hsf_invis_bndrs = bndrs }) =
+      text "HsForAllInvis:" <+> ppr bndrs
+
 instance (OutputableBndrId p, OutputableBndrFlag flag)
        => Outputable (HsTyVarBndr flag (GhcPass p)) where
     ppr = pprTyVarBndr
@@ -1598,8 +1623,8 @@ pprAnonWildCard = char '_'
 
 -- | Prints a forall; When passed an empty list, prints @forall .@/@forall ->@
 -- only when @-dppr-debug@ is enabled.
-pprHsForAll :: (OutputableBndrId p, OutputableBndrFlag flag)
-            => ForallVisFlag -> [LHsTyVarBndr flag (GhcPass p)]
+pprHsForAll :: OutputableBndrId p
+            => HsForAllTelescope (GhcPass p)
             -> LHsContext (GhcPass p) -> SDoc
 pprHsForAll = pprHsForAllExtra Nothing
 
@@ -1610,32 +1635,30 @@ pprHsForAll = pprHsForAllExtra Nothing
 -- function for this is needed, as the extra-constraints wildcard is removed
 -- from the actual context and type, and stored in a separate field, thus just
 -- printing the type will not print the extra-constraints wildcard.
-pprHsForAllExtra :: (OutputableBndrId p, OutputableBndrFlag flag)
-                 => Maybe SrcSpan -> ForallVisFlag
-                 -> [LHsTyVarBndr flag (GhcPass p)]
+pprHsForAllExtra :: forall p. OutputableBndrId p
+                 => Maybe SrcSpan
+                 -> HsForAllTelescope (GhcPass p)
                  -> LHsContext (GhcPass p) -> SDoc
-pprHsForAllExtra extra fvf qtvs cxt
-  = pp_forall <+> pprLHsContextExtra (isJust extra) cxt
+pprHsForAllExtra extra tele cxt
+  = pp_tele tele <+> pprLHsContextExtra (isJust extra) cxt
   where
-    pp_forall | null qtvs = whenPprDebug (forAllLit <> separator)
-              | otherwise = forAllLit <+> interppSP qtvs <> separator
+    pp_tele :: HsForAllTelescope (GhcPass p) -> SDoc
+    pp_tele tele = case tele of
+      HsForAllVis   { hsf_vis_bndrs   = qtvs } -> pp_forall (space <> arrow) qtvs
+      HsForAllInvis { hsf_invis_bndrs = qtvs } -> pp_forall dot qtvs
 
-    separator = ppr_forall_separator fvf
+    pp_forall :: forall flag. OutputableBndrFlag flag =>
+                 SDoc -> [LHsTyVarBndr flag (GhcPass p)] -> SDoc
+    pp_forall separator qtvs
+      | null qtvs = whenPprDebug (forAllLit <> separator)
+      | otherwise = forAllLit <+> interppSP qtvs <> separator
 
 -- | Version of 'pprHsForAll' or 'pprHsForAllExtra' that will always print
 -- @forall.@ when passed @Just []@. Prints nothing if passed 'Nothing'
 pprHsExplicitForAll :: (OutputableBndrId p)
-                    => ForallVisFlag
-                    -> Maybe [LHsTyVarBndr () (GhcPass p)] -> SDoc
-pprHsExplicitForAll fvf (Just qtvs) = forAllLit <+> interppSP qtvs
-                                                 <> ppr_forall_separator fvf
-pprHsExplicitForAll _   Nothing     = empty
-
--- | Prints an arrow for visible @forall@s (e.g., @forall a ->@) and a dot for
--- invisible @forall@s (e.g., @forall a.@).
-ppr_forall_separator :: ForallVisFlag -> SDoc
-ppr_forall_separator ForallVis   = space <> arrow
-ppr_forall_separator ForallInvis = dot
+                    => Maybe [LHsTyVarBndr () (GhcPass p)] -> SDoc
+pprHsExplicitForAll (Just qtvs) = forAllLit <+> interppSP qtvs <> dot
+pprHsExplicitForAll Nothing     = empty
 
 pprLHsContext :: (OutputableBndrId p)
               => LHsContext (GhcPass p) -> SDoc
@@ -1695,8 +1718,8 @@ ppr_mono_lty :: (OutputableBndrId p) => LHsType (GhcPass p) -> SDoc
 ppr_mono_lty ty = ppr_mono_ty (unLoc ty)
 
 ppr_mono_ty :: (OutputableBndrId p) => HsType (GhcPass p) -> SDoc
-ppr_mono_ty (HsForAllTy { hst_fvf = fvf, hst_bndrs = tvs, hst_body = ty })
-  = sep [pprHsForAll fvf tvs noLHsContext, ppr_mono_lty ty]
+ppr_mono_ty (HsForAllTy { hst_tele = tele, hst_body = ty })
+  = sep [pprHsForAll tele noLHsContext, ppr_mono_lty ty]
 
 ppr_mono_ty (HsQualTy { hst_ctxt = ctxt, hst_body = ty })
   = sep [pprLHsContextAlways ctxt, ppr_mono_lty ty]
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index 387536c2f2..7ca2d0025b 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -694,11 +694,17 @@ typeToLHsType ty
                                       , hst_body = go tau })
 
     go ty@(ForAllTy (Bndr _ argf) _)
-      | (tvs, tau) <- tcSplitForAllTysSameVis argf ty
-      = noLoc (HsForAllTy { hst_fvf = argToForallVisFlag argf
-                          , hst_bndrs = map go_tv tvs
+      = noLoc (HsForAllTy { hst_tele = tele
                           , hst_xforall = noExtField
                           , hst_body = go tau })
+      where
+        (tele, tau)
+          | isVisibleArgFlag argf
+          = let (req_tvbs, tau') = tcSplitForAllTysReq ty in
+            (mkHsForAllVisTele (map go_tv req_tvbs), tau')
+          | otherwise
+          = let (inv_tvbs, tau') = tcSplitForAllTysInvis ty in
+            (mkHsForAllInvisTele (map go_tv inv_tvbs), tau')
     go (TyVarTy tv)         = nlHsTyVar (getRdrName tv)
     go (LitTy (NumTyLit n))
       = noLoc $ HsTyLit noExtField (HsNumTy NoSourceText n)
@@ -723,7 +729,7 @@ typeToLHsType ty
         args :: [Type]
         (head, args) = splitAppTys ty
     go (CastTy ty _)        = go ty
-    go (CoercionTy co)      = pprPanic "toLHsSigWcType" (ppr co)
+    go (CoercionTy co)      = pprPanic "typeToLHsType" (ppr co)
 
          -- Source-language types have _invisible_ kind arguments,
          -- so we must remove them here (#8563)
@@ -743,14 +749,9 @@ typeToLHsType ty
                  Required  -> f `nlHsAppTy`     arg')
              head (zip args arg_flags)
 
-    argf_to_spec :: ArgFlag -> Specificity
-    argf_to_spec Required      = SpecifiedSpec
-    -- see Note [Specificity in HsForAllTy] in GHC.Hs.Type
-    argf_to_spec (Invisible s) = s
-
-    go_tv :: TyVarBinder -> LHsTyVarBndr Specificity GhcPs
-    go_tv (Bndr tv argf) = noLoc $ KindedTyVar noExtField
-                                               (argf_to_spec argf)
+    go_tv :: VarBndr TyVar flag -> LHsTyVarBndr flag GhcPs
+    go_tv (Bndr tv flag) = noLoc $ KindedTyVar noExtField
+                                               flag
                                                (noLoc (getRdrName tv))
                                                (go (tyVarKind tv))
 
diff --git a/compiler/GHC/HsToCore/Docs.hs b/compiler/GHC/HsToCore/Docs.hs
index 0f6d8ba9e4..d37c2dccaf 100644
--- a/compiler/GHC/HsToCore/Docs.hs
+++ b/compiler/GHC/HsToCore/Docs.hs
@@ -196,7 +196,7 @@ subordinates instMap decl = case decl of
         extract_deriv_ty (L l ty) =
           case ty of
             -- deriving (forall a. C a {- ^ Doc comment -})
-            HsForAllTy{ hst_fvf = ForallInvis
+            HsForAllTy{ hst_tele = HsForAllInvis{}
                       , hst_body = L _ (HsDocTy _ _ doc) }
                             -> Just (l, doc)
             -- deriving (C a {- ^ Doc comment -})
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index e84a4cbb27..b1d569e5e0 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -1265,7 +1265,7 @@ repLTy ty = repTy (unLoc ty)
 -- Desugar a type headed by an invisible forall (e.g., @forall a. a@) or
 -- a context (e.g., @Show a => a@) into a ForallT from L.H.TH.Syntax.
 -- In other words, the argument to this function is always an
--- @HsForAllTy ForallInvis@ or @HsQualTy@.
+-- @HsForAllTy HsForAllInvis{}@ or @HsQualTy@.
 -- Types headed by visible foralls (which are desugared to ForallVisT) are
 -- handled separately in repTy.
 repForallT :: HsType GhcRn -> MetaM (Core (M TH.Type))
@@ -1278,14 +1278,13 @@ repForallT ty
       }
 
 repTy :: HsType GhcRn -> MetaM (Core (M TH.Type))
-repTy ty@(HsForAllTy { hst_fvf = fvf, hst_bndrs = tvs, hst_body = body }) =
-  case fvf of
-    ForallInvis -> repForallT ty
-    ForallVis   -> let tvs' = map ((<$>) (setHsTyVarBndrFlag ())) tvs
-                       -- see Note [Specificity in HsForAllTy] in GHC.Hs.Type
-                   in addHsTyVarBinds tvs' $ \bndrs ->
-                   do body1 <- repLTy body
-                      repTForallVis bndrs body1
+repTy ty@(HsForAllTy { hst_tele = tele, hst_body = body }) =
+  case tele of
+    HsForAllInvis{} -> repForallT ty
+    HsForAllVis { hsf_vis_bndrs = tvs } ->
+      addHsTyVarBinds tvs $ \bndrs ->
+      do body1 <- repLTy body
+         repTForallVis bndrs body1
 repTy ty@(HsQualTy {}) = repForallT ty
 
 repTy (HsTyVar _ _ (L _ n))
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index c50514ffe1..24a3aa7c5b 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -1633,8 +1633,13 @@ instance ToHie (LHsType GhcRn) where
 
 instance ToHie (TScoped (LHsType GhcRn)) where
   toHie (TS tsc (L span t)) = concatM $ makeNode t span : case t of
-      HsForAllTy _ _ bndrs body ->
-        [ toHie $ tvScopes tsc (mkScope $ getLoc body) bndrs
+      HsForAllTy _ tele body ->
+        let scope = mkScope $ getLoc body in
+        [ case tele of
+            HsForAllVis { hsf_vis_bndrs = bndrs } ->
+              toHie $ tvScopes tsc scope bndrs
+            HsForAllInvis { hsf_invis_bndrs = bndrs } ->
+              toHie $ tvScopes tsc scope bndrs
         , toHie body
         ]
       HsQualTy _ ctx body ->
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index 2b7802a544..6ed05e3338 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -31,8 +31,7 @@ module GHC.Iface.Type (
         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
         IfaceForAllSpecBndr,
-        IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..),
-        ForallVisFlag(..), ShowForAllFlag(..),
+        IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..), ShowForAllFlag(..),
         mkIfaceForAllTvBndr,
         mkIfaceTyConKind,
         ifaceForAllSpecToBndrs, ifaceForAllSpecToBndr,
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index 1b04883fae..07e7572092 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -1890,9 +1890,16 @@ unpackedness :: { Located ([AddAnn], SourceText, SrcUnpackedness) }
         : '{-# UNPACK' '#-}'   { sLL $1 $> ([mo $1, mc $2], getUNPACK_PRAGs $1, SrcUnpack) }
         | '{-# NOUNPACK' '#-}' { sLL $1 $> ([mo $1, mc $2], getNOUNPACK_PRAGs $1, SrcNoUnpack) }
 
-forall_vis_flag :: { (AddAnn, ForallVisFlag) }
-        : '.'  { (mj AnnDot $1,    ForallInvis) }
-        | '->' { (mu AnnRarrow $1, ForallVis)   }
+forall_telescope :: { Located ([AddAnn], HsForAllTelescope GhcPs) }
+        : 'forall' tv_bndrs '.'  {% do { hintExplicitForall $1
+                                       ; pure $ sLL $1 $>
+                                           ( [mu AnnForall $1, mu AnnDot $3]
+                                           , mkHsForAllInvisTele $2 ) }}
+        | 'forall' tv_bndrs '->' {% do { hintExplicitForall $1
+                                       ; req_tvbs <- fromSpecTyVarBndrs $2
+                                       ; pure $ sLL $1 $> $
+                                           ( [mu AnnForall $1, mu AnnRarrow $3]
+                                           , mkHsForAllVisTele req_tvbs ) }}
 
 -- A ktype/ktypedoc is a ctype/ctypedoc, possibly with a kind annotation
 ktype :: { LHsType GhcPs }
@@ -1907,15 +1914,12 @@ ktypedoc :: { LHsType GhcPs }
 
 -- A ctype is a for-all type
 ctype   :: { LHsType GhcPs }
-        : 'forall' tv_bndrs forall_vis_flag ctype
-                                        {% let (fv_ann, fv_flag) = $3 in
-                                           hintExplicitForall $1 *>
-                                           ams (sLL $1 $> $
-                                                HsForAllTy { hst_fvf = fv_flag
-                                                           , hst_bndrs = $2
-                                                           , hst_xforall = noExtField
-                                                           , hst_body = $4 })
-                                               [mu AnnForall $1,fv_ann] }
+        : forall_telescope ctype      {% let (forall_anns, forall_tele) = unLoc $1 in
+                                         ams (sLL $1 $> $
+                                              HsForAllTy { hst_tele = forall_tele
+                                                         , hst_xforall = noExtField
+                                                         , hst_body = $2 })
+                                             forall_anns }
         | context '=>' ctype          {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2)
                                          >> return (sLL $1 $> $
                                             HsQualTy { hst_ctxt = $1
@@ -1937,15 +1941,12 @@ ctype   :: { LHsType GhcPs }
 -- to 'field' or to 'Int'. So we must use `ctype` to describe the type.
 
 ctypedoc :: { LHsType GhcPs }
-        : 'forall' tv_bndrs forall_vis_flag ctypedoc
-                                         {% let (fv_ann, fv_flag) = $3 in
-                                            hintExplicitForall $1 *>
-                                            ams (sLL $1 $> $
-                                                 HsForAllTy { hst_fvf = fv_flag
-                                                            , hst_bndrs = $2
-                                                            , hst_xforall = noExtField
-                                                            , hst_body = $4 })
-                                                [mu AnnForall $1,fv_ann] }
+        : forall_telescope ctypedoc   {% let (forall_anns, forall_tele) = unLoc $1 in
+                                         ams (sLL $1 $> $
+                                              HsForAllTy { hst_tele = forall_tele
+                                                         , hst_xforall = noExtField
+                                                         , hst_body = $2 })
+                                             forall_anns }
         | context '=>' ctypedoc       {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2)
                                          >> return (sLL $1 $> $
                                             HsQualTy { hst_ctxt = $1
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index df6a0f47a8..3f3eb48b68 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -23,6 +23,7 @@ module GHC.Rename.HsType (
         checkPrecMatch, checkSectionPrec,
 
         -- Binding related stuff
+        bindHsForAllTelescope,
         bindLHsTyVarBndr, bindLHsTyVarBndrs, WarnUnusedForalls(..),
         rnImplicitBndrs, bindSigTyVarsFV, bindHsQTyVars,
         FreeKiTyVars,
@@ -204,13 +205,11 @@ rnWcBody ctxt nwc_rdrs hs_ty
 
     rn_ty :: RnTyKiEnv -> HsType GhcPs -> RnM (HsType GhcRn, FreeVars)
     -- A lot of faff just to allow the extra-constraints wildcard to appear
-    rn_ty env (HsForAllTy { hst_fvf = fvf, hst_bndrs = tvs
-                          , hst_body = hs_body })
-      = bindLHsTyVarBndrs (rtke_ctxt env) WarnUnusedForalls
-                          Nothing tvs $ \ tvs' ->
+    rn_ty env (HsForAllTy { hst_tele = tele, hst_body = hs_body })
+      = bindHsForAllTelescope (rtke_ctxt env) tele $ \ tele' ->
         do { (hs_body', fvs) <- rn_lty env hs_body
-           ; return (HsForAllTy { hst_fvf = fvf, hst_xforall = noExtField
-                                , hst_bndrs = tvs', hst_body = hs_body' }
+           ; return (HsForAllTy { hst_xforall = noExtField
+                                , hst_tele = tele', hst_body = hs_body' }
                     , fvs) }
 
     rn_ty env (HsQualTy { hst_ctxt = L cx hs_ctxt
@@ -429,9 +428,10 @@ check_inferred_vars ctxt (Just msg) ty =
   where
     forallty_bndrs :: LHsType GhcPs -> [HsTyVarBndr Specificity GhcPs]
     forallty_bndrs (L _ ty) = case ty of
-      HsParTy _ ty'                  -> forallty_bndrs ty'
-      HsForAllTy { hst_bndrs = tvs } -> map unLoc tvs
-      _                              -> []
+      HsParTy _ ty' -> forallty_bndrs ty'
+      HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }}
+                    -> map unLoc tvs
+      _             -> []
 
 {- ******************************************************
 *                                                       *
@@ -559,14 +559,12 @@ rnLHsTyKi env (L loc ty)
 
 rnHsTyKi :: RnTyKiEnv -> HsType GhcPs -> RnM (HsType GhcRn, FreeVars)
 
-rnHsTyKi env ty@(HsForAllTy { hst_fvf = fvf, hst_bndrs = tyvars
-                            , hst_body = tau })
+rnHsTyKi env ty@(HsForAllTy { hst_tele = tele, hst_body = tau })
   = do { checkPolyKinds env ty
-       ; bindLHsTyVarBndrs (rtke_ctxt env) WarnUnusedForalls
-                           Nothing tyvars $ \ tyvars' ->
+       ; bindHsForAllTelescope (rtke_ctxt env) tele $ \ tele' ->
     do { (tau',  fvs) <- rnLHsTyKi env tau
-       ; return ( HsForAllTy { hst_fvf = fvf, hst_xforall = noExtField
-                             , hst_bndrs = tyvars' , hst_body =  tau' }
+       ; return ( HsForAllTy { hst_xforall = noExtField
+                             , hst_tele = tele' , hst_body =  tau' }
                 , fvs) } }
 
 rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
@@ -1051,6 +1049,19 @@ an LHsQTyVars can be semantically significant. As a result, we suppress
 -Wunused-foralls warnings in exactly one place: in bindHsQTyVars.
 -}
 
+bindHsForAllTelescope :: HsDocContext
+                      -> HsForAllTelescope GhcPs
+                      -> (HsForAllTelescope GhcRn -> RnM (a, FreeVars))
+                      -> RnM (a, FreeVars)
+bindHsForAllTelescope doc tele thing_inside =
+  case tele of
+    HsForAllVis { hsf_vis_bndrs = bndrs } ->
+      bindLHsTyVarBndrs doc WarnUnusedForalls Nothing bndrs $ \bndrs' ->
+        thing_inside $ mkHsForAllVisTele bndrs'
+    HsForAllInvis { hsf_invis_bndrs = bndrs } ->
+      bindLHsTyVarBndrs doc WarnUnusedForalls Nothing bndrs $ \bndrs' ->
+        thing_inside $ mkHsForAllInvisTele bndrs'
+
 -- | Should GHC warn if a quantified type variable goes unused? Usually, the
 -- answer is \"yes\", but in the particular case of binding 'LHsQTyVars', we
 -- avoid emitting warnings.
@@ -1820,8 +1831,8 @@ extract_lty (L _ ty) acc
       HsStarTy _ _                -> acc
       HsKindSig _ ty ki           -> extract_lty ty $
                                      extract_lty ki acc
-      HsForAllTy { hst_bndrs = tvs, hst_body = ty }
-                                  -> extract_hs_tv_bndrs tvs acc $
+      HsForAllTy { hst_tele = tele, hst_body = ty }
+                                  -> extract_hs_for_all_telescope tele acc $
                                      extract_lty ty []
       HsQualTy { hst_ctxt = ctxt, hst_body = ty }
                                   -> extract_lctxt ctxt $
@@ -1830,6 +1841,17 @@ extract_lty (L _ ty) acc
       -- We deal with these separately in rnLHsTypeWithWildCards
       HsWildCardTy {}             -> acc
 
+extract_hs_for_all_telescope :: HsForAllTelescope GhcPs
+                             -> FreeKiTyVars -- Accumulator
+                             -> FreeKiTyVars -- Free in body
+                             -> FreeKiTyVars
+extract_hs_for_all_telescope tele acc_vars body_fvs =
+  case tele of
+    HsForAllVis { hsf_vis_bndrs = bndrs } ->
+      extract_hs_tv_bndrs bndrs acc_vars body_fvs
+    HsForAllInvis { hsf_invis_bndrs = bndrs } ->
+      extract_hs_tv_bndrs bndrs acc_vars body_fvs
+
 extractHsTvBndrs :: [LHsTyVarBndr flag GhcPs]
                  -> FreeKiTyVars       -- Free in body
                  -> FreeKiTyVars       -- Free in result
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 533a794807..e610a60ff3 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2182,13 +2182,13 @@ rnConDecl (XConDecl (ConDeclGADTPrefixPs { con_gp_names = names, con_gp_ty = ty
          -- Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)
          -- in GHC.Hs.Type.
        ; case res_ty of
-           L l (HsForAllTy { hst_fvf = fvf })
-             |  ForallVis <- fvf
+           L l (HsForAllTy { hst_tele = tele })
+             |  HsForAllVis{} <- tele
              -> setSrcSpan l $ addErr $ withHsDocContext ctxt $ vcat
                 [ text "Illegal visible, dependent quantification" <+>
                   text "in the type of a term"
                 , text "(GHC does not yet support this)" ]
-             |  ForallInvis <- fvf
+             |  HsForAllInvis{} <- tele
              -> nested_foralls_contexts_err l ctxt
            L l (HsQualTy {})
              -> nested_foralls_contexts_err l ctxt
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)
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index 9dea719093..1a74f417d8 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -1490,19 +1490,19 @@ cvtTypeKind ty_str ty
                    ; cxt' <- cvtContext funPrec cxt
                    ; ty'  <- cvtType ty
                    ; loc <- getL
-                   ; let hs_ty  = mkHsForAllTy loc ForallInvis tvs' rho_ty
+                   ; let tele   = mkHsForAllInvisTele tvs'
+                         hs_ty  = mkHsForAllTy loc tele rho_ty
                          rho_ty = mkHsQualTy cxt loc cxt' ty'
 
                    ; return hs_ty }
 
            ForallVisT tvs ty
              | null tys'
-             -> do { let tvs_spec = map (TH.SpecifiedSpec <$) tvs
-                   -- see Note [Specificity in HsForAllTy] in GHC.Hs.Type
-                   ; tvs_spec' <- cvtTvs tvs_spec
-                   ; ty'       <- cvtType ty
-                   ; loc       <- getL
-                   ; pure $ mkHsForAllTy loc ForallVis tvs_spec' ty' }
+             -> do { tvs' <- cvtTvs tvs
+                   ; ty'  <- cvtType ty
+                   ; loc  <- getL
+                   ; let tele = mkHsForAllVisTele tvs'
+                   ; pure $ mkHsForAllTy loc tele ty' }
 
            SigT ty ki
              -> do { ty' <- cvtType ty
@@ -1735,8 +1735,7 @@ cvtPatSynSigTy (ForallT univs reqs (ForallT exis provs ty))
                                ; univs' <- cvtTvs univs
                                ; ty'    <- cvtType (ForallT exis provs ty)
                                ; let forTy = HsForAllTy
-                                              { hst_fvf = ForallInvis
-                                              , hst_bndrs = univs'
+                                              { hst_tele = mkHsForAllInvisTele univs'
                                               , hst_xforall = noExtField
                                               , hst_body = L l cxtTy }
                                      cxtTy = HsQualTy { hst_ctxt = L l []
@@ -1788,21 +1787,21 @@ unboxedSumChecks alt arity
 mkHsForAllTy :: SrcSpan
              -- ^ The location of the returned 'LHsType' if it needs an
              --   explicit forall
-             -> ForallVisFlag
-             -- ^ Whether this is @forall@ is visible (e.g., @forall a ->@)
-             --   or invisible (e.g., @forall a.@)
-             -> [LHsTyVarBndr Hs.Specificity GhcPs]
+             -> HsForAllTelescope GhcPs
              -- ^ The converted type variable binders
              -> LHsType GhcPs
              -- ^ The converted rho type
              -> LHsType GhcPs
              -- ^ The complete type, quantified with a forall if necessary
-mkHsForAllTy loc fvf tvs rho_ty
-  | null tvs  = rho_ty
-  | otherwise = L loc $ HsForAllTy { hst_fvf = fvf
-                                   , hst_bndrs = tvs
+mkHsForAllTy loc tele rho_ty
+  | no_tvs    = rho_ty
+  | otherwise = L loc $ HsForAllTy { hst_tele = tele
                                    , hst_xforall = noExtField
                                    , hst_body = rho_ty }
+  where
+    no_tvs = case tele of
+      HsForAllVis   { hsf_vis_bndrs   = bndrs } -> null bndrs
+      HsForAllInvis { hsf_invis_bndrs = bndrs } -> null bndrs
 
 -- | If passed an empty 'TH.Cxt', this simply returns the third argument
 -- (an 'LHsType'). Otherwise, return an 'HsQualTy' using the provided
diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs
index 0e7e806656..a3974a92bd 100644
--- a/compiler/GHC/Types/Var.hs
+++ b/compiler/GHC/Types/Var.hs
@@ -65,11 +65,10 @@ module GHC.Types.Var (
         -- * ArgFlags
         ArgFlag(Invisible,Required,Specified,Inferred),
         isVisibleArgFlag, isInvisibleArgFlag, sameVis,
-        AnonArgFlag(..), ForallVisFlag(..), argToForallVisFlag,
-        Specificity(..),
+        AnonArgFlag(..), Specificity(..),
 
         -- * TyVar's
-        VarBndr(..), TyCoVarBinder, TyVarBinder, InvisTVBinder,
+        VarBndr(..), TyCoVarBinder, TyVarBinder, InvisTVBinder, ReqTVBinder,
         binderVar, binderVars, binderArgFlag, binderType,
         mkTyCoVarBinder, mkTyCoVarBinders,
         mkTyVarBinder, mkTyVarBinders,
@@ -405,7 +404,6 @@ data ArgFlag = Invisible Specificity
   -- (<) on ArgFlag means "is less visible than"
 
 -- | Whether an 'Invisible' argument may appear in source Haskell.
--- see Note [Specificity in HsForAllTy] in GHC.Hs.Type
 data Specificity = InferredSpec
                    -- ^ the argument may not appear in source Haskell, it is
                    -- only inferred.
@@ -469,7 +467,6 @@ instance Binary ArgFlag where
 -- Appears here partly so that it's together with its friends ArgFlag
 -- and ForallVisFlag, but also because it is used in IfaceType, rather
 -- early in the compilation chain
--- See Note [AnonArgFlag vs. ForallVisFlag]
 data AnonArgFlag
   = VisArg    -- ^ Used for @(->)@: an ordinary non-dependent arrow.
               --   The argument is visible in source code.
@@ -491,26 +488,6 @@ instance Binary AnonArgFlag where
       0 -> return VisArg
       _ -> return InvisArg
 
--- | Is a @forall@ invisible (e.g., @forall a b. {...}@, with a dot) or visible
--- (e.g., @forall a b -> {...}@, with an arrow)?
-
--- See Note [AnonArgFlag vs. ForallVisFlag]
-data ForallVisFlag
-  = ForallVis   -- ^ A visible @forall@ (with an arrow)
-  | ForallInvis -- ^ An invisible @forall@ (with a dot)
-  deriving (Eq, Ord, Data)
-
-instance Outputable ForallVisFlag where
-  ppr f = text $ case f of
-                   ForallVis   -> "ForallVis"
-                   ForallInvis -> "ForallInvis"
-
--- | Convert an 'ArgFlag' to its corresponding 'ForallVisFlag'.
-argToForallVisFlag :: ArgFlag -> ForallVisFlag
-argToForallVisFlag Required  = ForallVis
-argToForallVisFlag Specified = ForallInvis
-argToForallVisFlag Inferred  = ForallInvis
-
 {- Note [AnonArgFlag]
 ~~~~~~~~~~~~~~~~~~~~~
 AnonArgFlag is used principally in the FunTy constructor of Type.
@@ -564,30 +541,7 @@ Conclusion: the easiest thing is to make mkLamType build
             (c => ty)
 when the argument is a predicate type.  See GHC.Core.TyCo.Rep
 Note [Types for coercions, predicates, and evidence]
-
-Note [AnonArgFlag vs. ForallVisFlag]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The AnonArgFlag and ForallVisFlag data types are quite similar at a first
-glance:
-
-  data AnonArgFlag   = VisArg    | InvisArg
-  data ForallVisFlag = ForallVis | ForallInvis
-
-Both data types keep track of visibility of some sort. AnonArgFlag tracks
-whether a FunTy has a visible argument (->) or an invisible predicate argument
-(=>). ForallVisFlag tracks whether a `forall` quantifier in a user-specified
-HsType is
-   visible:   forall a -> {...}
-   invisible: forall a. {...}
-In fact the visible form can currently only appear in kinds.
-
-Given their similarities, it's tempting to want to combine these two
-data types into one, but they actually represent distinct
-concepts. AnonArgFlag reflects a property of *Core* types, whereas
-ForallVisFlag reflects a property of the HsSyn source-code AST. In
-other words, AnonArgFlag is all about internals, whereas ForallVisFlag
-is all about surface syntax. Therefore, they are kept as separate data
-types.  -}
+-}
 
 {- *********************************************************************
 *                                                                      *
@@ -598,14 +552,16 @@ types.  -}
 -- Variable Binder
 --
 -- VarBndr is polymorphic in both var and visibility fields.
--- Currently there are sevenv different uses of 'VarBndr':
---   * Var.TyVarBinder            = VarBndr TyVar ArgFlag
---   * Var.InvisTVBinder          = VarBndr TyVar Specificity
---   * Var.TyCoVarBinder          = VarBndr TyCoVar ArgFlag
---   * TyCon.TyConBinder          = VarBndr TyVar TyConBndrVis
---   * TyCon.TyConTyCoBinder      = VarBndr TyCoVar TyConBndrVis
---   * IfaceType.IfaceForAllBndr  = VarBndr IfaceBndr ArgFlag
---   * IfaceType.IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
+-- Currently there are nine different uses of 'VarBndr':
+--   * Var.TyVarBinder               = VarBndr TyVar ArgFlag
+--   * Var.TyCoVarBinder             = VarBndr TyCoVar ArgFlag
+--   * Var.InvisTVBinder             = VarBndr TyVar Specificity
+--   * Var.ReqTVBinder               = VarBndr TyVar ()
+--   * TyCon.TyConBinder             = VarBndr TyVar TyConBndrVis
+--   * TyCon.TyConTyCoBinder         = VarBndr TyCoVar TyConBndrVis
+--   * IfaceType.IfaceForAllBndr     = VarBndr IfaceBndr ArgFlag
+--   * IfaceType.IfaceTyConBinder    = VarBndr IfaceBndr TyConBndrVis
+--   * IfaceType.IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity
 data VarBndr var argf = Bndr var argf
   deriving( Data )
 
@@ -619,6 +575,7 @@ data VarBndr var argf = Bndr var argf
 type TyCoVarBinder     = VarBndr TyCoVar ArgFlag
 type TyVarBinder       = VarBndr TyVar   ArgFlag
 type InvisTVBinder     = VarBndr TyVar   Specificity
+type ReqTVBinder       = VarBndr TyVar   ()
 
 tyVarSpecToBinders :: [VarBndr a Specificity] -> [VarBndr a ArgFlag]
 tyVarSpecToBinders = map tyVarSpecToBinder