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 typeForallVisFlag
to distinguish between invisibleforall
s (i.e, with dots) and visibleforall
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 toTcValidity
. - Introducing
splitLHsSigmaTyInvis
, a variant ofsplitLHsSigmaTy
that only splits invisibleforall
s. This function is used in certain places (e.g., in instance declarations) to ensure that GHC doesn't try to split visibleforall
s (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.