GitLab

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 foralls (i.e, with dots) and visible foralls (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 foralls. This function is used in certain places (e.g., in instance declarations) to ensure that GHC doesn't try to split visible foralls (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 (closed). Also fixes #15658 (closed) by documenting this feature in the users' guide.