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
HsForAllTyto add an additional field of typeForallVisFlagto distinguish between invisibleforalls (i.e, with dots) and visibleforalls (i.e., with arrows) - Changing
Parser.yaccordingly
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
vdqAllowedpredicate toTcValidity. - Introducing
splitLHsSigmaTyInvis, a variant ofsplitLHsSigmaTythat only splits invisibleforalls. This function is used in certain places (e.g., in instance declarations) to ensure that GHC doesn't try to split visibleforalls (e.g., if it tried splittinginstance 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.