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.

3 files changed, 48 insertions, 1 deletions

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'])