Skip to content
  • Ryan Scott's avatar
    Visible dependent quantification · c26d299d
    Ryan Scott authored and Marge Bot's avatar Marge Bot committed
    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.
    c26d299d