Visible dependent quantification (VDQ) is a new language feature (discussed in this GHC proposal) that will debut in GHC 8.10. VDQ grants the programmer to write first-class kinds that dependently quantify their arguments, such as forall k -> k -> Type. The key difference between this kind and forall k. k -> Type is the presence of an arrow after the forall, which indicates that the forall is visible. That is to say, a user must explicitly provide the k argument when instantiating it, rather than relying on type inference to figure it out implicitly.

In this talk, I will explain in more detail what VDQ is and provide examples to demonstrate situations where VDQ can be useful. Since VDQ is required in order to implement a handful of other GHC proposals, such as top-level kind signatures and constrained type families, I will also briefly discuss the interaction between VDQ and these proposals.

If the word “dependent” in “visible dependent quantification” brings Dependent Haskell to mind, that is no coincidence, as VDQ can be considered a very limited form of dependent types. In this talk, I will clarify the relationship between VDQ and Dependent Haskell, and consider what dependently types programs a user can (and cannot) write with VDQ.