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.

3 files changed, 64 insertions, 56 deletions

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