#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

#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

#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 ): 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

#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