Visible dependent quantification

This implements GHC proposal 35 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst) by adding the ability to write kinds with visible dependent quantification (VDQ). Most of the work for supporting VDQ was actually done _before_ this patch. That is, GHC has been able to reason about kinds with VDQ for some time, but it lacked the ability to let programmers directly write these kinds in the source syntax. This patch is primarly about exposing this ability, by: * Changing `HsForAllTy` to add an additional field of type `ForallVisFlag` to distinguish between invisible `forall`s (i.e, with dots) and visible `forall`s (i.e., with arrows) * Changing `Parser.y` accordingly The rest of the patch mostly concerns adding validity checking to ensure that VDQ is never used in the type of a term (as permitting this would require full-spectrum dependent types). This is accomplished by: * Adding a `vdqAllowed` predicate to `TcValidity`. * Introducing `splitLHsSigmaTyInvis`, a variant of `splitLHsSigmaTy` that only splits invisible `forall`s. This function is used in certain places (e.g., in instance declarations) to ensure that GHC doesn't try to split visible `forall`s (e.g., if it tried splitting `instance forall a -> Show (Blah a)`, then GHC would mistakenly allow that declaration!) This also updates Template Haskell by introducing a new `ForallVisT` constructor to `Type`. Fixes #16326. Also fixes #15658 by documenting this feature in the users' guide.
author: Ryan Scott <ryan.gl.scott@gmail.com> 2018-12-17 20:54:36 -0500
committer: Marge Bot <ben+marge-bot@smart-cactus.org> 2019-03-01 16:26:02 -0500
commit: c26d299dc422f43b8c37da4b26da2067eedcbae8 (patch)
tree: 517d7b87043152bee667485e186314d19b55cfba
parent: f838809f1e73c20bc70926fe98e735297572ac60 (diff)
download: haskell-c26d299dc422f43b8c37da4b26da2067eedcbae8.tar.gz
64 files changed, 813 insertions, 148 deletions
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs
index 7e451e5407..f397793bf7 100644
--- a/compiler/basicTypes/Var.hs
+++ b/compiler/basicTypes/Var.hs
@@ -62,7 +62,7 @@ module Var (
 
         -- * ArgFlags
         ArgFlag(..), isVisibleArgFlag, isInvisibleArgFlag, sameVis,
-        AnonArgFlag(..),
+        AnonArgFlag(..), ForallVisFlag(..), argToForallVisFlag,
 
         -- * TyVar's
         VarBndr(..), TyCoVarBinder, TyVarBinder,
@@ -425,15 +425,17 @@ instance Binary ArgFlag where
       1 -> return Specified
       _ -> return Inferred
 
--- The non-dependent version of ArgFlag, namely AnonArgFlag,
--- appears here partly so that it's together with its friend ArgFlag,
+-- | The non-dependent version of 'ArgFlag'.
+
+-- Appears here partly so that it's together with its friend ArgFlag,
 -- 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
-  | InvisArg  -- Used for (=>): a non-dependent predicate arrow
-              -- The argument is invisible in source code
+  = VisArg    -- ^ Used for @(->)@: an ordinary non-dependent arrow.
+              --   The argument is visible in source code.
+  | InvisArg  -- ^ Used for @(=>)@: a non-dependent predicate arrow.
+              --   The argument is invisible in source code.
   deriving (Eq, Ord, Data)
 
 instance Outputable AnonArgFlag where
@@ -450,6 +452,47 @@ 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 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 is visible
+(forall a -> {...}) or invisible (forall a. {...}).
+
+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 GHC
+AST. In other words, AnonArgFlag is all about internals, whereas ForallVisFlag
+is all about surface syntax. Therefore, they are kept as separate data types.
+-}
+
 {- *********************************************************************
 *                                                                      *
 *                   VarBndr, TyCoVarBinder
diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index a8a4fb6b40..5e0976d1a2 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -1144,18 +1144,21 @@ repLTys tys = mapM repLTy tys
 repLTy :: LHsType GhcRn -> DsM (Core TH.TypeQ)
 repLTy ty = repTy (unLoc ty)
 
-repForall :: HsType GhcRn -> DsM (Core TH.TypeQ)
+repForall :: ForallVisFlag -> HsType GhcRn -> DsM (Core TH.TypeQ)
 -- Arg of repForall is always HsForAllTy or HsQualTy
-repForall ty
+repForall fvf ty
  | (tvs, ctxt, tau) <- splitLHsSigmaTy (noLoc ty)
  = addHsTyVarBinds tvs $ \bndrs ->
    do { ctxt1  <- repLContext ctxt
       ; ty1    <- repLTy tau
-      ; repTForall bndrs ctxt1 ty1 }
+      ; case fvf of
+          ForallVis   -> repTForallVis bndrs ty1    -- forall a      -> {...}
+          ForallInvis -> repTForall bndrs ctxt1 ty1 -- forall a. C a => {...}
+      }
 
 repTy :: HsType GhcRn -> DsM (Core TH.TypeQ)
-repTy ty@(HsForAllTy {}) = repForall ty
-repTy ty@(HsQualTy {})   = repForall ty
+repTy ty@(HsForAllTy {hst_fvf = fvf}) = repForall fvf         ty
+repTy ty@(HsQualTy {})                = repForall ForallInvis ty
 
 repTy (HsTyVar _ _ (dL->L _ n))
   | isLiftedTypeKindTyConName n       = repTStar
@@ -2467,6 +2470,10 @@ repTForall :: Core [TH.TyVarBndrQ] -> Core TH.CxtQ -> Core TH.TypeQ
 repTForall (MkC tvars) (MkC ctxt) (MkC ty)
     = rep2 forallTName [tvars, ctxt, ty]
 
+repTForallVis :: Core [TH.TyVarBndrQ] -> Core TH.TypeQ
+              -> DsM (Core TH.TypeQ)
+repTForallVis (MkC tvars) (MkC ty) = rep2 forallVisTName [tvars, ty]
+
 repTvar :: Core TH.Name -> DsM (Core TH.TypeQ)
 repTvar (MkC s) = rep2 varTName [s]
 
diff --git a/compiler/hieFile/HieAst.hs b/compiler/hieFile/HieAst.hs
index 9752403054..2b112153bd 100644
--- a/compiler/hieFile/HieAst.hs
+++ b/compiler/hieFile/HieAst.hs
@@ -1386,7 +1386,7 @@ 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 ->
+      HsForAllTy _ _ bndrs body ->
         [ toHie $ tvScopes tsc (mkScope $ getLoc body) bndrs
         , toHie body
         ]
diff --git a/compiler/hsSyn/Convert.hs b/compiler/hsSyn/Convert.hs
index 1a801bb1b1..364bcb06c2 100644
--- a/compiler/hsSyn/Convert.hs
+++ b/compiler/hsSyn/Convert.hs
@@ -1405,11 +1405,18 @@ cvtTypeKind ty_str ty
                    ; let pcxt = parenthesizeHsContext funPrec cxt'
                    ; ty'  <- cvtType ty
                    ; loc <- getL
-                   ; let hs_ty  = mkHsForAllTy tvs loc tvs' rho_ty
+                   ; let hs_ty  = mkHsForAllTy tvs loc ForallInvis tvs' rho_ty
                          rho_ty = mkHsQualTy cxt loc pcxt ty'
 
                    ; return hs_ty }
 
+           ForallVisT tvs ty
+             | null tys'
+             -> do { tvs' <- cvtTvs tvs
+                   ; ty'  <- cvtType ty
+                   ; loc  <- getL
+                   ; pure $ mkHsForAllTy tvs loc ForallVis tvs' ty' }
+
            SigT ty ki
              -> do { ty' <- cvtType ty
                    ; ki' <- cvtKind ki
@@ -1638,7 +1645,8 @@ cvtPatSynSigTy (ForallT univs reqs (ForallT exis provs ty))
                                ; univs' <- hsQTvExplicit <$> cvtTvs univs
                                ; ty'    <- cvtType (ForallT exis provs ty)
                                ; let forTy = HsForAllTy
-                                              { hst_bndrs = univs'
+                                              { hst_fvf = ForallInvis
+                                              , hst_bndrs = univs'
                                               , hst_xforall = noExt
                                               , hst_body = cL l cxtTy }
                                      cxtTy = HsQualTy { hst_ctxt = cL l []
@@ -1692,15 +1700,19 @@ mkHsForAllTy :: [TH.TyVarBndr]
              -> 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.@)
              -> LHsQTyVars GhcPs
              -- ^ The converted type variable binders
              -> LHsType GhcPs
              -- ^ The converted rho type
              -> LHsType GhcPs
              -- ^ The complete type, quantified with a forall if necessary
-mkHsForAllTy tvs loc tvs' rho_ty
+mkHsForAllTy tvs loc fvf tvs' rho_ty
   | null tvs  = rho_ty
-  | otherwise = cL loc $ HsForAllTy { hst_bndrs = hsQTvExplicit tvs'
+  | otherwise = cL loc $ HsForAllTy { hst_fvf = fvf
+                                    , hst_bndrs = hsQTvExplicit tvs'
                                     , hst_xforall = noExt
                                     , hst_body = rho_ty }
 
diff --git a/compiler/hsSyn/HsDecls.hs b/compiler/hsSyn/HsDecls.hs
index c18a9ae1fc..f8709fbe1e 100644
--- a/compiler/hsSyn/HsDecls.hs
+++ b/compiler/hsSyn/HsDecls.hs
@@ -1457,7 +1457,7 @@ pprConDecl (ConDeclH98 { con_name = L _ con
                        , con_mb_cxt = mcxt
                        , con_args = args
                        , con_doc = doc })
-  = sep [ppr_mbDoc doc, pprHsForAll ex_tvs cxt, ppr_details args]
+  = sep [ppr_mbDoc doc, pprHsForAll ForallInvis 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
@@ -1470,7 +1470,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 (hsq_explicit qvars) cxt,
+    <+> (sep [pprHsForAll ForallInvis (hsq_explicit qvars) cxt,
               ppr_arrow_chain (get_args args ++ [ppr res_ty]) ])
   where
     get_args (PrefixCon args) = map ppr args
@@ -1777,7 +1777,7 @@ pprHsFamInstLHS :: (OutputableBndrId (GhcPass p))
    -> LHsContext (GhcPass p)
    -> SDoc
 pprHsFamInstLHS thing bndrs typats fixity mb_ctxt
-   = hsep [ pprHsExplicitForAll bndrs
+   = hsep [ pprHsExplicitForAll ForallInvis bndrs
           , pprLHsContext mb_ctxt
           , pp_pats typats ]
    where
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index fa87613416..aabe9f4597 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -19,7 +19,7 @@ HsTypes: Abstract syntax: user-defined types
 
 module HsTypes (
         HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind,
-        HsTyVarBndr(..), LHsTyVarBndr,
+        HsTyVarBndr(..), LHsTyVarBndr, ForallVisFlag(..),
         LHsQTyVars(..), HsQTvsRn(..),
         HsImplicitBndrs(..),
         HsWildCardBndrs(..),
@@ -56,7 +56,8 @@ module HsTypes (
         hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames,
         splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
         splitLHsPatSynTy,
-        splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy,
+        splitLHsForAllTy, splitLHsForAllTyInvis,
+        splitLHsQualTy, splitLHsSigmaTy, splitLHsSigmaTyInvis,
         splitHsFunType, hsTyGetAppHead_maybe,
         mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
         ignoreParens, hsSigType, hsSigWcType,
@@ -142,13 +143,18 @@ is a bit complicated.  Here's how it works.
 
 * In a HsType,
      HsForAllTy   represents an /explicit, user-written/ 'forall'
-                   e.g.   forall a b. ...
+                   e.g.   forall a b.   {...} or
+                          forall a b -> {...}
      HsQualTy     represents an /explicit, user-written/ context
                    e.g.   (Eq a, Show a) => ...
                   The context can be empty if that's what the user wrote
   These constructors represent what the user wrote, no more
   and no less.
 
+* The ForallVisFlag 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).
+
 * HsTyVarBndr describes a quantified type variable written by the
   user.  For example
      f :: forall a (b :: *).  blah
@@ -512,8 +518,10 @@ hsTvbAllKinded = all (isHsKindedTyVar . unLoc) . hsQTvExplicit
 -- | Haskell Type
 data HsType pass
   = HsForAllTy   -- See Note [HsType binders]
-      { hst_xforall :: XForAllTy pass,
-        hst_bndrs   :: [LHsTyVarBndr pass]
+      { hst_xforall :: XForAllTy pass
+      , hst_fvf     :: ForallVisFlag -- Is this `forall a -> {...}` or
+                                     --         `forall a. {...}`?
+      , hst_bndrs   :: [LHsTyVarBndr pass]
                                        -- Explicit, user-supplied 'forall a b c'
       , hst_body    :: LHsType pass      -- body type
       }
@@ -1137,6 +1145,13 @@ The SrcSpan is the span of the original HsPar
 -}
 
 --------------------------------
+
+-- | Decompose a pattern synonym type signature into its constituent parts.
+--
+-- Note that this function looks through parentheses, so it will work on types
+-- such as @(forall a. <...>)@. The downside to this is that it is not
+-- generally possible to take the returned types and reconstruct the original
+-- type (parentheses and all) from them.
 splitLHsPatSynTy :: LHsType pass
                  -> ( [LHsTyVarBndr pass]    -- universals
                     , LHsContext pass        -- required constraints
@@ -1145,11 +1160,18 @@ splitLHsPatSynTy :: LHsType pass
                     , LHsType pass)          -- body type
 splitLHsPatSynTy ty = (univs, reqs, exis, provs, ty4)
   where
-    (univs, ty1) = splitLHsForAllTy ty
+    (univs, ty1) = splitLHsForAllTyInvis ty
     (reqs,  ty2) = splitLHsQualTy ty1
-    (exis,  ty3) = splitLHsForAllTy ty2
+    (exis,  ty3) = splitLHsForAllTyInvis ty2
     (provs, ty4) = splitLHsQualTy ty3
 
+-- | Decompose a sigma type (of the form @forall <tvs>. context => body@)
+-- into its constituent parts.
+--
+-- Note that this function looks through parentheses, so it will work on types
+-- such as @(forall a. <...>)@. The downside to this is that it is not
+-- generally possible to take the returned types and reconstruct the original
+-- type (parentheses and all) from them.
 splitLHsSigmaTy :: LHsType pass
                 -> ([LHsTyVarBndr pass], LHsContext pass, LHsType pass)
 splitLHsSigmaTy ty
@@ -1157,22 +1179,82 @@ splitLHsSigmaTy ty
   , (ctxt, ty2) <- splitLHsQualTy ty1
   = (tvs, ctxt, ty2)
 
+-- | Like 'splitLHsSigmaTy', but only splits type variable binders that were
+-- quantified invisibly (e.g., @forall a.@, with a dot).
+--
+-- This function is used to split apart certain types, such as instance
+-- declaration types, which disallow visible @forall@s. For instance, if GHC
+-- split apart the @forall@ in @instance forall a -> Show (Blah a)@, then that
+-- declaration would mistakenly be accepted!
+--
+-- Note that this function looks through parentheses, so it will work on types
+-- such as @(forall a. <...>)@. The downside to this is that it is not
+-- generally possible to take the returned types and reconstruct the original
+-- type (parentheses and all) from them.
+splitLHsSigmaTyInvis :: LHsType pass
+                     -> ([LHsTyVarBndr pass], LHsContext pass, LHsType pass)
+splitLHsSigmaTyInvis ty
+  | (tvs,  ty1) <- splitLHsForAllTyInvis ty
+  , (ctxt, ty2) <- splitLHsQualTy ty1
+  = (tvs, ctxt, ty2)
+
+-- | Decompose a type of the form @forall <tvs>. body@) into its constituent
+-- parts.
+--
+-- Note that this function looks through parentheses, so it will work on types
+-- such as @(forall a. <...>)@. The downside to this is that it is not
+-- generally possible to take the returned types and reconstruct the original
+-- type (parentheses and all) from them.
 splitLHsForAllTy :: LHsType pass -> ([LHsTyVarBndr pass], LHsType pass)
 splitLHsForAllTy (L _ (HsParTy _ ty)) = splitLHsForAllTy ty
 splitLHsForAllTy (L _ (HsForAllTy { hst_bndrs = tvs, hst_body = body })) = (tvs, body)
 splitLHsForAllTy body              = ([], body)
 
+-- | Like 'splitLHsForAllTy', but only splits type variable binders that
+-- were quantified invisibly (e.g., @forall a.@, with a dot).
+--
+-- This function is used to split apart certain types, such as instance
+-- declaration types, which disallow visible @forall@s. For instance, if GHC
+-- split apart the @forall@ in @instance forall a -> Show (Blah a)@, then that
+-- declaration would mistakenly be accepted!
+--
+-- Note that this function looks through parentheses, so it will work on types
+-- such as @(forall a. <...>)@. The downside to this is that it is not
+-- generally possible to take the returned types and reconstruct the original
+-- type (parentheses and all) from them.
+splitLHsForAllTyInvis :: LHsType pass -> ([LHsTyVarBndr pass], LHsType pass)
+splitLHsForAllTyInvis lty@(L _ ty) =
+  case ty of
+    HsParTy _ ty' -> splitLHsForAllTyInvis ty'
+    HsForAllTy { hst_fvf = fvf', hst_bndrs = tvs', hst_body = body' }
+      |  fvf' == ForallInvis
+      -> (tvs', body')
+    _ -> ([], lty)
+
+-- | Decompose a type of the form @context => body@ into its constituent parts.
+--
+-- Note that this function looks through parentheses, so it will work on types
+-- such as @(context => <...>)@. The downside to this is that it is not
+-- generally possible to take the returned types and reconstruct the original
+-- type (parentheses and all) from them.
 splitLHsQualTy :: LHsType pass -> (LHsContext pass, LHsType pass)
 splitLHsQualTy (L _ (HsParTy _ ty)) = splitLHsQualTy ty
 splitLHsQualTy (L _ (HsQualTy { hst_ctxt = ctxt, hst_body = body })) = (ctxt,     body)
 splitLHsQualTy body              = (noLHsContext, body)
 
+-- | Decompose a type class instance type (of the form
+-- @forall <tvs>. context => instance_head@) into its constituent parts.
+--
+-- Note that this function looks through parentheses, so it will work on types
+-- such as @(forall <tvs>. <...>)@. The downside to this is that it is not
+-- generally possible to take the returned types and reconstruct the original
+-- type (parentheses and all) from them.
 splitLHsInstDeclTy :: LHsSigType GhcRn
                    -> ([Name], LHsContext GhcRn, LHsType GhcRn)
 -- Split up an instance decl type, returning the pieces
 splitLHsInstDeclTy (HsIB { hsib_ext = itkvs
                          , hsib_body = inst_ty })
-  | (tvs, cxt, body_ty) <- splitLHsSigmaTy inst_ty
+  | (tvs, cxt, body_ty) <- splitLHsSigmaTyInvis inst_ty
   = (itkvs ++ map hsLTyVarName tvs, cxt, body_ty)
          -- Return implicitly bound type and kind vars
          -- For an instance decl, all of them are in scope
@@ -1180,7 +1262,7 @@ splitLHsInstDeclTy (XHsImplicitBndrs _) = panic "splitLHsInstDeclTy"
 
 getLHsInstDeclHead :: LHsSigType pass -> LHsType pass
 getLHsInstDeclHead inst_ty
-  | (_tvs, _cxt, body_ty) <- splitLHsSigmaTy (hsSigType inst_ty)
+  | (_tvs, _cxt, body_ty) <- splitLHsSigmaTyInvis (hsSigType inst_ty)
   = body_ty
 
 getLHsInstDeclClass_maybe :: LHsSigType (GhcPass p)
@@ -1326,10 +1408,11 @@ instance (p ~ GhcPass pass,Outputable thing)
 pprAnonWildCard :: SDoc
 pprAnonWildCard = char '_'
 
--- | Prints a forall; When passed an empty list, prints @forall.@ only when
--- @-dppr-debug@
+-- | Prints a forall; When passed an empty list, prints @forall .@/@forall ->@
+-- only when @-dppr-debug@ is enabled.
 pprHsForAll :: (OutputableBndrId (GhcPass p))
-            => [LHsTyVarBndr (GhcPass p)] -> LHsContext (GhcPass p) -> SDoc
+            => ForallVisFlag -> [LHsTyVarBndr (GhcPass p)]
+            -> LHsContext (GhcPass p) -> SDoc
 pprHsForAll = pprHsForAllExtra Nothing
 
 -- | Version of 'pprHsForAll' that can also print an extra-constraints
@@ -1340,20 +1423,31 @@ pprHsForAll = pprHsForAllExtra Nothing
 -- 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 (GhcPass p))
-                 => Maybe SrcSpan -> [LHsTyVarBndr (GhcPass p)]
+                 => Maybe SrcSpan -> ForallVisFlag
+                 -> [LHsTyVarBndr (GhcPass p)]
                  -> LHsContext (GhcPass p) -> SDoc
-pprHsForAllExtra extra qtvs cxt
+pprHsForAllExtra extra fvf qtvs cxt
   = pp_forall <+> pprLHsContextExtra (isJust extra) cxt
   where
-    pp_forall | null qtvs = whenPprDebug (forAllLit <> dot)
-              | otherwise = forAllLit <+> interppSP qtvs <> dot
+    pp_forall | null qtvs = whenPprDebug (forAllLit <> separator)
+              | otherwise = forAllLit <+> interppSP qtvs <> separator
+
+    separator = ppr_forall_separator fvf
 
--- | Version of 'pprHsForall' or 'pprHsForallExtra' that will always print
+-- | Version of 'pprHsForAll' or 'pprHsForAllExtra' that will always print
 -- @forall.@ when passed @Just []@. Prints nothing if passed 'Nothing'
 pprHsExplicitForAll :: (OutputableBndrId (GhcPass p))
-               => Maybe [LHsTyVarBndr (GhcPass p)] -> SDoc
-pprHsExplicitForAll (Just qtvs) = forAllLit <+> interppSP qtvs <> dot
-pprHsExplicitForAll Nothing     = empty
+                    => 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
 
 pprLHsContext :: (OutputableBndrId (GhcPass p))
               => LHsContext (GhcPass p) -> SDoc
@@ -1413,8 +1507,8 @@ ppr_mono_lty :: (OutputableBndrId (GhcPass p)) => LHsType (GhcPass p) -> SDoc
 ppr_mono_lty ty = ppr_mono_ty (unLoc ty)
 
 ppr_mono_ty :: (OutputableBndrId (GhcPass p)) => HsType (GhcPass p) -> SDoc
-ppr_mono_ty (HsForAllTy { hst_bndrs = tvs, hst_body = ty })
-  = sep [pprHsForAll tvs noLHsContext, ppr_mono_lty ty]
+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 (HsQualTy { hst_ctxt = ctxt, hst_body = ty })
   = sep [pprLHsContextAlways ctxt, ppr_mono_lty ty]
diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index 16b2cf9dfd..62c153ef52 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -658,9 +658,10 @@ typeToLHsType ty
                                       , hst_xqual = noExt
                                       , hst_body = go tau })
 
-    go ty@(ForAllTy {})
-      | (tvs, tau) <- tcSplitForAllTys ty
-      = noLoc (HsForAllTy { hst_bndrs = map go_tv tvs
+    go ty@(ForAllTy (Bndr _ argf) _)
+      | (tvs, tau) <- tcSplitForAllTysSameVis argf ty
+      = noLoc (HsForAllTy { hst_fvf = argToForallVisFlag argf
+                          , hst_bndrs = map go_tv tvs
                           , hst_xforall = noExt
                           , hst_body = go tau })
     go (TyVarTy tv)         = nlHsTyVar (getRdrName tv)
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 985a612940..e2235ab01f 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -21,7 +21,8 @@ module IfaceType (
         IfaceTyLit(..), IfaceAppArgs(..),
         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
-        IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..), ShowForAllFlag(..),
+        IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..),
+        ForallVisFlag(..), ShowForAllFlag(..),
         mkIfaceForAllTvBndr,
 
         ifForAllBndrVar, ifForAllBndrName, ifaceBndrName,
diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y
index 63473b4540..739090f3f6 100644
--- a/compiler/parser/Parser.y
+++ b/compiler/parser/Parser.y
@@ -1852,6 +1852,10 @@ 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) }
+        | '->' { (mj AnnRarrow $1, ForallVis)   }
+
 -- A ktype/ktypedoc is a ctype/ctypedoc, possibly with a kind annotation
 ktype :: { LHsType GhcPs }
         : ctype                { $1 }
@@ -1865,12 +1869,15 @@ ktypedoc :: { LHsType GhcPs }
 
 -- A ctype is a for-all type
 ctype   :: { LHsType GhcPs }
-        : 'forall' tv_bndrs '.' ctype   {% hintExplicitForall $1 >>
+        : 'forall' tv_bndrs forall_vis_flag ctype
+                                        {% let (fv_ann, fv_flag) = $3 in
+                                           hintExplicitForall $1 *>
                                            ams (sLL $1 $> $
-                                                HsForAllTy { hst_bndrs = $2
+                                                HsForAllTy { hst_fvf = fv_flag
+                                                           , hst_bndrs = $2
                                                            , hst_xforall = noExt
                                                            , hst_body = $4 })
-                                               [mu AnnForall $1, mj AnnDot $3] }
+                                               [mu AnnForall $1,fv_ann] }
         | context '=>' ctype          {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2)
                                          >> return (sLL $1 $> $
                                             HsQualTy { hst_ctxt = $1
@@ -1892,12 +1899,15 @@ ctype   :: { LHsType GhcPs }
 -- to 'field' or to 'Int'. So we must use `ctype` to describe the type.
 
 ctypedoc :: { LHsType GhcPs }
-        : 'forall' tv_bndrs '.' ctypedoc {% hintExplicitForall $1 >>
+        : 'forall' tv_bndrs forall_vis_flag ctypedoc
+                                         {% let (fv_ann, fv_flag) = $3 in
+                                            hintExplicitForall $1 *>
                                             ams (sLL $1 $> $
-                                                 HsForAllTy { hst_bndrs = $2
+                                                 HsForAllTy { hst_fvf = fv_flag
+                                                            , hst_bndrs = $2
                                                             , hst_xforall = noExt
                                                             , hst_body = $4 })
-                                                [mu AnnForall $1,mj AnnDot $3] }
+                                                [mu AnnForall $1,fv_ann] }
         | context '=>' ctypedoc       {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2)
                                          >> return (sLL $1 $> $
                                             HsQualTy { hst_ctxt = $1
diff --git a/compiler/parser/RdrHsSyn.hs b/compiler/parser/RdrHsSyn.hs
index 0c3ed74c3b..480b7307dc 100644
--- a/compiler/parser/RdrHsSyn.hs
+++ b/compiler/parser/RdrHsSyn.hs
@@ -692,7 +692,7 @@ mkGadtDecl names ty
     , anns1 ++ anns2)
   where
     (ty'@(dL->L l _),anns1) = peel_parens ty []
-    (tvs, rho) = splitLHsForAllTy ty'
+    (tvs, rho) = splitLHsForAllTyInvis ty'
     (mcxt, tau, anns2) = split_rho rho []
 
     split_rho (dL->L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau })) ann
diff --git a/compiler/prelude/THNames.hs b/compiler/prelude/THNames.hs
index 40ef6a4062..140b3df6f8 100644
--- a/compiler/prelude/THNames.hs
+++ b/compiler/prelude/THNames.hs
@@ -96,9 +96,9 @@ templateHaskellNames = [
     -- PatSynArgs (for pattern synonyms)
     prefixPatSynName, infixPatSynName, recordPatSynName,
     -- Type
-    forallTName, varTName, conTName, infixTName, appTName, appKindTName,
-    equalityTName, tupleTName, unboxedTupleTName, unboxedSumTName,
-    arrowTName, listTName, sigTName, litTName,
+    forallTName, forallVisTName, varTName, conTName, infixTName, appTName,
+    appKindTName, equalityTName, tupleTName, unboxedTupleTName,
+    unboxedSumTName, arrowTName, listTName, sigTName, litTName,
     promotedTName, promotedTupleTName, promotedNilTName, promotedConsTName,
     wildCardTName, implicitParamTName,
     -- TyLit
@@ -429,12 +429,13 @@ infixPatSynName  = libFun (fsLit "infixPatSyn")  infixPatSynIdKey
 recordPatSynName = libFun (fsLit "recordPatSyn") recordPatSynIdKey
 
 -- data Type = ...
-forallTName, varTName, conTName, infixTName, tupleTName, unboxedTupleTName,
-    unboxedSumTName, arrowTName, listTName, appTName, appKindTName,
-    sigTName, equalityTName, litTName, promotedTName,
+forallTName, forallVisTName, varTName, conTName, infixTName, tupleTName,
+    unboxedTupleTName, unboxedSumTName, arrowTName, listTName, appTName,
+    appKindTName, sigTName, equalityTName, litTName, promotedTName,
     promotedTupleTName, promotedNilTName, promotedConsTName,
     wildCardTName, implicitParamTName :: Name
 forallTName         = libFun (fsLit "forallT")        forallTIdKey
+forallVisTName      = libFun (fsLit "forallVisT")     forallVisTIdKey
 varTName            = libFun (fsLit "varT")           varTIdKey
 conTName            = libFun (fsLit "conT")           conTIdKey
 tupleTName          = libFun (fsLit "tupleT")         tupleTIdKey
@@ -950,79 +951,80 @@ infixPatSynIdKey  = mkPreludeMiscIdUnique 381
 recordPatSynIdKey = mkPreludeMiscIdUnique 382
 
 -- data Type = ...
-forallTIdKey, varTIdKey, conTIdKey, tupleTIdKey, unboxedTupleTIdKey,
-    unboxedSumTIdKey, arrowTIdKey, listTIdKey, appTIdKey, appKindTIdKey,
-    sigTIdKey, equalityTIdKey, litTIdKey, promotedTIdKey,
+forallTIdKey, forallVisTIdKey, varTIdKey, conTIdKey, tupleTIdKey,
+    unboxedTupleTIdKey, unboxedSumTIdKey, arrowTIdKey, listTIdKey, appTIdKey,
+    appKindTIdKey, sigTIdKey, equalityTIdKey, litTIdKey, promotedTIdKey,
     promotedTupleTIdKey, promotedNilTIdKey, promotedConsTIdKey,
     wildCardTIdKey, implicitParamTIdKey, infixTIdKey :: Unique
 forallTIdKey        = mkPreludeMiscIdUnique 390
-varTIdKey           = mkPreludeMiscIdUnique 391
-conTIdKey           = mkPreludeMiscIdUnique 392
-tupleTIdKey         = mkPreludeMiscIdUnique 393
-unboxedTupleTIdKey  = mkPreludeMiscIdUnique 394
-unboxedSumTIdKey    = mkPreludeMiscIdUnique 395
-arrowTIdKey         = mkPreludeMiscIdUnique 396
-listTIdKey          = mkPreludeMiscIdUnique 397
-appTIdKey           = mkPreludeMiscIdUnique 398
-appKindTIdKey       = mkPreludeMiscIdUnique 399
-sigTIdKey           = mkPreludeMiscIdUnique 400
-equalityTIdKey      = mkPreludeMiscIdUnique 401
-litTIdKey           = mkPreludeMiscIdUnique 402
-promotedTIdKey      = mkPreludeMiscIdUnique 403
-promotedTupleTIdKey = mkPreludeMiscIdUnique 404
-promotedNilTIdKey   = mkPreludeMiscIdUnique 405
-promotedConsTIdKey  = mkPreludeMiscIdUnique 406
-wildCardTIdKey      = mkPreludeMiscIdUnique 407
-implicitParamTIdKey = mkPreludeMiscIdUnique 408
-infixTIdKey         = mkPreludeMiscIdUnique 409
+forallVisTIdKey     = mkPreludeMiscIdUnique 391
+varTIdKey           = mkPreludeMiscIdUnique 392
+conTIdKey           = mkPreludeMiscIdUnique 393
+tupleTIdKey         = mkPreludeMiscIdUnique 394
+unboxedTupleTIdKey  = mkPreludeMiscIdUnique 395
+unboxedSumTIdKey    = mkPreludeMiscIdUnique 396
+arrowTIdKey         = mkPreludeMiscIdUnique 397
+listTIdKey          = mkPreludeMiscIdUnique 398
+appTIdKey           = mkPreludeMiscIdUnique 399
+appKindTIdKey       = mkPreludeMiscIdUnique 400
+sigTIdKey           = mkPreludeMiscIdUnique 401
+equalityTIdKey      = mkPreludeMiscIdUnique 402
+litTIdKey           = mkPreludeMiscIdUnique 403
+promotedTIdKey      = mkPreludeMiscIdUnique 404
+promotedTupleTIdKey = mkPreludeMiscIdUnique 405
+promotedNilTIdKey   = mkPreludeMiscIdUnique 406
+promotedConsTIdKey  = mkPreludeMiscIdUnique 407
+wildCardTIdKey      = mkPreludeMiscIdUnique 408
+implicitParamTIdKey = mkPreludeMiscIdUnique 409
+infixTIdKey         = mkPreludeMiscIdUnique 410
 
 -- data TyLit = ...
 numTyLitIdKey, strTyLitIdKey :: Unique
-numTyLitIdKey = mkPreludeMiscIdUnique 410
-strTyLitIdKey = mkPreludeMiscIdUnique 411
+numTyLitIdKey = mkPreludeMiscIdUnique 411
+strTyLitIdKey = mkPreludeMiscIdUnique 412
 
 -- data TyVarBndr = ...
 plainTVIdKey, kindedTVIdKey :: Unique
-plainTVIdKey       = mkPreludeMiscIdUnique 412
-kindedTVIdKey      = mkPreludeMiscIdUnique 413
+plainTVIdKey       = mkPreludeMiscIdUnique 413
+kindedTVIdKey      = mkPreludeMiscIdUnique 414
 
 -- data Role = ...
 nominalRIdKey, representationalRIdKey, phantomRIdKey, inferRIdKey :: Unique
-nominalRIdKey          = mkPreludeMiscIdUnique 414
-representationalRIdKey = mkPreludeMiscIdUnique 415
-phantomRIdKey          = mkPreludeMiscIdUnique 416
-inferRIdKey            = mkPreludeMiscIdUnique 417
+nominalRIdKey          = mkPreludeMiscIdUnique 415
+representationalRIdKey = mkPreludeMiscIdUnique 416
+phantomRIdKey          = mkPreludeMiscIdUnique 417
+inferRIdKey            = mkPreludeMiscIdUnique 418
 
 -- data Kind = ...
 varKIdKey, conKIdKey, tupleKIdKey, arrowKIdKey, listKIdKey, appKIdKey,
   starKIdKey, constraintKIdKey :: Unique
-varKIdKey         = mkPreludeMiscIdUnique 418
-conKIdKey         = mkPreludeMiscIdUnique 419
-tupleKIdKey       = mkPreludeMiscIdUnique 420
-arrowKIdKey       = mkPreludeMiscIdUnique 421
-listKIdKey        = mkPreludeMiscIdUnique 422
-appKIdKey         = mkPreludeMiscIdUnique 423
-starKIdKey        = mkPreludeMiscIdUnique 424
-constraintKIdKey  = mkPreludeMiscIdUnique 425
+varKIdKey         = mkPreludeMiscIdUnique 419
+conKIdKey         = mkPreludeMiscIdUnique 420
+tupleKIdKey       = mkPreludeMiscIdUnique 421
+arrowKIdKey       = mkPreludeMiscIdUnique 422
+listKIdKey        = mkPreludeMiscIdUnique 423
+appKIdKey         = mkPreludeMiscIdUnique 424
+starKIdKey        = mkPreludeMiscIdUnique 425
+constraintKIdKey  = mkPreludeMiscIdUnique 426
 
 -- data FamilyResultSig = ...
 noSigIdKey, kindSigIdKey, tyVarSigIdKey :: Unique
-noSigIdKey        = mkPreludeMiscIdUnique 426
-kindSigIdKey      = mkPreludeMiscIdUnique 427
-tyVarSigIdKey     = mkPreludeMiscIdUnique 428
+noSigIdKey        = mkPreludeMiscIdUnique 427
+kindSigIdKey      = mkPreludeMiscIdUnique 428
+tyVarSigIdKey     = mkPreludeMiscIdUnique 429
 
 -- data InjectivityAnn = ...
 injectivityAnnIdKey :: Unique
-injectivityAnnIdKey = mkPreludeMiscIdUnique 429
+injectivityAnnIdKey = mkPreludeMiscIdUnique 430
 
 -- data Callconv = ...
 cCallIdKey, stdCallIdKey, cApiCallIdKey, primCallIdKey,
   javaScriptCallIdKey :: Unique
-cCallIdKey          = mkPreludeMiscIdUnique 430
-stdCallIdKey        = mkPreludeMiscIdUnique 431
-cApiCallIdKey       = mkPreludeMiscIdUnique 432
-primCallIdKey       = mkPreludeMiscIdUnique 433
-javaScriptCallIdKey = mkPreludeMiscIdUnique 434
+cCallIdKey          = mkPreludeMiscIdUnique 431
+stdCallIdKey        = mkPreludeMiscIdUnique 432
+cApiCallIdKey       = mkPreludeMiscIdUnique 433
+primCallIdKey       = mkPreludeMiscIdUnique 434
+javaScriptCallIdKey = mkPreludeMiscIdUnique 435
 
 -- data Safety = ...
 unsafeIdKey, safeIdKey, interruptibleIdKey :: Unique
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index 4e7cd84276..aaeb902754 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -154,7 +154,6 @@ import NameSet          ( NameSet, mkNameSet, elemNameSet )
 import BasicTypes       ( Arity, Boxity(..), TupleSort(..), ConTagZ,
                           SourceText(..) )
 import ForeignCall
-import Var              ( AnonArgFlag(..) )
 import SrcLoc           ( noSrcSpan )
 import Unique
 import Data.Array
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 499fd74bd9..b84bbe3bae 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -170,11 +170,13 @@ 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 hs_ty@(HsForAllTy { hst_bndrs = tvs, hst_body = hs_body })
+    rn_ty env hs_ty@(HsForAllTy { hst_fvf = fvf, hst_bndrs = tvs
+                                , hst_body = hs_body })
       = bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc hs_ty) Nothing tvs $ \ tvs' ->
         do { (hs_body', fvs) <- rn_lty env hs_body
-           ; return (HsForAllTy { hst_xforall = noExt, hst_bndrs = tvs'
-                                , hst_body = hs_body' }, fvs) }
+           ; return (HsForAllTy { hst_fvf = fvf, hst_xforall = noExt
+                                , hst_bndrs = tvs', hst_body = hs_body' }
+                    , fvs) }
 
     rn_ty env (HsQualTy { hst_ctxt = dL->L cx hs_ctxt
                         , hst_body = hs_ty })
@@ -479,13 +481,14 @@ rnLHsTyKi env (dL->L loc ty)
 
 rnHsTyKi :: RnTyKiEnv -> HsType GhcPs -> RnM (HsType GhcRn, FreeVars)
 
-rnHsTyKi env ty@(HsForAllTy { hst_bndrs = tyvars, hst_body  = tau })
+rnHsTyKi env ty@(HsForAllTy { hst_fvf = fvf, hst_bndrs = tyvars
+                            , hst_body = tau })
   = do { checkPolyKinds env ty
        ; bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc ty)
                            Nothing tyvars $ \ tyvars' ->
     do { (tau',  fvs) <- rnLHsTyKi env tau
-       ; return ( HsForAllTy { hst_xforall = noExt, hst_bndrs = tyvars'
-                             , hst_body =  tau' }
+       ; return ( HsForAllTy { hst_fvf = fvf, hst_xforall = noExt
+                             , hst_bndrs = tyvars' , hst_body =  tau' }
                 , fvs) } }
 
 rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 6078a7a7ff..4736ded2f2 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -725,7 +725,8 @@ tcStandaloneDerivInstType ctxt
                   HsIB { hsib_ext = vars
                        , hsib_body
                            = L (getLoc deriv_ty_body) $
-                             HsForAllTy { hst_bndrs = tvs
+                             HsForAllTy { hst_fvf = ForallInvis
+                                        , hst_bndrs = tvs
                                         , hst_xforall = noExt
                                         , hst_body  = rho }}
        let (tvs, _theta, cls, inst_tys) = tcSplitDFunTy dfun_ty
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index ef038e119b..24b416c6e8 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -666,14 +666,18 @@ 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_bndrs = hs_tvs, hst_body = ty }) exp_kind
+tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
+                                   , hst_body = ty }) exp_kind
   = do { (tclvl, wanted, (tvs', ty'))
             <- pushLevelAndCaptureConstraints $
                bindExplicitTKBndrs_Skol hs_tvs $
                tc_lhs_type mode ty exp_kind
     -- Do not kind-generalise here!  See Note [Kind generalisation]
     -- Why exp_kind?  See Note [Body kind of HsForAllTy]
-       ; let bndrs       = mkTyVarBinders Specified tvs'
+       ; let argf        = case fvf of
+                             ForallVis   -> Required
+                             ForallInvis -> Specified
+             bndrs       = mkTyVarBinders argf tvs'
              skol_info   = ForAllSkol (ppr forall)
              m_telescope = Just (sep (map ppr hs_tvs))
 
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 76d1510aa3..fcac5cb33d 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2311,7 +2311,8 @@ getGhciStepIO = do
         ioM     = nlHsAppTy (nlHsTyVar ioTyConName) (nlHsTyVar a_tv)
 
         step_ty = noLoc $ HsForAllTy
-                     { hst_bndrs = [noLoc $ UserTyVar noExt (noLoc a_tv)]
+                     { hst_fvf = ForallInvis
+                     , hst_bndrs = [noLoc $ UserTyVar noExt (noLoc a_tv)]
                      , hst_xforall = noExt
                      , hst_body  = nlHsFunTy ghciM ioM }
 
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 027a4013ab..17e3f54893 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -366,8 +366,8 @@ tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
 tcPatSynSig name sig_ty
   | HsIB { hsib_ext = implicit_hs_tvs
          , hsib_body = hs_ty }  <- sig_ty
-  , (univ_hs_tvs, hs_req,  hs_ty1)     <- splitLHsSigmaTy hs_ty
-  , (ex_hs_tvs,   hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1
+  , (univ_hs_tvs, hs_req,  hs_ty1)     <- splitLHsSigmaTyInvis hs_ty
+  , (ex_hs_tvs,   hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
   = do {  traceTc "tcPatSynSig 1" (ppr sig_ty)
        ; (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
            <- pushTcLevelM_   $
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 631c777ab7..1aba34e802 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1814,7 +1814,8 @@ reifyType :: TyCoRep.Type -> TcM TH.Type
 reifyType ty                | tcIsLiftedTypeKind ty = return TH.StarT
   -- Make sure to use tcIsLiftedTypeKind here, since we don't want to confuse it
   -- with Constraint (#14869).
-reifyType ty@(ForAllTy {})  = reify_for_all ty
+reifyType ty@(ForAllTy (Bndr _ argf) _)
+                            = reify_for_all argf ty
 reifyType (LitTy t)         = do { r <- reifyTyLit t; return (TH.LitT r) }
 reifyType (TyVarTy tv)      = return (TH.VarT (reifyName tv))
 reifyType (TyConApp tc tys) = reify_tc_app tc tys   -- Do not expand type synonyms here
@@ -1836,19 +1837,24 @@ reifyType ty@(AppTy {})     = do
       filterByList (map isVisibleArgFlag $ appTyArgFlags ty_head ty_args)
                    ty_args
 reifyType ty@(FunTy { ft_af = af, ft_arg = t1, ft_res = t2 })
-  | InvisArg <- af = reify_for_all ty  -- Types like ((?x::Int) => Char -> Char)
+  | InvisArg <- af = reify_for_all Inferred ty  -- Types like ((?x::Int) => Char -> Char)
   | otherwise      = do { [r1,r2] <- reifyTypes [t1,t2] ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) }
 reifyType (CastTy t _)      = reifyType t -- Casts are ignored in TH
 reifyType ty@(CoercionTy {})= noTH (sLit "coercions in types") (ppr ty)
 
-reify_for_all :: TyCoRep.Type -> TcM TH.Type
-reify_for_all ty
-  = do { cxt' <- reifyCxt cxt;
-       ; tau' <- reifyType tau
-       ; tvs' <- reifyTyVars tvs
-       ; return (TH.ForallT tvs' cxt' tau') }
+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
+  tvs' <- reifyTyVars tvs
+  case argToForallVisFlag argf of
+    ForallVis   -> do phi' <- reifyType phi
+                      pure $ TH.ForallVisT tvs' phi'
+    ForallInvis -> do let (cxt, tau) = tcSplitPhiTy phi
+                      cxt' <- reifyCxt cxt
+                      tau' <- reifyType tau
+                      pure $ TH.ForallT tvs' cxt' tau'
   where
-    (tvs, cxt, tau) = tcSplitSigmaTy ty
+    (tvs, phi) = tcSplitForAllTysSameVis argf ty
 
 reifyTyLit :: TyCoRep.TyLit -> TcM TH.TyLit
 reifyTyLit (NumTyLit n) = return (TH.NumTyLit n)
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 1f6372cd0a..155037b775 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -59,7 +59,8 @@ module TcType (
   -- These are important because they do not look through newtypes
   getTyVar,
   tcSplitForAllTy_maybe,
-  tcSplitForAllTys, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs,
+  tcSplitForAllTys, tcSplitForAllTysSameVis,
+  tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs,
   tcSplitPhiTy, tcSplitPredFunTy_maybe,
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
   tcSplitFunTysN,
@@ -128,7 +129,8 @@ module TcType (
 
   --------------------------------
   -- Rexported from Type
-  Type, PredType, ThetaType, TyCoBinder, ArgFlag(..), AnonArgFlag(..),
+  Type, PredType, ThetaType, TyCoBinder,
+  ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
 
   mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys, mkTyCoInvForAllTy,
   mkInvForAllTy, mkInvForAllTys,
@@ -1354,6 +1356,14 @@ 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.
+tcSplitForAllTysSameVis :: ArgFlag -> Type -> ([TyVar], Type)
+tcSplitForAllTysSameVis supplied_argf ty = ASSERT( all isTyVar (fst sty) ) sty
+  where sty = splitForAllTysSameVis supplied_argf ty
+
 -- | Like 'tcSplitForAllTys', but splits off only named binders.
 tcSplitForAllVarBndrs :: Type -> ([TyVarBinder], Type)
 tcSplitForAllVarBndrs ty = ASSERT( all isTyVarBinder (fst sty)) sty
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 8ab63f49cc..d17ac0f567 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -464,6 +464,55 @@ allConstraintsAllowed (TySynKindCtxt {})     = False
 allConstraintsAllowed (TyFamResKindCtxt {})  = False
 allConstraintsAllowed _ = True
 
+-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
+-- context for the type of a term, where visible, dependent quantification is
+-- currently disallowed.
+--
+-- An example of something that is unambiguously the type of a term is the
+-- @forall a -> a -> a@ in @foo :: forall a -> a -> a@. On the other hand, the
+-- same type in @type family Foo :: forall a -> a -> a@ is unambiguously the
+-- kind of a type, not the type of a term, so it is permitted.
+--
+-- For more examples, see
+-- @testsuite/tests/dependent/should_compile/T16326_Compile*.hs@ (for places
+-- where VDQ is permitted) and
+-- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where
+-- VDQ is disallowed).
+vdqAllowed :: UserTypeCtxt -> Bool
+-- Currently allowed in the kinds of types...
+vdqAllowed (KindSigCtxt {}) = True
+vdqAllowed (TySynCtxt {}) = True
+vdqAllowed (ThBrackCtxt {}) = True
+vdqAllowed (GhciCtxt {}) = True
+vdqAllowed (TyVarBndrKindCtxt {}) = True
+vdqAllowed (DataKindCtxt {}) = True
+vdqAllowed (TySynKindCtxt {}) = True
+vdqAllowed (TyFamResKindCtxt {}) = True
+-- ...but not in the types of terms.
+vdqAllowed (ConArgCtxt {}) = False
+  -- We could envision allowing VDQ in data constructor types so long as the
+  -- constructor is only ever used at the type level, but for now, GHC adopts
+  -- the stance that VDQ is never allowed in data constructor types.
+vdqAllowed (FunSigCtxt {}) = False
+vdqAllowed (InfSigCtxt {}) = False
+vdqAllowed (ExprSigCtxt {}) = False
+vdqAllowed (TypeAppCtxt {}) = False
+vdqAllowed (PatSynCtxt {}) = False
+vdqAllowed (PatSigCtxt {}) = False
+vdqAllowed (RuleSigCtxt {}) = False
+vdqAllowed (ResSigCtxt {}) = False
+vdqAllowed (ForSigCtxt {}) = False
+vdqAllowed (DefaultDeclCtxt {}) = False
+-- We count class constraints as "types of terms". All of the cases below deal
+-- with class constraints.
+vdqAllowed (InstDeclCtxt {}) = False
+vdqAllowed (SpecInstCtxt {}) = False
+vdqAllowed (GenSigCtxt {}) = False
+vdqAllowed (ClassSCCtxt {}) = False
+vdqAllowed (SigmaCtxt {}) = False
+vdqAllowed (DataTyCtxt {}) = False
+vdqAllowed (DerivClauseCtxt {}) = False
+
 {-
 Note [Correctness and performance of type synonym validity checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -615,9 +664,8 @@ check_type ve (CastTy ty _) = check_type ve ty
 --
 -- Critically, this case must come *after* the case for TyConApp.
 -- See Note [Liberal type synonyms].
-check_type ve@(ValidityEnv{ ve_tidy_env = env
-                          , ve_rank = rank
-                          , ve_expand = expand }) ty
+check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
+                          , ve_rank = rank, ve_expand = expand }) ty
   | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
         ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
@@ -628,6 +676,12 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env
                 -- Reject forall (a :: Eq b => b). blah
                 -- In a kind signature we don't allow constraints
 
+        ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs
+                         || vdqAllowed ctxt)
+                   (illegalVDQTyErr env ty)
+                -- Reject visible, dependent quantification in the type of a
+                -- term (e.g., `f :: forall a -> a -> Maybe a`)
+
         ; check_valid_theta env' SigmaCtxt expand theta
                 -- Allow     type T = ?x::Int => Int -> Int
                 -- but not   type T = ?x::Int
@@ -851,6 +905,15 @@ constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
 constraintTyErr env ty
   = (env, text "Illegal constraint in a kind:" <+> ppr_tidy env ty)
 
+-- | Reject a use of visible, dependent quantification in the type of a term.
+illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
+illegalVDQTyErr env ty =
+  (env, vcat
+  [ hang (text "Illegal visible, dependent quantification" <+>
+          text "in the type of a term:")
+       2 (ppr_tidy env ty)
+  , text "(GHC does not yet support this)" ] )
+
 {-
 Note [Liberal type synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 3594c7a3a3..86f72b88f2 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -32,7 +32,7 @@ module TyCoRep (
         KindOrType, Kind,
         KnotTied,
         PredType, ThetaType,      -- Synonyms
-        ArgFlag(..), AnonArgFlag(..),
+        ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
 
         -- * Coercions
         Coercion(..),
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 473e9e5ef8..7ff5bb4c84 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -14,7 +14,7 @@ module Type (
         -- $type_classification
 
         -- $representation_types
-        TyThing(..), Type, ArgFlag(..), AnonArgFlag,
+        TyThing(..), Type, ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
         KindOrType, PredType, ThetaType,
         Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder,
         KnotTied,
@@ -42,7 +42,7 @@ module Type (
         mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInvForAllTy, mkInvForAllTys,
-        splitForAllTys, splitForAllVarBndrs,
+        splitForAllTys, splitForAllTysSameVis, splitForAllVarBndrs,
         splitForAllTy_maybe, splitForAllTy,
         splitForAllTy_ty_maybe, splitForAllTy_co_maybe,
         splitPiTy_maybe, splitPiTy, splitPiTys,
@@ -1455,6 +1455,18 @@ 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.
+splitForAllTysSameVis :: ArgFlag -> Type -> ([TyCoVar], Type)
+splitForAllTysSameVis supplied_argf 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 (tv:tvs)
+    split orig_ty _                            tvs = (reverse tvs, orig_ty)
+
 -- | 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/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst
index cfe07deb81..cd865e257f 100644
--- a/docs/users_guide/8.10.1-notes.rst
+++ b/docs/users_guide/8.10.1-notes.rst
@@ -44,6 +44,16 @@ Language
     type T = Just (Nothing :: Maybe a)         -- no longer accepted
     type T = Just Nothing :: Maybe (Maybe a)   -- still accepted
 
+- GHC now parses visible, dependent quantifiers (as proposed in
+  `GHC proposal 35
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst>`__),
+  such as the following: ::
+
+    data Proxy :: forall k -> k -> Type
+
+  See the `section on explicit kind quantification
+  <#explicit-kind-quantification>`__ for more details.
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 9ba8fa2daf..67be116ae4 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9170,6 +9170,8 @@ GHC reports an error, saying that the kind of ``a`` should be a kind variable
 restricted to be ``Type``. The function definition is then rejected for being
 more specific than its type signature.
 
+.. _explicit-kind-quantification:
+
 Explicit kind quantification
 ----------------------------
 
@@ -9253,6 +9255,53 @@ Closed type family instances are subject to the same rules: ::
   type family F :: Maybe (Maybe k) where
     F @k = 'Just ('Nothing :: Maybe k) -- accepted
 
+Kind variables can also be quantified in *visible* positions. Consider the
+following two examples: ::
+
+  data ProxyKInvis (a :: k)
+  data ProxyKVis k (a :: k)
+
+In the first example, the kind variable ``k`` is an *invisible* argument to
+``ProxyKInvis``. In other words, a user does not need to instantiate ``k``
+explicitly, as kind inference automatically determines what ``k`` should be.
+For instance, in ``ProxyKInvis True``, ``k`` is inferred to be ``Bool``.
+This is reflected in the kind of ``ProxyKInvis``: ::
+
+  ProxyKInvis :: forall k. k -> Type
+
+In the second example, ``k`` is a *visible* argument to ``ProxyKVis``. That is
+to say, ``k`` is an argument that users must provide explicitly when applying
+``ProxyKVis``. For example, ``ProxyKVis Bool True`` is a well formed type.
+
+What is the kind of ``ProxyKVis``? One might say
+``forall k. Type -> k -> Type``, but this isn't quite right, since this would
+allow incorrect things like ``ProxyKVis Bool Int``, which should be rejected
+due to the fact that ``Int`` is not of kind ``Bool``. The key observation is that
+the kind of the second argument *depend* on the first argument. GHC indicates
+this dependency in the syntax that it gives for the kind of ``ProxyKVis``: ::
+
+  ProxyKVis :: forall k -> k -> Type
+
+This kind is similar to the kind of ``ProxyKInvis``, but with a key difference:
+the type variables quantified by the ``forall`` are followed by an arrow
+(``->``), not a dot (``.``). This is a visible, dependent quantifier. It is
+visible in that it the user must pass in a type for ``k`` explicitly, and it is
+dependent in the sense that ``k`` appears later in the kind of ``ProxyKVis``.
+As a counterpart, the ``k`` binder in ``forall k. k -> Type`` can be thought
+of as an *invisible*, dependent quantifier.
+
+GHC permits writing kinds with this syntax, provided that the
+``ExplicitForAll`` and ``PolyKinds`` language extensions are enabled. Just
+like the invisible ``forall``, one can put explicit kind signatures on visibly
+bound kind variables, so the following is syntactically valid: ::
+
+  ProxyKVis :: forall (k :: Type) -> k -> Type
+
+Currently, the ability to write visible, dependent quantifiers is limited to
+kinds. Consequently, visible dependent quantifiers are rejected in any context
+that is unambiguously the type of a term. They are also rejected in the types
+of data constructors.
+
 Kind-indexed GADTs
 ------------------
 
diff --git a/docs/users_guide/index.rst b/docs/users_guide/index.rst
index c20aec7e56..c886722859 100644
--- a/docs/users_guide/index.rst
+++ b/docs/users_guide/index.rst
@@ -14,6 +14,7 @@ Contents:
    intro
    8.6.1-notes
    8.8.1-notes
+   8.10.1-notes
    ghci
    runghc
    usage
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib.hs b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
index 60527b6c82..69a40428b8 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
@@ -52,10 +52,10 @@ module Language.Haskell.TH.Lib (
     bindS, letS, noBindS, parS, recS,
 
     -- *** Types
-        forallT, varT, conT, appT, appKindT, arrowT, infixT, uInfixT, parensT,
-        equalityT, listT, tupleT, unboxedTupleT, unboxedSumT, sigT, litT,
-        wildCardT, promotedT, promotedTupleT, promotedNilT, promotedConsT,
-        implicitParamT,
+        forallT, forallVisT, varT, conT, appT, appKindT, arrowT, infixT,
+        uInfixT, parensT, equalityT, listT, tupleT, unboxedTupleT, unboxedSumT,
+        sigT, litT, wildCardT, promotedT, promotedTupleT, promotedNilT,
+        promotedConsT, implicitParamT,
     -- **** Type literals
     numTyLit, strTyLit,
     -- **** Strictness
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
index ec9ca4fafb..14ef0a02a8 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
@@ -646,6 +646,9 @@ forallT tvars ctxt ty = do
     ty1    <- ty
     return $ ForallT tvars1 ctxt1 ty1
 
+forallVisT :: [TyVarBndrQ] -> TypeQ -> TypeQ
+forallVisT tvars ty = ForallVisT <$> sequenceA tvars <*> ty
+
 varT :: Name -> TypeQ
 varT = return . VarT
 
diff --git a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
index c25b2fb702..fa00c8c537 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
@@ -647,12 +647,23 @@ commaSepApplied :: [Name] -> Doc
 commaSepApplied = commaSepWith (pprName' Applied)
 
 pprForall :: [TyVarBndr] -> Cxt -> Doc
-pprForall tvs cxt
+pprForall = pprForall' ForallInvis
+
+pprForallVis :: [TyVarBndr] -> Cxt -> Doc
+pprForallVis = pprForall' ForallVis
+
+pprForall' :: ForallVisFlag -> [TyVarBndr] -> Cxt -> Doc
+pprForall' fvf tvs cxt
   -- even in the case without any tvs, there could be a non-empty
   -- context cxt (e.g., in the case of pattern synonyms, where there
   -- are multiple forall binders and contexts).
   | [] <- tvs = pprCxt cxt
-  | otherwise = text "forall" <+> hsep (map ppr tvs) <+> char '.' <+> pprCxt cxt
+  | otherwise = text "forall" <+> hsep (map ppr tvs)
+                              <+> separator <+> pprCxt cxt
+  where
+    separator = case fvf of
+                  ForallVis   -> text "->"
+                  ForallInvis -> char '.'
 
 pprRecFields :: [(Name, Strict, Type)] -> Type -> Doc
 pprRecFields vsts ty
@@ -750,6 +761,7 @@ pprParendType tuple | (TupleT n, args) <- split tuple
 pprParendType (ImplicitParamT n t)= text ('?':n) <+> text "::" <+> ppr t
 pprParendType EqualityT           = text "(~)"
 pprParendType t@(ForallT {})      = parens (ppr t)
+pprParendType t@(ForallVisT {})   = parens (ppr t)
 pprParendType t@(AppT {})         = parens (ppr t)
 pprParendType t@(AppKindT {})     = parens (ppr t)
 
@@ -759,6 +771,7 @@ pprUInfixT t               = ppr t
 
 instance Ppr Type where
     ppr (ForallT tvars ctxt ty) = sep [pprForall tvars ctxt, ppr ty]
+    ppr (ForallVisT tvars ty)   = sep [pprForallVis tvars [], ppr ty]
     ppr ty = pprTyApp (split ty)
        -- Works, in a degnerate way, for SigT, and puts parens round (ty :: kind)
        -- See Note [Pretty-printing kind signatures]
@@ -791,10 +804,15 @@ pprTyApp (fun, args) = pprParendType fun <+> sep (map pprParendTypeArg args)
 pprFunArgType :: Type -> Doc    -- Should really use a precedence argument
 -- Everything except forall and (->) binds more tightly than (->)
 pprFunArgType ty@(ForallT {})                 = parens (ppr ty)
+pprFunArgType ty@(ForallVisT {})              = parens (ppr ty)
 pprFunArgType ty@((ArrowT `AppT` _) `AppT` _) = parens (ppr ty)
 pprFunArgType ty@(SigT _ _)                   = parens (ppr ty)
 pprFunArgType ty                              = ppr ty
 
+data ForallVisFlag = ForallVis   -- forall a -> {...}
+                   | ForallInvis -- forall a.   {...}
+  deriving Show
+
 data TypeArg = TANormal Type
              | TyArg Kind
 
diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
index 7bff489650..22c6cd1def 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
@@ -2099,6 +2099,7 @@ data PatSynArgs
   deriving( Show, Eq, Ord, Data, Generic )
 
 data Type = ForallT [TyVarBndr] Cxt Type  -- ^ @forall \<vars\>. \<ctxt\> => \<type\>@
+          | ForallVisT [TyVarBndr] Type   -- ^ @forall \<vars\> -> \<type\>@
           | AppT Type Type                -- ^ @T a b@
           | AppKindT Type Kind            -- ^ @T \@k t@
           | SigT Type Kind                -- ^ @t :: k@
diff --git a/libraries/template-haskell/changelog.md b/libraries/template-haskell/changelog.md
index cfed120471..a64795b5b9 100644
--- a/libraries/template-haskell/changelog.md
+++ b/libraries/template-haskell/changelog.md
@@ -5,6 +5,9 @@
   * Introduce a `liftTyped` method to the `Lift` class and set the default
     implementations of `lift`/`liftTyped` to be in terms of each other.
 
+  * Add a `ForallVisT` constructor to `Type` to represent visible, dependent
+    quantification.
+
 ## 2.15.0.0 *TBA*
 
   * In `Language.Haskell.TH.Syntax`, `DataInstD`, `NewTypeInstD`, `TySynEqn`,
diff --git a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
new file mode 100644
index 0000000000..109b18e9f7
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module T16326_Compile1 where
+
+import Data.Kind
+
+type DApply a (b :: a -> Type) (f :: forall (x :: a) -> b x) (x :: a) =
+  f x
+
+type DComp a
+           (b :: a -> Type)
+           (c :: forall (x :: a). b x -> Type)
+           (f :: forall (x :: a). forall (y :: b x) -> c y)
+           (g :: forall (x :: a) -> b x)
+           (x :: a) =
+  f (g x)
+
+type family ElimList a
+                     (p :: [a] -> Type)
+                     (s :: [a])
+                     (pNil :: p '[])
+                     (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs))
+                  :: p s where
+  forall a p pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)).
+    ElimList a p '[] pNil pCons =
+      pNil
+  forall a p x xs pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)).
+    ElimList a p (x:xs) pNil pCons =
+      pCons x xs (ElimList a p xs pNil pCons)
+
+data Proxy' :: forall k -> k -> Type where
+  MkProxy' :: forall k (a :: k). Proxy' k a
+
+type family Proxy2' ∷ ∀ k → k → Type where
+  Proxy2' = Proxy'
diff --git a/testsuite/tests/dependent/should_compile/T16326_Compile2.hs b/testsuite/tests/dependent/should_compile/T16326_Compile2.hs
new file mode 100644
index 0000000000..ac528e28d1
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T16326_Compile2.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16326_Compile2 where
+
+import Data.Kind
+
+type family Wat :: forall a. a
+type Lol = Wat @(forall a -> a) (forall a -> a) (forall a. a) @(forall a. a)
+               Type Bool
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index ca5f436174..e630f1a90a 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -65,3 +65,5 @@ test('T15076c', normal, compile, [''])
 test('T15829', normal, compile, [''])
 test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions'])
 test('T14729kind', normal, ghci_script, ['T14729kind.script'])
+test('T16326_Compile1', normal, compile, [''])
+test('T16326_Compile2', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/T15859.stderr b/testsuite/tests/dependent/should_fail/T15859.stderr
index c4dc1ef086..ec0e091055 100644
--- a/testsuite/tests/dependent/should_fail/T15859.stderr
+++ b/testsuite/tests/dependent/should_fail/T15859.stderr
@@ -1,6 +1,8 @@
 
-T15859.hs:14:5: error:
-    • Cannot apply expression of type ‘forall k -> k -> *’
-      to a visible type argument ‘Int’
-    • In the expression: (undefined :: KindOf A) @Int
-      In an equation for ‘a’: a = (undefined :: KindOf A) @Int
+T15859.hs:14:19: error:
+    • Illegal visible, dependent quantification in the type of a term:
+      forall k -> k -> *
+      (GHC does not yet support this)
+    • In the expansion of type synonym ‘KindOf’
+      In an expression type signature: KindOf A
+      In the expression: undefined :: KindOf A
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail1.hs b/testsuite/tests/dependent/should_fail/T16326_Fail1.hs
new file mode 100644
index 0000000000..eccbae3deb
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail1.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail1 where
+
+id1 :: forall a -> a -> a
+id1 _ x = x
+
+type Foo = forall a -> a -> a
+id2 :: Foo
+id2 _ x = x
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr
new file mode 100644
index 0000000000..c56bd105db
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail1.stderr
@@ -0,0 +1,13 @@
+
+T16326_Fail1.hs:5:8: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a -> a -> a
+      (GHC does not yet support this)
+    • In the type signature: id1 :: forall a -> a -> a
+
+T16326_Fail1.hs:9:8: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a -> a -> a
+      (GHC does not yet support this)
+    • In the expansion of type synonym ‘Foo’
+      In the type signature: id2 :: Foo
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail10.hs b/testsuite/tests/dependent/should_fail/T16326_Fail10.hs
new file mode 100644
index 0000000000..e9fdb16c64
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail10.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail10 where
+
+import Data.Kind
+
+type Const a b = a
+
+flurmp :: a -> ()
+flurmp _ = ()
+{-# RULES "flurmp"
+    forall (x :: forall a -> a -> a). flurmp x = () #-}
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr
new file mode 100644
index 0000000000..bceccb1dcd
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail10.stderr
@@ -0,0 +1,7 @@
+
+T16326_Fail10.hs:12:18: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a -> a -> a
+      (GHC does not yet support this)
+    • In a RULE for ‘x’: forall a -> a -> a
+      When checking the transformation rule "flurmp"
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail11.hs b/testsuite/tests/dependent/should_fail/T16326_Fail11.hs
new file mode 100644
index 0000000000..2ed92c3675
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail11.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module T16326_Fail11 where
+
+class C a where
+  m :: b -> a
+  default m :: (forall x -> x) ~ b => b -> a
+  m = undefined
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr
new file mode 100644
index 0000000000..396010dbd7
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail11.stderr
@@ -0,0 +1,7 @@
+
+T16326_Fail11.hs:9:11: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall x -> x
+      (GHC does not yet support this)
+    • When checking the class method: m :: forall a b. C a => b -> a
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail12.hs b/testsuite/tests/dependent/should_fail/T16326_Fail12.hs
new file mode 100644
index 0000000000..5db0c2eb3a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail12.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail12 where
+
+class (forall a -> Show a) => C a
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
new file mode 100644
index 0000000000..30b35de4f7
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
@@ -0,0 +1,8 @@
+
+T16326_Fail12.hs:6:1: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a -> Show a
+      (GHC does not yet support this)
+    • In the context: forall a -> Show a
+      While checking the super-classes of class ‘C’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail2.hs b/testsuite/tests/dependent/should_fail/T16326_Fail2.hs
new file mode 100644
index 0000000000..398c0d586e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail2.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE ForeignFunctionInterface #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail2 where
+
+foreign import ccall "blah" blah :: forall a -> a -> IO ()
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr
new file mode 100644
index 0000000000..3e3f0c1128
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail2.stderr
@@ -0,0 +1,8 @@
+
+T16326_Fail2.hs:6:37: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a -> a -> IO ()
+      (GHC does not yet support this)
+    • In the type signature: blah :: forall a -> a -> IO ()
+      When checking declaration:
+        foreign import ccall safe "blah" blah :: forall a -> a -> IO ()
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail3.hs b/testsuite/tests/dependent/should_fail/T16326_Fail3.hs
new file mode 100644
index 0000000000..4d598d6564
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail3.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail3 where
+
+pattern Nil :: forall a -> [a]
+pattern Nil <- undefined
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr
new file mode 100644
index 0000000000..27ed998b45
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail3.stderr
@@ -0,0 +1,5 @@
+
+T16326_Fail3.hs:6:1: error:
+    Illegal visible, dependent quantification in the type of a term:
+      forall a -> [a]
+    (GHC does not yet support this)
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail4.hs b/testsuite/tests/dependent/should_fail/T16326_Fail4.hs
new file mode 100644
index 0000000000..b1ba79dddc
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail4.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail4 where
+
+foo :: Maybe a -> Maybe a -> Maybe a
+foo xs ys = zipWith ((<>) :: forall a -> Maybe a -> Maybe a -> Maybe a) xs ys
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
new file mode 100644
index 0000000000..258fc08607
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
@@ -0,0 +1,11 @@
+
+T16326_Fail4.hs:6:30: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a1 -> Maybe a1 -> Maybe a1 -> Maybe a1
+      (GHC does not yet support this)
+    • In an expression type signature:
+        forall a -> Maybe a -> Maybe a -> Maybe a
+      In the first argument of ‘zipWith’, namely
+        ‘((<>) :: forall a -> Maybe a -> Maybe a -> Maybe a)’
+      In the expression:
+        zipWith ((<>) :: forall a -> Maybe a -> Maybe a -> Maybe a) xs ys
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail5.hs b/testsuite/tests/dependent/should_fail/T16326_Fail5.hs
new file mode 100644
index 0000000000..e5b18181c7
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail5.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module T16326_Fail5 where
+
+isJust :: Maybe a -> Bool
+isJust (Nothing :: forall a -> Maybe a) = False
+isJust (Just _)                         = True
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
new file mode 100644
index 0000000000..59c27c2464
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
@@ -0,0 +1,9 @@
+
+T16326_Fail5.hs:7:20: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a1 -> Maybe a1
+      (GHC does not yet support this)
+    • In a pattern type signature: forall a -> Maybe a
+      In the pattern: Nothing :: forall a -> Maybe a
+      In an equation for ‘isJust’:
+          isJust (Nothing :: forall a -> Maybe a) = False
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail6.hs b/testsuite/tests/dependent/should_fail/T16326_Fail6.hs
new file mode 100644
index 0000000000..75f4f9a674
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail6.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail6 where
+
+import Data.Kind
+
+data Foo :: Type -> Type where
+  MkFoo :: forall a -> a -> Foo a
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
new file mode 100644
index 0000000000..bb78e2f457
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
@@ -0,0 +1,7 @@
+
+T16326_Fail6.hs:9:3: error:
+    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
+      Suggestion: instead use this type signature:
+        MkFoo :: forall a. a -> Foo a
+    • In the definition of data constructor ‘MkFoo’
+      In the data type declaration for ‘Foo’
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail7.hs b/testsuite/tests/dependent/should_fail/T16326_Fail7.hs
new file mode 100644
index 0000000000..9c3801faf0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail7.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE PolyKinds #-}
+module T16326_Fail7 where
+
+import Data.Kind
+
+-- Make sure that this doesn't parse as something goofy like
+--  forall (forall :: Type -> Type) (k :: Type). forall k -> k -> Type
+data Foo :: forall k -> k -> Type
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail7.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail7.stderr
new file mode 100644
index 0000000000..13fc416995
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail7.stderr
@@ -0,0 +1,5 @@
+
+T16326_Fail7.hs:8:13: error:
+    Illegal symbol ‘forall’ in type
+    Perhaps you intended to use RankNTypes or a similar language
+    extension to enable explicit-forall syntax: forall <tvs>. <type>
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail8.hs b/testsuite/tests/dependent/should_fail/T16326_Fail8.hs
new file mode 100644
index 0000000000..3a214edc31
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail8.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16326_Fail8 where
+
+class C a
+data Blah a
+instance forall a -> C (Blah a)
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
new file mode 100644
index 0000000000..16c2aa617e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
@@ -0,0 +1,6 @@
+
+T16326_Fail8.hs:7:10: error:
+    Illegal class instance: ‘forall a -> C (Blah a)’
+      Class instances must be of the form
+        context => C ty_1 ... ty_n
+      where ‘C’ is a class
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail9.hs b/testsuite/tests/dependent/should_fail/T16326_Fail9.hs
new file mode 100644
index 0000000000..084a908a3a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail9.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+module T16326_Fail9 where
+
+lol :: forall a. a
+lol = undefined
+
+t :: Bool
+t = lol @(forall a -> a -> a) undefined True
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr
new file mode 100644
index 0000000000..3ad4e754a9
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail9.stderr
@@ -0,0 +1,8 @@
+
+T16326_Fail9.hs:11:5: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a -> a -> a
+      (GHC does not yet support this)
+    • In the expression: lol @(forall a -> a -> a) undefined True
+      In an equation for ‘t’:
+          t = lol @(forall a -> a -> a) undefined True
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 4b258cc065..ca8a50addf 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -40,3 +40,15 @@ test('T15743d', normal, compile_fail, [''])
 test('T15825', normal, compile_fail, [''])
 test('T15859', normal, compile_fail, [''])
 test('T15264', normal, compile_fail, [''])
+test('T16326_Fail1', normal, compile_fail, [''])
+test('T16326_Fail2', normal, compile_fail, [''])
+test('T16326_Fail3', normal, compile_fail, [''])
+test('T16326_Fail4', normal, compile_fail, [''])
+test('T16326_Fail5', normal, compile_fail, [''])
+test('T16326_Fail6', normal, compile_fail, [''])
+test('T16326_Fail7', normal, compile_fail, [''])
+test('T16326_Fail8', normal, compile_fail, [''])
+test('T16326_Fail9', normal, compile_fail, [''])
+test('T16326_Fail10', normal, compile_fail, [''])
+test('T16326_Fail11', normal, compile_fail, [''])
+test('T16326_Fail12', normal, compile_fail, [''])
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index 9a0c6b8e6e..1bc285ac3b 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -379,6 +379,7 @@
                    ({ DumpRenamedAst.hs:19:11-33 }
                     (HsForAllTy
                      (NoExt)
+                     (ForallInvis)
                      [({ DumpRenamedAst.hs:19:18-19 }
                        (UserTyVar
                         (NoExt)
diff --git a/testsuite/tests/th/T16326_TH.hs b/testsuite/tests/th/T16326_TH.hs
new file mode 100644
index 0000000000..df546b9df2
--- /dev/null
+++ b/testsuite/tests/th/T16326_TH.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16326_TH where
+
+import Control.Monad.IO.Class
+import Data.Kind
+import Data.Proxy
+import Language.Haskell.TH hiding (Type)
+import System.IO
+
+data Foo :: forall a -> a -> Type
+type family Foo2 :: forall a -> a -> Type where
+  Foo2 = Foo
+
+$(do info <- reify ''Foo2
+     liftIO $ hPutStrLn stderr $ pprint info
+
+     dec <- [d| data Nested :: forall a. forall b -> forall c.
+                               forall d -> forall e.
+                               Proxy '[a,b,c,d,e] -> Type |]
+     liftIO $ hPutStrLn stderr $ pprint dec
+     pure dec)
diff --git a/testsuite/tests/th/T16326_TH.stderr b/testsuite/tests/th/T16326_TH.stderr
new file mode 100644
index 0000000000..8a41fd116d
--- /dev/null
+++ b/testsuite/tests/th/T16326_TH.stderr
@@ -0,0 +1,22 @@
+type family T16326_TH.Foo2 :: forall (a_0 :: *) -> a_0 -> * where
+    T16326_TH.Foo2 = T16326_TH.Foo
+data Nested_0 :: forall a_1 .
+                 forall b_2 ->
+                 forall c_3 .
+                 forall d_4 ->
+                 forall e_5 .
+                 Data.Proxy.Proxy ('(:) a_1
+                                        ('(:) b_2 ('(:) c_3 ('(:) d_4 ('(:) e_5 '[]))))) ->
+                 *
+T16326_TH.hs:(17,3)-(24,13): Splicing declarations
+    do info <- reify ''Foo2
+       liftIO $ hPutStrLn stderr $ pprint info
+       dec <- [d| data Nested :: forall a.
+                                 forall b ->
+                                 forall c. forall d -> forall e. Proxy '[a, b, c, d, e] -> Type |]
+       liftIO $ hPutStrLn stderr $ pprint dec
+       pure dec
+  ======>
+    data Nested :: forall a.
+                   forall b ->
+                   forall c. forall d -> forall e. Proxy '[a, b, c, d, e] -> Type
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 7d6340bc43..70070a4687 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -13,7 +13,7 @@ if config.have_ext_interp :
        setTestOpts(extra_ways(['ext-interp']))
        setTestOpts(only_ways(['normal','ghci','ext-interp']))
 
-broken_tests = ["ClosedFam1TH","T10620","T10828","T11721_TH","T11797","T12045TH2","T12478_1","T12646","T13642","T14060","T15502","T15738","T15792","T15845","T16180","T1835","T3920","T4135","T4188","T5037","T5362","T7477","T7910","T8761","T8884","T8953","T9262","T9692","T9738","TH_Lift","TH_RichKinds","TH_RichKinds2","TH_Roles3","TH_TyInstWhere2","TH_implicitParams","TH_recursiveDo","TH_reifyDecl1","TH_reifyExplicitForAllFams","TH_reifyInstances","TH_reifyMkName","TH_repE2","TH_repGuard","TH_repPrim","TH_repPrim2","TH_repUnboxedTuples","TH_spliceE6"]
+broken_tests = ["ClosedFam1TH","T10620","T10828","T11721_TH","T11797","T12045TH2","T12478_1","T12646","T13642","T14060","T15502","T15738","T15792","T15845","T16180","T1835","T3920","T4135","T4188","T5037","T5362","T7477","T7910","T8761","T8884","T8953","T9262","T9692","T9738","TH_Lift","TH_RichKinds","TH_RichKinds2","TH_Roles3","TH_TyInstWhere2","TH_implicitParams","TH_recursiveDo","TH_reifyDecl1","TH_reifyExplicitForAllFams","TH_reifyInstances","TH_reifyMkName","TH_repE2","TH_repGuard","TH_repPrim","TH_repPrim2","TH_repUnboxedTuples","TH_spliceE6","T16326_TH"]
 # ext-interp, integer-gmp and llvm is broken see #16087
 def broken_ext_interp(name, opts):
 	if name in broken_tests and config.ghc_built_by_llvm:
@@ -471,3 +471,4 @@ test('T16180', normal, compile_and_run, ['-package ghc'])
 test('T16183', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T16195', normal, multimod_compile, ['T16195.hs', '-v0'])
 test('T16293b', normal, compile, [''])
+test('T16326_TH', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
diff --git a/utils/haddock b/utils/haddock
-Subproject c323c257be0bc118a0501416f06bda8fd51c92f
+Subproject 8459c600e0f6da3f85abefdefe651bbe3ed3da4
author	Ryan Scott <ryan.gl.scott@gmail.com>	2018-12-17 20:54:36 -0500
committer	Marge Bot <ben+marge-bot@smart-cactus.org>	2019-03-01 16:26:02 -0500
commit	c26d299dc422f43b8c37da4b26da2067eedcbae8 (patch)
tree	517d7b87043152bee667485e186314d19b55cfba
parent	f838809f1e73c20bc70926fe98e735297572ac60 (diff)
download	haskell-c26d299dc422f43b8c37da4b26da2067eedcbae8.tar.gz