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.

5 files changed, 31 insertions, 6 deletions

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`,