#15658: strange inferred kind with TypeInType -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: TypeInType, | GHCProposal Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeInType, GHCProposal Comment: This is expected: `TypeInType` gives programmers a limited ability to write dependent quantification in kinds. The [https://downloads.haskell.org/~ghc/8.4.3/docs/html/users_guide/glasgow_exts.... #inferring-dependency-in-datatype-declarations Inferring dependency in datatype declarations] section of the users' guide documents this feature to some degree. The part that is not documented is the `forall k ->` bit, which I'll briefly explain here. Here is the type family you wrote (with explicit kinds for clarity): {{{#!hs type family F (f :: *) (a :: *) :: a }}} This binds the `f` and `a` type variables, and interestingly enough, it //reuses// the bound `a` type variable later in the return kind. In other words, `a` is used in a dependent fashion, so the kind for `F` is (again, with explicit kinds for clarity): {{{#!hs F :: * -> forall (a :: *) -> a }}} This kind says that `F` takes two type arguments of kind `*` and returns a type of kind `a`, where `a` is the second type argument. Importantly, the kind of `F` is //not// `* -> forall (a :: *). a`, since that would imply that `a` is insivible (i.e., that you don't explicitly pass it as an argument to `F`). You can think of the use of `->` versus `.` as indicating visible arguments versus invisible ones. As I briefly mentioned before, this aspect of kinds is not really documented at the moment. This is partly because while you can observe these kinds in GHCi (through `:kind`), you cannot write them yourself (they'll simply fail to parse at the moment). [https://github.com/ghc- proposals/ghc-proposals/pull/81 This GHC proposal] aims to rectify this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15658#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15658: strange inferred kind with TypeInType -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: TypeInType, | GHCProposal Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:2 dmwit]:

So without the explicit kinding, I would expect ghci to give `G` the kind `forall a -> a`. But ghci does not agree:

{{{

...

:k G G :: a }}}

That's due to a separate GHC bug, #14238, which has been fixed in GHC 8.6.1. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15658#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15658: strange inferred kind with TypeInType -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.4.2 Resolution: | Keywords: TypeInType, | GHCProposal, | VisibleDependentQuantification Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #16326 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/378 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeInType, GHCProposal => TypeInType, GHCProposal, VisibleDependentQuantification -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15658#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15658: strange inferred kind with TypeInType -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.4.2 Resolution: fixed | Keywords: TypeInType, | GHCProposal, | VisibleDependentQuantification Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #16326 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/378 -------------------------------------+------------------------------------- Comment (by simonpj): Should we have a regression test here? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15658#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#15658: strange inferred kind with TypeInType -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.4.2 Resolution: fixed | Keywords: TypeInType, | GHCProposal, | VisibleDependentQuantification Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #16326 | 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/15658#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler