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.

7 files changed, 105 insertions, 20 deletions

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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~