Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,929
    • Issues 4,929
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 462
    • Merge requests 462
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Merge requests
  • !378

Visible dependent quantification

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Ryan Scott requested to merge RyanGlScott/ghc:visible-dependent-quantification into master Feb 15, 2019
  • Overview 77
  • Commits 1
  • Pipelines 10
  • Changes 64

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.

Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: visible-dependent-quantification