[GHC] #16326: Implement visible dependent quantification

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

[GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:  8.10.1
          Component:  Compiler       |           Version:  8.7
           Keywords:  GHCProposal    |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #15658
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC proposal 35 ([https://github.com/ghc-proposals/ghc-
 proposals/blob/master/proposals/0035-forall-arrow.rst A syntax for visible
 dependent quantification]) has been accepted. This ticket tracks its
 implementation.

 Along with implementing it, we should also document it in the users' guide
 (the subject of #15658).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:  GHCProposal
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 What about GHC Proposal 81 [https://github.com/ghc-proposals/ghc-
 proposals/pull/81 Syntax for visible dependent quantification].  How do 35
 and 81 relate?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:  GHCProposal
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Those are the exact same thing. The link you gave is the pull request that
 was later assigned the number 35 in `ghc-proposals`' indexing scheme when
 it was merged. (The number 81 just means that it was the 81st pull request
 that the repo had in its history.)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  patch
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:  GHCProposal
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/378
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  new => patch
 * differential:   => https://gitlab.haskell.org/ghc/ghc/merge_requests/378


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  patch
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:  GHCProposal,
                                     |  VisibleDependentQuantification
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/378
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * keywords:  GHCProposal => GHCProposal, VisibleDependentQuantification


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  closed
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:  fixed             |             Keywords:  GHCProposal,
                                     |  VisibleDependentQuantification
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  dependent/should_compile/T16326_Compile{1,2},
                                     |  dependent/should_fail/T16326_Fail{1,2,3,4,5,6,7,8,9,10,11,12},
                                     |  th/T16326_TH
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/378
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  patch => closed
 * testcase:   =>
     dependent/should_compile/T16326_Compile{1,2},
     dependent/should_fail/T16326_Fail{1,2,3,4,5,6,7,8,9,10,11,12},
     th/T16326_TH
 * resolution:   => fixed


Comment:

 Landed in
 [https://gitlab.haskell.org/ghc/ghc/commit/c26d299dc422f43b8c37da4b26da2067eedcbae8
 c26d299dc422f43b8c37da4b26da2067eedcbae8].

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  closed
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:  fixed             |             Keywords:  GHCProposal,
                                     |  VisibleDependentQuantification
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  dependent/should_compile/T16326_Compile{1,2},
                                     |  dependent/should_fail/T16326_Fail{1,2,3,4,5,6,7,8,9,10,11,12},
                                     |  th/T16326_TH
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/378
-------------------------------------+-------------------------------------

Comment (by Marge Bot <ben+marge-bot@…>):

 In [changeset:"c26d299dc422f43b8c37da4b26da2067eedcbae8/ghc" c26d299/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="c26d299dc422f43b8c37da4b26da2067eedcbae8"
 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 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.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  closed
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:  fixed             |             Keywords:  GHCProposal,
                                     |  VisibleDependentQuantification
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  dependent/should_compile/T16326_Compile{1,2},
                                     |  dependent/should_fail/T16326_Fail{1,2,3,4,5,6,7,8,9,10,11,12},
                                     |  th/T16326_TH
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/378
-------------------------------------+-------------------------------------

Comment (by goldfire):

 :)

 We discussed the possibility of allowing VDQ in visible type applications,
 and how this patch wouldn't do so. Is there a Trac ticket requesting this?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16326: Implement visible dependent quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16326: Implement visible dependent quantification
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  task              |               Status:  closed
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.7
      Resolution:  fixed             |             Keywords:  GHCProposal,
                                     |  VisibleDependentQuantification
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  dependent/should_compile/T16326_Compile{1,2},
                                     |  dependent/should_fail/T16326_Fail{1,2,3,4,5,6,7,8,9,10,11,12},
                                     |  th/T16326_TH
      Blocked By:                    |             Blocking:
 Related Tickets:  #15658            |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/378
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:7 goldfire]:
 > We discussed the possibility of allowing VDQ in visible type
 applications, and how this patch wouldn't do so. Is there a Trac ticket
 requesting this?

 #16371.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16326#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets